Anzeige
Erschienen in:
2005 | OriginalPaper | Buchkapitel
The Space Efficiency of OSHL
verfasst von : Swaha Miller, David A. Plaisted
Erschienen in: Automated Reasoning with Analytic Tableaux and Related Methods
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
Ordered semantic hyper-linking (OSHL) is a first-order theorem prover that tries to take advantage of the speed of propositional theorem proving techniques. It instantiates first-order clauses to ground clauses, and applies propositional techniques to these ground clauses. OSHL-U extends OSHL with rules for unit clauses to speed up the instantiation strategy. OSHL-U obtains many of the same proofs as Otter does. This shows that many first-order theorems can be obtained without true unification, so techniques used to speed up propositional provers may be applicable to them. OSHL-U, in finding proofs, also generates and stores significantly fewer clauses than resolution prover Otter on many TPTP problems. On some TPTP groups, OSHL-U finds more proofs than Otter, despite a slower inference rate.