Skip navigation
Skip navigation

System description: The Tableau workbench

Abate, Pietro; Gore, Rajeev

Description

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...[Show more]

dc.contributor.authorAbate, Pietro
dc.contributor.authorGore, Rajeev
dc.coverage.spatialCachan France
dc.date.accessioned2015-12-10T22:29:17Z
dc.date.createdNovember 29-30 2007
dc.identifier.isbn1571-0661
dc.identifier.urihttp://hdl.handle.net/1885/54837
dc.description.abstractThe 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.
dc.publisherElsevier
dc.relation.ispartofseriesWorkshop on Methods for Modalities (M4M5 2007)
dc.sourceProceedings of the 5th Workshop on Methods for Modalities (M4M5 2007)
dc.source.urihttp://dx.doi.org/10.1016/j.entcs.2009.02.025
dc.subjectKeywords: Automation; Hooks; Linguistics; Logic devices; Machinery; Semantic Web; automated deduction; Automated theorem provers; Blocking techniques; Cut and pastes; Generic frameworks; generic tableau theorem prover; Logic modules; Optimisation; Propositional log automated deduction; generic tableau theorem prover; system description; tableaux strategies
dc.titleSystem description: The Tableau workbench
dc.typeConference paper
local.description.notesImported from ARIES
local.description.refereedYes
dc.date.issued2009
local.identifier.absfor010107 - Mathematical Logic, Set Theory, Lattices and Universal Algebra
local.identifier.absfor080203 - Computational Logic and Formal Languages
local.identifier.absfor080299 - Computation Theory and Mathematics not elsewhere classified
local.identifier.ariespublicationu8803936xPUB311
local.type.statusPublished Version
local.contributor.affiliationAbate, Pietro, College of Engineering and Computer Science, ANU
local.contributor.affiliationGore, Rajeev, College of Engineering and Computer Science, ANU
local.description.embargo2037-12-31
local.bibliographicCitation.startpage55
local.bibliographicCitation.lastpage67
local.identifier.doi10.1016/j.entcs.2009.02.029
dc.date.updated2016-02-24T11:44:10Z
local.identifier.scopusID2-s2.0-62649138772
CollectionsANU Research Publications

Download

File Description SizeFormat Image
01_Abate_System_description:_The_2009.pdf140.18 kBAdobe PDF    Request a copy
02_Abate_System_description:_The_2009.pdf258.06 kBAdobe PDF    Request a copy


Items in Open Research are protected by copyright, with all rights reserved, unless otherwise indicated.

Updated:  19 May 2020/ Responsible Officer:  University Librarian/ Page Contact:  Library Systems & Web Coordinator