DocumentCode
2268756
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
fYear
1988
fDate
0-0 1988
Firstpage
218
Lastpage
227
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;
fLanguage
English
Publisher
ieee
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
Type
conf
DOI
10.1109/LICS.1988.5121
Filename
5121
Link To Document