Tutorial: The Tableau Work Bench: Theory and Practice

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.