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/