Abstract
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.
| Original language | English |
|---|---|
| Title of host publication | Proceedings of the 5th Workshop on Methods for Modalities (M4M5 2007) |
| Editors | C. Areces, S. Demri |
| Place of Publication | The Netherlands |
| Publisher | Elsevier |
| Pages | 55-67 |
| Edition | Peer Reviewed |
| ISBN (Print) | 1571-0661 |
| DOIs | |
| Publication status | Published - 2009 |
| Event | Workshop on Methods for Modalities (M4M5 2007) - Cachan France Duration: 1 Jan 2009 → … http://dx.doi.org/10.1016/j.entcs.2009.02.025 |
Publication series
| Name | |
|---|---|
| Number | C |
| Volume | 231 |
Conference
| Conference | Workshop on Methods for Modalities (M4M5 2007) |
|---|---|
| Period | 1/01/09 → … |
| Other | November 29-30 2007 |
| Internet address |