Gallier, Jean HNarendran, PaliathPlaisted, DavidSnyder, Wayne2023-05-222023-05-221988-03-012007-09-25https://repository.upenn.edu/handle/20.500.14332/7576Rigid 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.GRASPReport