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