The tableau workbench

P Abate, R Goré - Electronic Notes in Theoretical Computer Science, 2009 - Elsevier
P Abate, R Goré
Electronic Notes in Theoretical Computer Science, 2009Elsevier
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 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.
Elsevier