Rigid E-unification: NP-completeness and applications to equational matings (Q921913)

The completeness of the method of equational matings is preserved when unrestricted E-unification is replaced by rigid E-unification. By showing that rigid E-unification is decidable, the authors eliminate one of the reasons for the undecidability of the method of equational matings. They also prove that rigid E-unification is NP-complete and that finite complete sets of rigid E-unifiers always exist. Finally, they discuss some implications of these results regarding the complexity of theorem proving in first-order logic with equality; for instance, the problem of deciding whether a family of mated sets is an equational mating is NP- complete, whereas the analogous problem for languages without equality can be solved in linear time.