A new method for proving termination of AC-rewrite systems

Abstract

A new method, which extends the lexicographic recursive path ordering of Dershowitz and Kamin and Levy, to prove termination of associative-commutative (AC) rewrite systems is proposed. Instead of comparing the arguments of an AC-operator using the multiset extension, we partition them into disjoint subsets and each subset is used only once for comparison. To preserve transitivity, we introduce two techniques–pseudocopying and elevating of arguments of an AC operator. This method imposes no restrictions at all on the underlying precedence relation on function symbols. It can therefore prove termination of a much more extensive class of AC rewrite systems, than previous methods such as associative path ordering which restrict AC operators to be minimal or sub-minimal in precedence. A number of examples illustrating the power of the approach are discussed. The method has been implemented in SUTRA (formerly called RRL, Rewrite Rule Laboratory), a theorem proving environment based on rewrite techniques and completion.