KIT | KIT-Bibliothek | Impressum | Datenschutz

A-ordered tableaux

Haehnle, Reiner; Klingenbeck, Stefan


In resolution proof procedures refinements based on A-orderings of
literals have a long tradition and are well investigated. In
tableau proof procedures such refinements were only recently
introduced by the authors of the present paper. In this paper we
prove the following results: we give a completeness proof of
A-ordered ground clause tableaux which is a lot easier to follow
than the previous one. The technique used in the proof is extended
to the non-clausal case as well as to the non-ground case and we
introduce an ordered version of Hintikka sets that shares the model
existence property of standard Hintikks sets. We show that
A-ordered tableaux are a proof confluent refinement of tableaux and
that A-ordered tableaux together with the connection refinement
yield an incomplete proof procedure. We introduce A-ordered
first-order NNF tableaux, prove their completeness, and we briefly
discuss implementation issues.

Volltext §
DOI: 10.5445/IR/35195
Cover der Publikation
Zugehörige Institution(en) am KIT Fakultät für Informatik – Institut für Logik, Komplexität und Deduktionssysteme (ILKD)
Publikationstyp Buch
Publikationsjahr 1995
Sprache Englisch
Identifikator urn:nbn:de:swb:90-AAA351956
KITopen-ID: 35195
Erscheinungsvermerk Karlsruhe 1995. (Interner Bericht. Fakultät für Informatik, Universität Karlsruhe. 1995,26.)
KIT – Die Forschungsuniversität in der Helmholtz-Gemeinschaft
KITopen Landing Page