The Tableau WorkBench (TWB)

The TWB has the infrastructure to add histories and variables to tableau/sequent rules. Operationally, a history or a variable is an object that must be instantiated by the user when defining a logic module.

The TWB library defines the interface for such objects in terms of an Ocaml functor. The TWB data types library defines three generic data structures that can be assembled by the user to define complex histories or variables. The three basic functors to build such data structures are:

• TwbSet.Make ( ElementTYPE ) : defines a set of elements of type ElementTYPE
• TwbMSet.Make ( ElementTYPE ) : defines a multi set of elements of type ElementTYPE
• TwbList.Make ( ElementTYPE ) : defines a list of elements of type ElementTYPE

A functor is a function that given a module of type ElementTYPE returns a module of type TwbSet.S . The ElementTYPE type module has the follwing signature:


module type ValType =
    sig
        type t
        val copy : t -> t
        val to_string : t -> string
    end


For example, if we want to add a history of type set of formulae we need to define a module FormulaSet by using the functor TwbSet.Make and passing to it the type formula as ElementTYPE as shown below.


module FormulaSet = TwbSet.Make(
    struct
        type t = formula
        let to_string = formula_printer
        let copy s = s
    end
)


Once the module is defined, we add it to the tableau/sequent node by using the following syntax. The keyword HISTORIES expects a sequence of history declarations. Each such declaration consists of three elements. The first element is an uppercase identifier (e.g. BOXES) naming the history used in the tableau rules, followed by a colon. The second element is the type of the history (e.g FormulaSet.Set) , followed by an := operator. The third element is the default value for the history (e.g. a new empty object of type FormulaSet.set).


HISTORIES
  BOXES    : FormulaSet.set := new FormulaSet.set
END


Variables are declared similarly with the following syntax. The only difference is that the identifier used for variables is always lowercase. 
VARIABLES
  var1    : FormulaSet.set := new FormulaSet.set
END