System Description: The Tableau WorkBench


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 like backjumping, simplification and caching. We
describe the latest version of the TWB which has changed substantially since our system
description in TABLEAU 2003.

Paper Submitted to CADE 2007

cade07.pdf43.04 KB