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.

Motivations

Theorem provers for non-classical logics have matured dramatically in the last ten years. At one extreme, highly optimized and specific theorem provers like FACT and MSPASS can test formulae with hundreds of symbols within a few seconds. At the other extreme, generic logical frameworks like Isabelle allow us to implement almost any logical calculus as a "shallow embedding", and obtain a theorem prover for that logic by defining an associated collection of search tactics. But researchers that are merely interested in mechanising their favourite logic often find these tools too complex to modify or to program. For example, FACT is written in Lisp while Isabelle requires months to learn. In the middle are the LWB, Lotrec and LeanTap which implement many different logics or which allow users to create their own prover. The LWB provides a large (but fixed) number of logics while Lotrec requires the logic to have a binary relational semantics. If you have just invented a new tableau calculus for a logic without such semantics, then Lotrec and the LWB are not very useful. Lazy logicians, as opposed to real programmers, usually then extend LeanTap, but there is no generic LeanTap implementation that contains features like loop-checking or further optimisations. Moreover, the original LeanTap utilises various insights into the underlying Prolog engine like first argument indexing, and these are rarely understood or used in its extensions.

Architecture

The TWB is organised into four main components which total roughly 4000 lines of Ocaml code (loc). The core (464 loc) contains all type definitions and the strategy implementation. The data-type library (664 loc) implements support data structures. The tableau library (818) provides the machinery to implement tableau-based provers. The syntax library (1624) provides an easy way to access the TWB library and to define specific logic modules. Finally the command line interface (226 loc) provides a simple shell interface for compiling and executing the logic modules on input formulae. The core library defines the architecture of the prover using abstract data types. Figure ?? shows an overview of the structure of the core library, including the main methods of each class and the relation between each class and basic data type. The core library is composed of the following modules: *Sequence: Since OCaml is by design an eager language, we avoid wasteful computations by using a generic lazy list (library) to construct the proof tree; * Tree: Defines the proof tree data type; * Node: Defines a node as a generic container which encapsulates arbitrary data structures (like sets, multi-sets, sequences, etc.); * Rule: Implements the interface to define logical rules in the TWB. A rule can be seen as a re-writing function that is applied if a pre-condition is met. Defines the interface for specifying rules; * Strategy: The Strategy module implements an interpreter for the tactic language which is loosely related to the tactic language employed in theorem provers like Isabelle; * Visit: The Visit module implements the core algorithm to generate and visit the proof tree given the current node and the current state of the strategy;

Core Algorithm

[inline:algorithm.gif] The core algorithm of the TWB is a procedure to visit a tree that is generated by the repeated application of a finite set of rules to an initial node containing a finite number of formulae. The three main decisions to make are: which leaf to choose as the current node; which rule to apply to the chosen node; and which principal formula to choose from the chosen node for the chosen rule. This visit procedure is composed of two ''recursive functions'': the first function selects a new rule to be applied to the current node while the second function traverses the tree generated by the application of the rule, by recursively calling the visit procedure. In the figure above, we show a snapshot of the visit procedure by focusing on a node in the proof tree (the ''current node''). The visit procedure uses the following four basic components: * Rule condition: this function is used by the strategy procedure and checks if a rule is applicable to the current node and if the side conditions of the rule are satisfied. The result of this function is a partition of the current node according to the patterns specified in the numerator of the selected rule. * Rule action: this function accepts a rule that has been selected and applies it to the current node to expand the proof tree. The result of this function is a list of nodes, each identifying a new branch in the proof tree. *Branch condition:] this function is executed after visiting the i^th sub-tree rooted at the current node to determine if the sub-tree created so far (including all the already visited branches) satisfies a logic-specific condition. If so, the visit explores the next branch (if any), otherwise, the visit is interrupted and the procedure backtracks. * Rule backtrack: these functions are executed after all branches (or a number of them according to the branch condition) are visited to synthesise their results into one result for the current node and pass it up to its parent.

Programming Language and Style.

