Tutorial: The Tableau Work Bench: Theory and Practice

===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, contracton-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.