To be delivered at TABLEAUX 2007 : http://tableaux2007.univ-cezanne.fr

Authors: Pietro Abate and Rajeev Gore

Level: You should know the basics of tableau/sequent calculi as

explained in the Handbook of Tableau Methods (for example).

Only rudimentary programming knowledge is required but basic

functional programming knowledge would be ideal.

The following notions would be useful for understanding some of

the more advanced concepts: termination methods like

loop-checks and histories; optimisation methods like

backjumping and simplification; proof-theoretic notions like

invertible rules, contraction-free calculi and stoups.

Abstract:

Tableau/sequent calculi are now a standard method for automating

deduction in non-classical logics. The currently available avenue for

rapid prototyping of your favourite tableau/sequent calculus is to

modify LeanTAP since general logical frameworks like Coq, ELF,

Isabelle and NuPrl take months to master and existing provers like

the Logics Work Bench provide only a fixed number of logics. The TWB

is a generic tableau framework for building tableau/sequent-based

theorem provers for (non-classical) propositional logics.

The TWB provides an extremely simple way for specifying the syntax of

formulae and rules, together with a simple way to specify a search

strategy for rule applications. It provides basic facilities for

ensuring termination via loop checks (blocking) and also allows

information to be passed from children to parents using

variables. There are also hooks which allow you to implement more

complicated optimisation techniques like backjumping (use-check) and

(modal) simplification.

The underlying implementation uses high-level functional programming

to avoid imperative constructs, and is tuned for efficiency. For

example, our optimised implementation of modal logic K is competitive

against the Logics Work Bench. The TWB currently has implementations

tableau/sequent provers for the following propositional logics: CPL,

K, KT, S4, PLTL, UB, LCK, CTL. We plan to add the following soon: K4,

K45, S5, G, Grz, PDL, Int, BiInt, Kt, Kt.S4 ...

We explain the basic architecture of the TWB, give pointers to the

theory underlying this architecture, and then concentrate on how to

build tableau-based and sequent-based theorem provers for various

propositional non-classical logics using case-studies and exercises.