We considered Prolog, Mercury, Haskell, Java and C++ but wrote the TWB in OCaml because it is a functional language with a large number of third party libraries. Functional languages are more concise than languages like C or Java, and functional programs are therefore easier to maintain and more resistant to memory management problems and runtime errors. OCaml also has a broad community of users, many third party libraries and has already been used to implement other successful generic theorem provers like Coq, Hol light and NuPrl. OCaml is an hybrid language which mixes elements of imperative programming with its functional basis. To minimise coding errors and reduce maintenance time, the TWB core infrastructure uses a purely functional style. But to avoid some of the ensuing performance penalties, a number of data structures use imperative programming style. Currently the TWB runs on modern operating systems such as Gnu/Linux and MacOsX. Moreover, the TWB has virtually no dependencies on third-party software outside the OCaml compiler itself, making it easy to install and port to other platforms. Why not just use Isabelle? Surely you can do all this sort of stuff in any logical framework? We actually received a review for one of our papers which claimed that most of the TWB could be built within Isabelle in one afternoon's work. Yes, you can use Isabelle, and yes, you can build the whole of the TWB inside Isabelle or any other logical framework. But try it and you will soon see that what you get is an extremely slow behemoth which will not run at an acceptable speed. For example, just the various pattern matching and rewriting principles built into the TWB rule syntax will be hard enough. The reason is that Isabelle is too big a hammer for the nail we have. There is no need for all of the higher order machinery that comes for free with Isabelle. Ideally we want to turn off interaction and have the TWB find closed tableau automatically. So you will end up having to program tactics and tactical on top of the Isabelle version of the TWB anyway. Finally, Isabelle does not compile down to a stand alone program for the tableau calculus that you have designed. We challenge anyone that belives they can mimic the TWB in Isabelle (or any other logical framework) to try it and report back to us. In particular, please try to log the time it took you and record the run times for your prover for modal logic K and S4 say on our examples from the "demo" page.

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.

Example: S4


