Model generation style completeness proofs for constraint tableaux with superposition
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 | Fakultät für Informatik – Institut für Logik, Komplexität und Deduktionssysteme (ILKD) |
| Publikationstyp | Buch |
| Publikationsjahr | 2001 |
| Sprache | Englisch |
| Identifikator | urn:nbn:de:swb:90-AAA182820018 KITopen-ID: 18282001 |
| Erscheinungsvermerk | Karlsruhe 2001. (Interner Bericht. Fakultät für Informatik, Universität Karlsruhe. 2001,20.) |