THEOREM-PROVING USING EQUATIONAL MATINGS AND RIGID E-UNIFICATION

In this paper, it is shown that the method of matings due to Andrews and Bibel can be extended to (first-order) languages with equality. A decidable version of E-unification called rigid E-unification is introduced, and it is shown that the method of equational matings remains complete when used in conjunction with rigid E-unification. Checking that a family of mated sets is an equational mating is equivalent to the following restricted kind of E-unification. Problem Given E --> = {E(i)\1 less-than-or-equal-to i less-than-or-equal-to n} a family of n finite sets of equations and S = {<u(i),v(i)>\1 less-than-or-equal-to i less-than-or-equal-to n} a set of n pairs of terms, is there a substitution theta such that, treating each set theta(E(i)) as a set of ground equations (i.e., holding the variables in theta(E(i)) "rigid"), theta(u(i)), and theta(v(i)) are provably equal from theta(E(i)) for i = 1,...,n? Equivalently, is there a substitution theta such that theta(u(i)) and theta(v(i)) can be shown congruent from theta(E(i)) by the congruence closure method for i = 1,...,n? A substitution theta-solving the above problem is called a rigid E --> -unifier of S, and a pair <E -->,S> such that S has some rigid E --> -unifier is called an equational premating. It is shown that deciding whether a pair <E -->, S> is an equational premating is an NP-complete problem.