Record Details

A PATH ORDERING FOR PROVING TERMINATION OF AC REWRITE SYSTEMS

DSpace at IIT Bombay

View Archive Info
 
 
Field Value
 
Title A PATH ORDERING FOR PROVING TERMINATION OF AC REWRITE SYSTEMS
 
Creator KAPUR, D
SIVAKUMAR, G
ZHANG, HT
 
Subject ac rewrite systems
path ordering
 
Description We describe a method that extends the lexicographic recursive path ordering of Dershowitz and Kamin and Levy for proving termination of associative-commutative (AC) rewrite systems. Instead of comparing the arguments of an AC-operator using the multiset extension, we partition them into disjoint subsets and use each subset 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 can previous methods, such as associative path ordering, that restrict AC operators to be minimal or subminimal in precedence. A number of examples illustrating the power of the approach are discussed. The method has been implemented in RRL, Rewrite Rule Laboratory, a theorem-proving environment based on rewrite techniques and completion.
 
Publisher KLUWER ACADEMIC PUBL
 
Date 2011-08-17T03:01:23Z
2011-12-26T12:55:18Z
2011-12-27T05:44:04Z
2011-08-17T03:01:23Z
2011-12-26T12:55:18Z
2011-12-27T05:44:04Z
1995
 
Type Article
 
Identifier JOURNAL OF AUTOMATED REASONING, 14(2), 293-316
0168-7433
http://dx.doi.org/10.1007/BF00881859
http://dspace.library.iitb.ac.in/xmlui/handle/10054/9717
http://hdl.handle.net/10054/9717
 
Language en