A TOTAL AC-COMPATIBLE ORDERING BASED ON RPO

摘要

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. [References: 20]