paper accepted to m4m http://m4m.loria.fr/M4M5/
==Abstract==
The Tableau Workbench (TWB) is a generic framework for building automated
theorem provers for arbitrary propositional logics. The TWB has a small core
that defines its general architecture, some extra machinery to specify
tableau-based provers and an abstraction language for expressing tableau
rules. This language allows users to ``cut and paste'' tableau rules from
textbooks and to specify a search strategy for applying those rules in a
systematic manner. A new logic module defined by a user is translated and
compiled with the proof engine to produce a specialized theorem prover for
that logic. The TWB provides various hooks for implementing blocking
techniques using histories and variables, as well as hooks for
utilising/defining optimisation techniques. We describe the latest version
of the TWB which has changed substantially since our system description in
TABLEAUX 2003.