Paramodulation with Built-in AC-Theories and Symbolic Constraints

Complete paramodulation strategies are developed for clauses with symbolic constraints and built-in associativity and commutativity (AC) properties for a subset of the function symbols. Apart from the reduced search space due to the inherited ordering and unification restrictions of the inferences (cf. Nieuwenhuis and Rubio, 1995), symbolic constraints turn out to be especially useful in the context of built-in equationaltheoriesE. In every inference, instead of producing as many conclusions as minimalE-unifiers of two termssandt, one single conclusion is generated with an additionalE-unification problems = tkept in its constraint. In the AC-case developed here (the most extensively studied built-in theory), the computation of the (doubly exponentially many) AC-unifiers can thus be completely avoided. These results are also applied here to more efficient strategies (sometimes decision procedures) in theories expressed by finitesaturatedsets of clauses and, in particular, to rewriting and Knuth–Bendix completion modulo AC.