Implementing tableaux by decision diagrams

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.