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;