MPI-INF/SWS Research Reports 1991-2021

2. Number - All Departments


Ordered semantic hyper-linking

Plaisted, David A.

August 1994, 22 pages.

Status: available - back from printing

We propose a method for combining the clause linking theorem proving method with theorem proving methods based on orderings. This may be useful for incorporating term-rewriting based approaches into clause linking. In this way, some of the propositional inefficiencies of ordering-based approaches may be overcome, while at the same time incorporating the advantages of ordering methods into clause linking. The combination also provides a natural way to combine resolution on non-ground clauses, with the clause linking method, which is essentially a ground method. We describe the method, prove completeness, and show that the enumeration part of clause linking with semantics can be reduced to polynomial time in certain cases. We analyze the complexity of the proposed method, and also give some plausibility arguments concerning its expected performance.

  • Attachement: MPI-I-94-235.dvi (117 KBytes); (290 KBytes); MPI-I-94-235.pdf (248 KBytes)

URL to this document:

Hide details for BibTeXBibTeX
  AUTHOR = {Plaisted, David A.},
  TITLE = {Ordered semantic hyper-linking},
  TYPE = {Research Report},
  INSTITUTION = {Max-Planck-Institut f{\"u}r Informatik},
  ADDRESS = {Im Stadtwald, D-66123 Saarbr{\"u}cken, Germany},
  NUMBER = {MPI-I-94-235},
  MONTH = {August},
  YEAR = {1994},
  ISSN = {0946-011X},