English
 
Help Privacy Policy Disclaimer
  Advanced SearchBrowse

Item

ITEM ACTIONSEXPORT

Released

Report

Ordered semantic hyper-linking

MPS-Authors
/persons/resource/persons45200

Plaisted,  David
Programming Logics, MPI for Informatics, Max Planck Society;

External Resource
No external resources are shared
Fulltext (restricted access)
There are currently no full texts shared for your IP range.
Fulltext (public)

MPI-I-94-235.pdf
(Any fulltext), 248KB

Supplementary Material (public)
There is no public supplementary material available
Citation

Plaisted, D.(1994). Ordered semantic hyper-linking (MPI-I-94-235). Saarbrücken: Max-Planck-Institut für Informatik.


Cite as: https://hdl.handle.net/11858/00-001M-0000-0014-B5B7-2
Abstract
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.