Recursive Path Orderings Can Also Be Incremental

10 years 4 months ago
Recursive Path Orderings Can Also Be Incremental
In this paper the Recursive Path Ordering is adapted for proving termination of rewriting incrementally. The new ordering, called Recursive Path Ordering with Modules, has as ingredients not only a precedence but also an underlying ordering =B. It can be used for incremental (innermost) termination proofs of hierarchical unions by defining =B as an extension of the termination proof obtained for the base system. Furthermore, there are practical situations in which such proofs can be done modularly.
Mirtha-Lina Fernández, Guillem Godoy, Alber
Added 28 Jun 2010
Updated 28 Jun 2010
Type Conference
Year 2005
Where LPAR
Authors Mirtha-Lina Fernández, Guillem Godoy, Albert Rubio
Comments (0)