Documentation

The Tableaux Work Bench TWB is a generic framework for building automated theorem provers for arbitrary logics without learning complex programming languages. For modularity, the TWB architecture consists of loosely coupled libraries which can be individually replaced without compromising the soundness of the system. For generality, the TWB consists of a small core that defines a very generic infrastructure which can be easily adapted to implement different deduction methods. Some extra machinery tailors this core to tableau-based theorem proving and provides various hooks for optimisation techniques and loop-checking methods. For user-friendliness, there is a high level specification language to specify logical connectives, tableau rules and a strategy for proof-search. A logic module defined by the user is translated by the TWB into OCaml code, which is then compiled with the existing libraries to produce an OCaml program that implements a tableau prover for that logic. Non-programmers can enter their pen-and-paper specifications with minor modifications to implement naive provers for their favourite logics without learning OCaml. Expert users can utilise the various optimisation hooks to produce faster provers and even tailor the system to their own requirements by writing their own OCaml libraries. Whether the TWB can be used to produce truly efficient theorem provers is still open. We briefly describe the TWB architecture, its user interface and some benchmarks to show that it achieves its intended purpose of filling the middle ground for non-classical (currently propositional) theorem proving. The TWB should be particularly useful for teaching automated reasoning where the emphasis is on automated deduction methods rather than on programming techniques.