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

Authors: 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}
  }