Skip to main navigation Skip to search Skip to main content

Rigid E-unification is NP-complete.

  • University of Pennsylvania

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

7 Scopus citations

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 as in NP-complete problem. Some implications of this result regarding the complexity of theorem proving in first-order logic with equality are discussed.

Original languageEnglish
Title of host publicationProc Third Annu Symp on Logic in Comput Sci
PublisherPubl by IEEE
Pages218-227
Number of pages10
ISBN (Print)0818608536
StatePublished - 1988

Publication series

NameProc Third Annu Symp on Logic in Comput Sci

Fingerprint

Dive into the research topics of 'Rigid E-unification is NP-complete.'. Together they form a unique fingerprint.

Cite this