(* An version of Heuerding's S4 tableau calculus *)

SIMPLIFICATION := Kopt.simpl (* functions for modal simplification *)
PP := Kopt.nnf (* functions for nnf and modal simplification *)
NEG := Kopt.neg (* function to negate initial formula *)
open Twblib (* functions for manipulation of set-histories *)

CONNECTIVES
And, "_&_", Two; Or, "_v_", Two;
Imp, "_->_", One; DImp, "_<->_", One;
Dia, "Dia_", Zero; Box, "Box_", Zero;
Not, "~_", Zero
END

HISTORIES
(DIAS : Set of Formula := new Set.set);
(UBXS : Set of Formula := new Set.set)
END

TABLEAU
RULE Id { A } ; { ~ A } ; Z
======================
Close
END

RULE And { A & B } == A ; B END

RULE Or { A v B } ; X == A ; X[A] | B ; X[B] END

RULE T { Box P } == P
COND notin(P, UBXS)
ACTION [ UBXS := add(P,UBXS);
DIAS := emptyset(DIAS)
]
END

RULE S4 { Dia P } ; Z
----------------
P ; UBXS

COND notin(Dia P, DIAS)
ACTION [ DIAS := add(Dia P,DIAS) ]
END

END

STRATEGY := ( (False|Id|And|T|Or)* ; S4 )*

Connectives and Histories

==Defining Connectives == The connectives section defines the syntax of the formulae used in the rule definitions (as formula schema) and as input formulae. A connective is either a constant or is defined as a triple (Type, Form, Precedence) where the first component is an OCaml type constructor (which will be redundant in future releases), the second component specifies the concrete syntax with the underscore "_" interpreted as a meta-variable occurrence, and the third component is a binding strength "Zero'', "One'' or "Two'' with "Two'' the weakest. ==Defining Histories and Variables== Histories and variables allow users to decorate tableau nodes with additional data structures to maintain branch-wide information during proof search. Variables must begin with a lower-case letter and histories with an upper-case letter. Histories are used to pass information top-down and are typically used to implement blocking techniques. Variables are used to pass information bottom-up from already explored sub-trees to parents. For example, the traditional notion of a tableau being ``Open'' or ``Closed'' is carried from the leaves to the root by default variable called status. Histories and variables can be given a default value which is an OCaml expression of the correct type. Figure~\ref{fig:s4} contains two histories called DIAS and UBXS with each defined to be a set of formulae which is the empty set by default. The default value for singleton elements can be left unspecified. The default value for other data containers is just an empty instance of that data container.

Defining Rules

Tableau rules may consist of up to seven components: *Numerator: The numerator is a list of formula schemas separated by semicolons and specifies a partition of the current node in the proof tree. Formulae schemas are parsed according to the connectives declared in the connectives section with principal formulae enclosed in braces { }. A pattern is ''restricted'' if it is specified by a formula schema containing connectives like A -> B and Box A. A pattern is {\em unrestricted} if it is specified by just a meta-variable like X. There may be many ways of partitioning a node to match the pattern specified by the numerator leading to implicit choice-points. * Separator: A rule commits to the first numerator pattern choice if the separator between the numerator and denominators is a sequence of at least two "='' symbols. A rule backtracks over the different pattern choice-points if the separator is a sequence of at least two ``-'' symbols and the current partition choice does not close. Intuitively, a rule that commits is declared to be invertible and a rule that does not commit is declared to be non-invertible. However, the TWB does not check that the rule is really invertible. It assumes that the user has proved an inversion lemma independently. * Denominator: In general, a rule can have a list of denominators related by a branching operator. Each denominator is a list of formula schemas and specifies how to construct the root nodes of the branches that extend the tableau using the patterns assigned to the meta-variables in the numerator. The (universal) branch separator | is an instruction to close the current node if ''every'' denominator closes. The (existential) branch separator || is an instruction to close the current node if ''some'' denominator closes. These are actually instances of conditional branching which are instructions to close the current node if the denominators meet a specified condition. * Cond: A rule is applicable if the side-conditions are satisfied as specified using the COND construct. If all the side conditions are true, then the tentative partition is accepted. Otherwise the partition is not considered and the pattern matching algorithm proceeds until a successful partition is found. * Action: If the rule is applicable then the ACTION construct specifies actions on the current histories or variables to compute the histories of the children. * Branch: Conversely, branch conditions, specified by the keyword BRANCH, are executed on backtracking to check whether to explore the next branch (if there is one) or to backtrack further. It is possible to specify a list of branch conditions, one for every branch and each set of branch conditions will have access to all variables returned by any branch already explored. An attempt to access a variable related to a branch yet to be visit will generate a run-time error. * Backtrack: Specifies how to synthesise the result for the current node from the results of the children.

Defining the Strategy

A strategy specifies the order in which rules are applied during proof search. The TWB tactic language is nispeired to Isabelle tactic language. It has the following operators where '''t_1''' and '''t_2''' are tactics (terms built from this language) and '''r''' is a rule: '''Fail''', '''Skip''', '''Alt(t_1, t_2)''' (alternation), '''Rule(r)''', '''Seq(t_1, t_2)''' (sequential application), '''Repeat(t)''' (repeatedly apply '''t''' until it fails, and then succeed). The strategy from S4 says ``repeatedly apply the first applicable rule from the left until none are applicable, and then apply the S4 rule, and repeat this process until no rules are applicable''. This strategy is applied to every branch of the proof tree according to the visit algorithm. More Formally: * Skip: t = Skip : t always succeeds * Fail: t = Fail : t always fails * Rule: t = Rule(r) : t succeeds when rule r is applicable. * AndThen: t = t_1 ; t_2 : t fails if either t_1 or t_2 fail, succeeds otherwise. * OrElse: t = t_1 | t_2 : t fails if both t_1 and t_2 fail, succeeds otherwise. * Repeat: Repeat(t) = mu(X) . (t ; X | Skip) : If tactic t succeeds, the tactic Repeat(t) behaves like t ; Repeat(t). If t fails, then the tactic Repeat(t) behaves like Skip. The strategy Repeat always succeeds and is usually written and (t*).