Orderings and Constraints: Theory and Practice of Proving Termination

In contrast to the current general way of developing tools for proving termination automatically, this paper intends to show an alternative program based on using on the one hand the theory of term orderings to develop powerful and widely applicable methods and on the other hand constraint based techniques to put them in practice. In order to show that this program is realizable a constraint-based framework is presented where ordering based methods for term rewriting, including extensions like Associative-Commutative rewriting, ContextSensitive rewriting or Higher-Order rewriting, as well as the use of rewriting strategies, can be put in practice in a natural way.

• Type: Conference
• Year: 2007
• Where: BIRTHDAY
• Authors: Cristina Borralleras, Albert Rubio
• Keywords: Applied Computing, BIRTHDAY 2007, Contextsensitive Rewriting, Current General Way, Term Rewriting