The Tableau Workbench. 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.

References in zbMATH (referenced in 4 articles , 1 standard article )

Showing results 1 to 4 of 4.
Sorted by year (citations)

  1. McCabe-Dansted, John; Dixon, Clare; French, Tim; Reynolds, Mark: Sublogics of a branching time logic of robustness (2019)
  2. Golińska-Pilarek, Joanna; Muñoz-Velasco, Emilio; Mora-Bonilla, Angel: Relational dual tableau decision procedure for modal logic K (2012)
  3. van Valkenhoef, Gert; van der Vaart, Elske; Verbrugge, Rineke: OOPS: an (S5_n) prover for educational settings (2010) ioport
  4. Abate, Pietro; Goré, Rajeev: The Tableau Workbench (2009)