Termination of rewrite systems by elementary interpretations |
| |
Authors: | Pierre Lescanne |
| |
Affiliation: | (1) Centre de Recherche en Informatique de Nancy (CNRS) and INRIA-Lorraine, Campus Scientifique, BP 239, 54506 Vanduvre-lès-Nancy, France |
| |
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: | Rewrite systems Termination Well-foundedness Total connection |
本文献已被 SpringerLink 等数据库收录! |
|