Title :
Rigid E-unification is NP-complete
Author :
Gallier, J. ; Snyder, W. ; Narendran, P. ; Plaisted, D.
Author_Institution :
CIS Dept., Pennsylvania Univ., Philadelphia, PA, USA
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.<>
Keywords :
formal logic; theorem proving; NP-complete; complexity of theorem proving; first-order languages; first-order logic; mated sets; rigid E-unification; theorem-proving method; unification modulo equational theories; Computational Intelligence Society; Equations; Logic; NP-complete problem; Polynomials;
Conference_Titel :
Logic in Computer Science, 1988. LICS '88., Proceedings of the Third Annual Symposium on
Conference_Location :
Edinburgh, UK
Print_ISBN :
0-8186-0853-6
DOI :
10.1109/LICS.1988.5121
