Developing path orderings for associative-commutative (AC) rewrite systems has been quite a challenge at least for a decade. Compatibility with the recursive path ordering (RPO) schemes is desirable, and this property helps in orienting the commonly encountered distributivity axiom as desired. For applications in theorem proving and constraint solving, a total ordering on ground terms involving AC operators is often required. It is shown how the main solutions proposed so far with the desired properties can be viewed as arising from a common framework. A general scheme that works for non-ground (general) terms also is proposed. The proposed definition allows flexibility (using different abstractions) in the way the candidates of a term with respect to an associative-commutative function symbol are compared, thus leading to at least two distinct orderings on terms (from the same precendence relation on funciton symbols).
To view the entire paper click here