KIT | KIT-Bibliothek | Impressum
Open Access Logo
URN: urn:nbn:de:swb:90-AAA223961

Implementing semantic tableaux

Posegga, Joachim; Schmitt, Peter H.


This report describes implementions of the tableau calculus for
first-order logic. First an extremely simple implementation,
called leanTAP, is presented, which nonetheless covers the full
functionality of the calculus and is also competitive with respect
to performance. A second approach uses compilation techniques for
proof search. Improvements inculding universal variables and
lemmata are considered as well as more efficient data structures
using reduced ordered binary decision diagrams. The implementation
language is PROLOG. In all cases fully operational PROLOG code is
given. For leanTAP a formal proof of the correctness of the
implementation is given relying on the operational semantics of
PROLOG as given by the SLD-tree model.

This report will appear as a chapter in the
Handbook of Tableau-based Methods in Automated Deduction
edited by: D. Gabbay, M. D'Agostino, R. H\"{a}hnle, and

Electronic availability will be discontinued after final acceptance
for publication is obtained.

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