Paper Info
Title
A total AC-compatible ordering based on RPO
Abstract
We define a simplification ordering on terms which is AC-compatible and total on non-AC-equivalent ground terms, without any restrictions on the signature like the number of AC-symbols or free symbols. Unlike previous work by Narendran and Rusinowitch (1991) our AC-RPO ordering is not based on polynomial interpretations, but on a simple extension of the well-known RPO ordering (with a total (arbitrary) precedence on the function symbols). This solves an open question posed e.g. by Bachmair (1992). A second difference is that this ordering is also defined on terms with variables, which makes it applicable in practice for complete theorem proving strategies with built-in AC-unification and for orienting non-ground rewrite systems. The ordering is defined in a simple way by means of rewrite rules, and can be easily implemented, since its main component is RPO.
Year
DOI
Venue
1995
10.1016/0304-3975(94)00276-2
Theor. Comput. Sci.
Keywords
DocType
Volume
total AC-compatible
Journal
142
Issue
ISSN
Citations 
2
Theoretical Computer Science
20
PageRank 
References 
Authors
0.92
17
2
Name
Order
Citations
PageRank
Albert Rubio122819.44
Robert Nieuwenhuis2140593.78