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