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

Implementing tableaux by decision diagrams

Goubault-Larrecq, Jean


Binary Decision Diagrams (BDDs) are usually thought of as devices
engineered specially for classical propositional logic. We show
that we can build on one of their variants, Minato's zero-suppressed
BDDs, to build compact data structures that encode whole tableaux.
We call these structures tableaux decision diagrams (TDDs), and show
how tableaux proof search is implemented in this framework. For
this to be efficient, we have to restrict to canonical proof formats
(in the sense of Galmiche et al.) to be able to take advantage of
sharing in TDDs. Sharing is fundamental, not because it reduces
memory consumption, but because it allows us to expand or close many
tableaux paths in parallel, with corresponding gains in efficiency.
We provide some empirical evidence that this is indeed efficient, by
illustrating the method on a well-chosen system for propositional
intuitionistic logic.

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