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

TwbSet API


class type ['basetype] twbset =
    object('typesettype)
        method add : 'basetype -> 'typesettype
        method add_filter : ('basetype -> 'basetype -> bool ) -> 'basetype -> 'typesettype
        method addlist : 'basetype list -> 'typesettype
        method del : 'basetype -> 'typesettype
        method mem : 'basetype -> bool
        method elements : 'basetype list
        method hd : 'basetype
        method is_empty : bool
        method filter : ('basetype -> bool) -> 'typesettype
        method length : int
        method cardinal : int
        method intersect : 'typesettype -> 'typesettype
        method union: 'typesettype -> 'typesettype
        method subset: 'typesettype -> bool
        method is_equal : 'typesettype -> bool
        method copy : 'typesettype
        method empty : 'typesettype
        method to_string : string
    end

The TwbSet API is parametrized in the its input type. In the following let ''' 'basetype ''' be the base type (eg. a formula or a Formula.set ) and ''' 'twbsettype ''' the resulting type TwbSet.set . We now explain all methods * method add : 'basetype -> 'typesettype : add en element of type 'basetype to the object and return the modified object. Example:


(* add : (formula list * Formula.set) -> Formula.set *)
let add (l,h) = h#addlist l

* method add_filter : ('basetype -> 'basetype -> bool ) -> 'basetype -> 'typesettype * method addlist : 'basetype list -> 'typesettype : add a list of elements * method del : 'basetype -> 'typesettype : remove one element * method mem : 'basetype -> bool : check if an element is present * method elements : 'basetype list : return the list of element in the object * method hd : 'basetype : return an element of the object. If the data type is implemented as a list, then it returns the first element of the list, otherwise it returns an unspecified element of the collection. * method is_empty : bool : check if the object is empty * method filter : ('basetype -> bool) -> 'typesettype * method length : int : returns the cardinality of the object * method cardinal : int : same as ''length'' * method intersect : 'typesettype -> 'typesettype * method union: 'typesettype -> 'typesettype * method subset: 'typesettype -> bool * method is_equal : 'typesettype -> bool * method copy : 'typesettype : return a deep copy of the object * method empty : 'typesettype : return an empty instance of the object * method to_string : string : return a string containing the human readable representation of the object