EVA STAR Trefferanzeige

Volltext Volltext.pdf1.pdf (357 KB)
URN (für Zitat) http://nbn-resolving.org/urn:nbn:de:swb:90-AAA403961
Titel Implementing tableaux by decision diagrams.
Autor Goubault-Larrecq, Jean
Institution Fakultät für Informatik (INFORMATIK)
Institut für Logik, Komplexität und Deduktionssysteme (ILKD)
Dokumenttyp Buch
Jahr 1996
Erscheinungsvermerk Karlsruhe 1996. (Interner Bericht. Fakultät für Informatik, Universität Karlsruhe. 1996,32.)
Abstract
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.