Theorem proving using equational matings and rigid E -unification

Abstract

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≤i≤n} a family of n finite sets of equations and S={⟨u _i ,v _i ⟩ |1≤i≤n} a set of n pairs of terms, is there a substitution θ such that, treating each set θ(E _i ) as a set of ground equations (i.e., holding the variables in θ(E _i ) “rigid”), θ(u _i ), and θ(v _i ) are provably equal from θ(E _i ) for i=1,...,n? Equivalently, is there a substitution θ such that θ(u _i ) and θ(v _i ) can be shown congruent from θ(E _i ) 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.