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

Source:

(2007)

Abstract:

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.

Notes:

Paper sumbitted to Tableaux 2007 http://tableaux2007.univ-cezanne.fr/