Rigid E-Unification: NP-Completeness and Applications to Equational Matings

Rigid E-unification is a restricted kind of unification modulo equational theories, or E-unification, that arises naturally in extending Andrews's theorem proving method of matings to first-order languages with equality. This extension was first presented in Gallier, Raatz, and Snyder, where it was conjectured that rigid E-unification is decidable. In this paper, it is shown that rigid E-unification is NP-complete and that finite complete sets of rigid E-unifiers always exist. As a consequence, deciding whether a family of mated sets is an equational mating is an NP-complete problem. Some implications of this result regarding the complexity of theorem proving in first-order logic with equality are also discussed.