Paper: Rigid E-unification is NP-complete (at LICS 1988)
Authors: Jean H. Gallier Wayne Snyder Paliath Narendran David A. PlaistedAbstract
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 Symp. on Logic in Computer Science, {LICS} 1988}, year = 1988, editor = {Yuri Gurevich}, month = {July}, pages = {218--227}, location = {Edinburgh, Scotland, UK}, publisher = {IEEE Computer Society Press} }