KIT | KIT-Bibliothek | Impressum
Open Access Logo
§
Volltext
URN: urn:nbn:de:swb:90-AAA182820018

Model generation style completeness proofs for constraint tableaux with superposition

Giese, Martin

Abstract:

We present several calculi that integrate equality handling
by superposition and ordered paramodulation into a free
variable tableau calculus. We prove completeness of this
calculus by an adaptation of the model generation technique
commonly used for completeness proofs of resolution calculi.
The calculi and the completeness proof are compared to earlier
results of Degtyarev and Voronkov.


Zugehörige Institution(en) am KIT Institut für Logik, Komplexität und Deduktionssysteme (ILKD)
Publikationstyp Buch
Jahr 2001
Sprache Englisch
Identifikator URN: urn:nbn:de:swb:90-AAA182820018
KITopen ID: 18282001
Erscheinungsvermerk Karlsruhe 2001. (Interner Bericht. Fakultät für Informatik, Universität Karlsruhe. 2001,20.)
KIT – Die Forschungsuniversität in der Helmholtz-Gemeinschaft KITopen Landing Page