## Paper: Rigid E-unification is NP-complete (at LICS 1988)

**Jean H. Gallier Wayne Snyder Paliath Narendran David A. Plaisted**

### Abstract

Rigid E-unification is a restricted kind of unification modulo equational theories, or E-unification, that arises naturally in extending P. Andrews' (1981) theorem-proving method of mating to first-order languages with equality. 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 discussed

### BibTeX

@InProceedings{GallierSnyderNarend-RigidEunificationis, author = {Jean H. Gallier and Wayne Snyder and Paliath Narendran and David A. Plaisted}, title = {Rigid E-unification is NP-complete}, booktitle = {Proceedings of the Third Annual IEEE Symposium on Logic in Computer Science (LICS 1988)}, year = {1988}, month = {July}, pages = {218--227}, location = {Edinburgh, Scotland, UK}, publisher = {IEEE Computer Society Press} }