Associative-Commutative Reduction Orderings via Head-Preserving Interpretations

Abstract

We introduce a generic definition of reduction orderings on term algebras containing associative-commutative (AC) operators. These orderings are compatible with the AC theory hence makes them suitable for use in deduction systems where AC operators are built-in. Furthermore, they have the nice property of being total on AC classes of ground terms, a required property for example to avoid failure in AC-completion, or to insure completeness of ordered strategies in first-order theorem proving with built-in AC operators. We show that the two definitions already known of such total and AC-compatible orderings [narendran91rta,nieuwenhuis93rta] are actually instances of our definition. Finally, we find new such orderings which have more properties, first an ordering based on an integer polynomial interpretation, answering positively to a question left open by Narendran and Rusinowitch, and second an ordering which allow to orient the distributivity axiom in the usual way, answering positively to a question of the RTA'93 open problems list.

full paper