Name
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.<> |
Year | DOI | Venue |
|---|---|---|
1988 | 10.1109/LICS.1988.5121 | Edinburgh, UK |
Keywords | Field | DocType |
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 | Discrete mathematics,NP-complete,Second-order logic,Unification,Modulo,Automated theorem proving,First-order logic,Mathematics | Conference |
Citations | PageRank | References |
19 | 1.47 | 6 |
Authors | ||
4 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Jean H. Gallier | 1 | 749 | 111.86 |
| Wayne Snyder | 2 | 225 | 23.79 |
| Paliath Narendran | 3 | 1100 | 114.99 |
| David A. Plaisted | 4 | 1680 | 255.36 |