Defining the Calculus for a Logic

A tableau calculus is defined in the TWB by writing a ''logic module'' like s4.ml containing four main sections: CONNECTIVES for defining the concrete syntax of formulae; HISTORIES for defining the variables and histories; TABLEAU for defining the of tableau rules; and STRATEGY for defining the systematic proof-search procedure. A logic module is automatically translated into OCaml code and then compiled and linked to the TWB libraries. The resulting object is an automatic theorem prover that accepts formulae with a syntax as specified in the connectives section and which outputs the derivation tree. Our rule syntax mimics the literature so that non-technical users can ``cut and paste'' their favourite rules. By using only the Connectives and Tableau Rules, a naive user can easily implement a rudimentary prover for the chosen logic. The Histories and Strategy hooks allow more expert users to assert greater control over the prover, and in the extreme case, even have access to the full underlying programming language. By compiling rules to native code, it is possible to run the prover at full speed, bypassing any intermediate abstraction layer. Moreover it simplifies the design of the underlying abstract machine, and ultimately reduces the TWB to a collection of high order functors.