Ac-superposition with constraints: No AC-unifiers needed

Abstract

We prove the completeness of (basic) deduction strategies with constrained clauses modulo associativity and commutativity (AC). Here each inference generates one single conclusion with an additional equality s=ACt in its constraint (instead of one conclusion for each minimal AC-unifier, i.e. exponentially many). Furthermore, computing AC-unifiers is not needed at all. A clause C 〚 T 〛 is redundant if the constraint T is not AC-unifiable. If C is the empty clause this has to be decided to know whether C 〚 T 〛 denotes an inconsistency. In all other cases any sound method to detect unsatisfiable constraints can be used.