System description: The Tableau workbench

Pietro Abate; Rajeev Gore

doi:10.1016/j.entcs.2009.02.029

System description: The Tableau workbench

Pietro Abate, Rajeev Gore

Research output: Chapter in Book/Report/Conference proceeding › Conference Paper › peer-review

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	https://doi.org/10.1016/j.entcs.2009.02.029
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	http://dx.doi.org/10.1016/j.entcs.2009.02.025

Access to Document

10.1016/j.entcs.2009.02.029

Cite this

@inproceedings{49388fa44bc244dda6a8cb9ce758b701,

title = "System description: The Tableau workbench",

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.",

author = "Pietro Abate and Rajeev Gore",

year = "2009",

doi = "10.1016/j.entcs.2009.02.029",

language = "English",

isbn = "1571-0661",

publisher = "Elsevier",

number = "C",

pages = "55--67",

editor = "\{C. Areces, S. Demri\}",

booktitle = "Proceedings of the 5th Workshop on Methods for Modalities (M4M5 2007)",

address = "Netherlands",

edition = "Peer Reviewed",

note = "Workshop on Methods for Modalities (M4M5 2007) ; Conference date: 01-01-2009",

url = "http://dx.doi.org/10.1016/j.entcs.2009.02.025",

}

TY - GEN

T1 - System description: The Tableau workbench

AU - Abate, Pietro

AU - Gore, Rajeev

PY - 2009

Y1 - 2009

N2 - 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.

AB - 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.

UR - https://www.scopus.com/pages/publications/62649138772

U2 - 10.1016/j.entcs.2009.02.029

DO - 10.1016/j.entcs.2009.02.029

M3 - Conference Paper

SN - 1571-0661

SP - 55

EP - 67

BT - Proceedings of the 5th Workshop on Methods for Modalities (M4M5 2007)

A2 - null, C. Areces, S. Demri

PB - Elsevier

CY - The Netherlands

T2 - Workshop on Methods for Modalities (M4M5 2007)

Y2 - 1 January 2009

ER -

System description: The Tableau workbench

Abstract

Publication series

Conference

Access to Document

Other files and links

Fingerprint

Cite this