Theory and Practice of a Generic Tableau Engine: The Tableau WorkBench




The tableau method is widely used by logicians to give decision procedure for classical and non classical logics. But the move from proof-theoretic tool to an efficient automated theorem prover is often difficult for researchers with no technical background. The main ``problem'' is the non-determinism inherent in the tableau method. In this paper we give a functional algorithm to mechanize the tableau method which is concise and easy to re-use. We also briefly describe an implementation of this algorithm called the Tableau Workbench.


Paper sumbitted to Tableaux 2007