MPI-I-94-235. August 1994, 22 pages. | Status: available - back from printing | Next --> Entry | Previous <-- Entry
Abstract in LaTeX format:
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.
References to related material:
|To download this research report, please select the type of document that fits best your needs.||Attachement Size(s):|
|MPI-I-94-235.pdf||117 KBytes; 290 KBytes; 248 KBytes|
|Please note: If you don't have a viewer for PostScript on your platform, try to install GhostScript and GhostView|