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 Rubio | 1 | 228 | 19.44 |
Robert Nieuwenhuis | 2 | 1405 | 93.78 |