Defining Histories and Variables

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