Theorem Proving Using Equational Matings and Rigid E-Unifications

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 = {Ei | 1 ≤ i ≤ n} a family of n finite sets of equations and S = {〈ui, vi〉 | 1 ≤ i ≤ n} a set of n pairs of terms, is there a substitution θ such that, treating each set θ(Ei) as a set of ground equations (i.e. holding the variables in θ(Ei) "rigid"), θ(ui) and θ(vi) are provably equal from θ(Ei) for i = 1, ... ,n? Equivalently, is there a substitution θ such that θ(ui) and θ(vi) can be shown congruent from θ(Ei) by the congruence closure method for i 1, ... , n? A substitution θ 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.