Termination of rewrite systems by elementary interpretations
- 1 January 1995
- journal article
- research article
- Published by Association for Computing Machinery (ACM) in Formal Aspects of Computing
- Vol. 7 (1) , 77-90
- https://doi.org/10.1007/bf01214624
Abstract
We focus on termination proofs of rewrite systems, especially of rewrite systems containing associative and commutative operators. We prove their termination by elementary interpretations, more specifically, by functions defined by addition, multiplication and exponentiation. We discuss a method based on polynomial interpretations and propose an implementation of a mechanisation of the comparison of expressions built with polynomials and exponentials.Keywords
This publication has 13 references indexed in Scilit:
- Termination by completionApplicable Algebra in Engineering, Communication and Computing, 1990
- A new method for proving termination of AC-rewrite systemsPublished by Springer Nature ,1990
- Implementation of completion by transition rules + control: ORMEPublished by Springer Nature ,1990
- Comtes — An experimental environment for the completion of term rewriting systemsLecture Notes in Computer Science, 1989
- An overview of LP, the Larch ProverLecture Notes in Computer Science, 1989
- Completion procedures as transition rules + controlPublished by Springer Nature ,1989
- Termination of rewriting systems by polynomial interpretations and its implementationScience of Computer Programming, 1987
- On word problems in equational theoriesPublished by Springer Nature ,1987
- Proving termination of associative commutative rewriting systems by rewritingPublished by Springer Nature ,1986
- Termination orderings for associative-commutative rewriting systemsJournal of Symbolic Computation, 1985