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