Proving associative-commutative termination using RPO-compatible orderings

Developing path orderings for associative-commutative (AC) rewrite systems has been quite a challenge at least for a decade. Compatibility with the re cursive path ordering (RPO) schemes is desirable, and this property helps i n orienting the commonly encountered distributivity axiom as desired. For a pplications 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 ([7],[13]) with the desired properties can b e viewed as arising from a common framework. A general scheme that works fo r non-ground (general) terms also is proposed. The proposed definition allo ws flexibility (using different abstractions) in the way the candidates of a term with respect to an associative-commutative function symbol are compa red, thus leading to at least two distinct orderings on terms (from the sam e precedence relation on function symbols).