```
N
-----------
d1 ... dn
```

where N
is the numerator, while ''d1 ... dn'' is a list of n denominators.
The numerator contains one or more distinguished formula schemas
called ''principal formulae'' and one or more formulae schema called
''side formulae''. We use meta-variables '''A, B, P, Q, ... ''' to
represent principal formulae and '''X,Y,Z''' for, possibly empty,
"containers" of side formulae: traditionally sets, multisets or
sequences, but possibly more complex data structures for generality.
Operationally, tableau rules can be seen as functions to transform a
(container) node into a list of (container) nodes during the
construction of a graph. We say that a rule is ''applicable'' if we
can ''partition'' the contents of the current node to instantiate
the meta-variables in the numerator .
The ''denominators'' of a rule represent actions to expand the graph by
creating new nodes according to these instantiations.
The repeated application of rules gives rise to a tree of nodes, with
children obtained from their parent by instantiating a rule. To
capture sequent calculi as well as tableau calculi, we view this
process as a search for a proof where all leaves are "closed". But
in general, for tableau calculi with cyclic proofs, there are really
three notions: ''success'', ''failure'' and ''undetermined'': we
stay with the dichotomy "closed" as success (of proof search) and
"open" as failure (of proof search) for now to simplify the
exposition.
A numerator pattern like '''Z''' is ''unrestricted'' since its shape
does not restrict its contents in any way. Conversely, the pattern
'''Box X''' is restricted to contain only Box-formulae, '''X &Y''' is
restricted to contain only &-formulae while '''{A & B}''' is
restricted to contain exactly one single &-formula. Patterns
like '''X & Y''' are allowed to be empty, but '''{A & B}''' is not.
Currently, we forbid purely structural numerators like '''X;Y''' which
non-determ-inistically partition the node '''N''' into two arbitrary
disjoint containers '''X''' and '''Y''' (even though such numerators may be
useful for linear logic), and numerators like '''Box X ; Box Y; Z'''
since both can lead to an exponential number of possible different
partitions.
Consequently, the ''only'' form of non-determinism in rules
is the ''formula choice'' non-determinism in
choosing the principal formula.
More generally called ''instance choice'', this non-determinism
leads to ''implicit branching'' since the choice-point is hidden in
the pattern-matching (rule instance). We return to this issue later
after identifying the various forms of non-determinism inherent in
tableau proof search.
```
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
```

```
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
```
STRATEGY := tactic ( (Id ! False ! And ! Or ! K)* )
```

Or alternatively:
```
STRATEGY :=
let sat = tactic ( (Id ! False ! And ! Or) ) in
tactic ( ((sat)* ; K )* )
```

The strategy says ``repeatedly apply the first applicable rule from the left until none are applicable, and then apply the '''K''' rule, and repeat this process until no rules are applicable''. This strategy is applied to every branch of the proof tree according to the visit algorithm.
More Formally:
'''t_1''' and '''t_2''' are tactics (terms built from this language) and '''r''' is a rule: '''Fail''', '''Skip''', '''Alt(t_1, t_2)''' (alternation), '''Rule(r)''', '''Seq(t_1, t_2)''' (sequential application), '''Repeat(t)''' (repeatedly apply '''t''' until it fails, and then succeed).
* Skip: t = Skip : t always succeeds
* Fail: t = Fail : t always fails
* Rule: t = Rule(r) : t succeeds when rule r is applicable.
* AndThen: t = t_1 ; t_2 : t fails if either t_1 or t_2 fail, succeeds otherwise.
* OrElse: t = t_1 | t_2 : t fails if both t_1 and t_2 fail, succeeds otherwise.
* Repeat: Repeat(t) = mu(X) . (t ; X | Skip) : If tactic t succeeds, the tactic Repeat(t) behaves like t ; Repeat(t). If t fails, then the tactic Repeat(t) behaves like Skip. The strategy Repeat always succeeds and is usually written and (t*).```
$./twbcompile pc.ml
............Done.
$
```

The result of the compilation is the file '''pc.twb''' that is the object prover for propositional classical logic.
===Running .twb files===
To run the file '''pc.twb''' we can either give it a file of formulae to prove as argument or passing a formula
on the stdin channel.
We show the proof trace of a simple tautology `~ (~ p) <-> p`

:
```
$./pc.twb --trace
~ (~ p) <-> p
Proving: ~ (~ p) <-> p
Start Node: ((p & (~ p)) v (p & (~ p)))
Or ( 0 -> 1 )
(p & (~ p)) ;
And ( 1 -> 2 )
(~ p) ; p
Id ( 2 -> 3 )
Or ( 0 -> 4 )
(p & (~ p)) ;
And ( 4 -> 5 )
(~ p) ; p
Id ( 5 -> 6 )
Time:0.0000
Result:Close
Total Rules applications:6
```

''''Note that the initial formula is immediately transformed into
negated normal form before being processed by the tableau
rules.''''
====Command Line Options====
Provers generated with the TWB have a number of standard options to switch on/off different
behaviors. In particular, for the moment we concentrate on just a few of the options :
* ''--noneg'' is the runtime option to switch off the negation of the input formula. This is useful when
the prover is used as a satisfiability procedure. The same effect is obtained by not specifying
a value for the NEG function in the logic module source.
* ''--nopp'' disables the preprocessing function. In our example, the negation normal form function nnf
is the pre-processing function PP.
* ''--trace'' enables a rule by rule trace of the proof. By default the twb outputs only the outcome of the proof. By tracing the proof it
is possible to do a step by step analysis of the proof. Useful for debugging.
* ''--verbose'' displays additional information
```
$./pc.twb --help
usage: ./pc.twb [-options] [file]
--nopp disable preproc function
--noneg disable negation function
--level trace level
--trace print proof trace
--time set exec timeout
--verbose print additional information
--outdir set output directory
--out set output type
--nocache disable function memoization
-help Display this list of options
--help Display this list of options
```

```
CONNECTIVES [ "~";"&";"v";"->";"<->" ]
```

The keyword '''CONNECTIVES''' in the TWB introduces a list of string separated with a simicolon ";".
Each string can be used as a connective in the grammar definition (below) and it will become a reserved keyword.
Connectives can be of variable length, can be composed by a mix of numbers, symbols and characters.
====Restrictions====
* The backslash symbol "\" cannot be used.
* The symbol vertical bar "|" cannot be used.
* Double semicolon ";;" cannot be used.
* The string "ATOM" cannot be used.
* The symbols "(", ")", "{" , "}" cannot be used.
===Grammar===
```
GRAMMAR
formula :=
ATOM | Verum | Falsum
| formula & formula
| formula v formula
| formula -> formula
| formula <-> formula
| ~ formula
;;
expr := formula ;;
END
```

The TWB allows the user to define the grammar to be used for the formulae in the tableau/sequent rules.
A TWB grammar is composed of a sequence of productions separated by a double semicolon ";;". Two
mandatory productions are ''formula'' and ''expr''. A third pre-defined production that can be omitted is ''node''.
* node: this production defines the shape of a tableau/sequent node. By default, a tableau node is composed of a set of formulae.
* expr: this production defines the outer most expressions used in the definition of tableau rules. Generally an expression is just a formula. In more complicated tableau rules, an expression can be a formula decorated with a label or with another arbitrary data structure.
* formula : this production defines the shape of the formula definition to be used in the tableau rules.
====Conventions====
* Lower case identifier in a production are interpreted as a grammar identifier for a production.
* Upper case identifiers are interpreted as constants (eg. Verum and Falsum).
* The keyword '''ATOM''' identifies an atom in the grammar.
====Restrictions====
The grammar accepted by the TWB is a loose LL(1) grammar. Conflicts are not handled automatically and the definition
of ambiguous grammars can lead to unspecified results.
====NOTA BENE====
At the moment of writing the grammar machinery still has some minor bugs that we
are seeking to address in future releases.
===OCaml Code ===
```
open Twblib
open Pclib
```

Since the TWB is built on top of ocaml, it is possible to specify arbitrary ocaml functions with a twb file.
In this example, we use twb modules by using the ocaml directive ''open''. This operation imports into
the current namespace all the functions and data types defined in the module "twblib.ml" and "pclib.ml".
Note that the leading lowercase letter of the file name is capitalised when using the "open" directive.
In general, it is possible to write arbitrary functions and data types that can be used in the subsequent part of file.
===Tableau Definition===
```
TABLEAU
RULE Id { a } ; { ~ a } ; X === Close END
RULE False { Falsum} ; X === Close END
RULE And { A & B } ; X === A ; B ; X END
RULE Or { A v B } ; X === A ; X | B ; X END
END
```

A tableau definition is delimited of the keywords '''TABLEAU ... END'''.
A tableau is composed of a sequence of
rule definitions. A rule is delimited by the keywords '''RULE ... END''' .
In general, tableau/sequent rules may consist of up to seven components:
*Numerator: The numerator is a list of formula schemas separated by semicolons and specifies a partition of the current node in the proof tree. Formulae schemas are parsed according to the connectives declared in the connectives section with principal formulae enclosed in braces { }. A pattern is ''restricted'' if it is specified by a formula schema containing connectives like A -> B and Box A. A pattern is {\em unrestricted} if it is specified by just a meta-variable like X. There may be many ways of partitioning a node to match the pattern specified by the numerator leading to implicit choice-points.
* Separator: A rule commits to the first numerator pattern choice if the separator between the numerator and denominators is a sequence of at least two "='' symbols. A rule backtracks over the different pattern choice-points if the separator is a sequence of at least two ``-'' symbols and the current partition choice does not close. Intuitively, a rule that commits is declared to be invertible and a rule that does not commit is declared to be non-invertible. However, the TWB does not check that the rule is really invertible. It assumes that the user has proved an inversion lemma independently.
* Denominator: In general, a rule can have a list of denominators related by a branching operator. Each denominator is a list of formula schemas and specifies how to construct the root nodes of the branches that extend the tableau using the patterns assigned to the meta-variables in the numerator. The (universal) branch separator | is an instruction to close the current node if ''every'' denominator closes. The (existential) branch separator || is an instruction to close the current node if ''some'' denominator closes. These are actually instances of conditional branching which are instructions to close the current node if the denominators meet a specified condition.
* Cond: A rule is applicable if the side-conditions are satisfied as specified using the COND construct. If all the side conditions are true, then the tentative partition is accepted. Otherwise the partition is not considered and the pattern matching algorithm proceeds until a successful partition is found.
* Action: If the rule is applicable then the ACTION construct specifies actions on the current histories or variables to compute the histories of the children.
* Branch: Conversely, branch conditions, specified by the keyword BRANCH, are executed on backtracking to check whether to explore the next branch (if there is one) or to backtrack further. It is possible to specify a list of branch conditions, one for every branch and each set of branch conditions will have access to all variables returned by any branch already explored. An attempt to access a variable related to a branch yet to be visit will generate a run-time error.
* Backtrack: Specifies how to synthesize the result for the current node from the results of the children.
====We now analyze each rule definition:====
```
RULE False
{ Falsum } ; X
=======================
Close
END
```

This rule define an axiom. The rule is introduced by the keyword '''RULE''', it is the followed by an uppercase rule
identifier ''False'' that will be used to invoke the rule in the strategy section. The body of the rule is a schema
representing a tableau / sequent node as defined in the grammar. In this case a tableau node is a set of formulae
separated by a semicolon ";". In this case, for the rule to be applicable, the node schema requires a principal formula
containing the constant '''Falsum''' and an anonymous, possibly empty, set of formulae '''X''' that contains all other formulae
in the node.
If the rule is applicable, then this particular rule stops the procedure by using the keyword '''Close'''. Intuitively this rule is
a device to stop the procedure whenever we find an instance of bottom (Falsum) in the tableau node.
```
RULE Id
{ a } ; { ~ a } ; X
=========================
Close
END
```

The rule above defines the axiom '''Id''' that detects classical inconsistencies, that is a positive and a negative occurrence of an
atom in a tableau node. The body of this rule has two principal formulae and a anonymous set X. This rule elucidates two important
features of the pattern matching machinery of the TWB. First we notice that we used lower case to identify the schemas
`{ a } ; { ~ a }`

. In the pattern definitions, lowercase always match atoms, while uppercase match both atoms and
formulae. In this instance we want to restrict the application of the rule Id only to atoms. Secondly, when the same identifier is used
more then once in the definition of a formula schema, the TWB machinery will try to unify it with other occurrences. In this case the rule
will be applicable if and only if, the atom '''a''' occurs both positively and in the formula '''~ a''' .
```
RULE And
{ A & B } ; X
=======================
A ; B ; X
END
```

The rule '''And''' is a rewriting rule. The body of the rule is composed by a principal formula and an anonymous set.
If there is at least one formula in the current tableau node containing a conjunction (eg. a & b), then the rule is applicable.
Then the denominator of the rule, breaks down the conjunction into its conjuncts and copies across all the other formulae in
the node untouched.
====Note====
Even if it is always possible to specify the anonymous set in the rule schemas, this is not recommended. The default of the TWB is to
leave untouched all formulae that are not explicitly manipulated by a rule application. The previous rule could have also been written as
```
RULE And { A & B } === A ; B END
```

and we will often use this formulation in the remainder of this tutorial.
-------------
EXERCISE: how does the following rule differ operationally from the And rule above?
```
RULE And A & B === A ; B END
```

ANSWER:
In the first case, the rule will choose one single &-formula as principal formula.
In the second case all &-formulae will be chosen at once in one rule application.
But note that the subformula (d & e) below is not touched because it is not at the
top-level in node 1.
```
#echo "(a & b) & (c & (d & e)) " | ./pc.twb --trace --noneg
And ( 0 -> 1 )
(a & b) ; (c & (d & e))
And ( 1 -> 2 )
a ; b ; c ; d & e ;
Time:0.0000
Result:Open
Total Rules applications:2
```

--------------------------
```
RULE Or
{ A v B }
======================
A | B
END
```

First note, that there is no ancillary X in the numerator or denominator in keeping with the just mentioned note which allows us to assume that all other formulae in the node are left untouched.
The '''Or''' rule matches a disjunction and creates two new branches that will be explored by the tableau procedure. The semantics of the
Or rule requires both branches to be closed, for the tableau rooted at the current node to be closed. This semantics is enforced by using the
single bar "|" as the separator between two branches. In particular, the single bar imposes a condition on backtracking whether to explore the
next branch or not. To understand how the TWB works in this instance we need to introduce the notion of visit more in details. By default, the
TWB uses a left-to-right depth-first visiting strategy. When the strategy is invoked with the current node, first an applicable rule is selected, then
the rule is applied and the strategy is re-invoked on all branches that result from the rule application. On backtrack, that is, when the visit function
returns from the visit of a branch, a branching condition is checked to decide whether to explore the next branch. In this particular instance
the visit condition will check if the visit of the first branch lead to a closed tableau. If this is the case, the second branch is explored. Otherwise
a result of an open branch is immediately returned.
EXERCISE: Consider the variant Or-rule below:
```
RULE Or-wrong
A v B
======================
A | B
END
```

How does it differ from the previous Or-rule, and more importantly, is it semantically sound given our
usual interpretation of the classical disjunction?
===Strategy===
` STRATEGY := tactic ( (Id ! False ! And ! Or)* ) `

===Operators===
```
PP := List.map nnf
NEG := List.map neg
MAIN
```

The '''PP''' directive defines a PreProcessor as indicated by the function to the right of the := sign.
If '''PP''' is defined then the TWB first uses this preprocessor on all input formulae.
The '''NEG''' directive defines a NEGation function as indicated by the function to the right of the := sign.
By default, the TWB NEGates all input formulae using this function.
The preprocessor '''PP''' is invoked ''*after*'' the NEGation function so the directives in this case tell the TWB to NEGate all inputs, and then put the result into nnf by pushing negations down to atomic level.
The MAIN directive just tells the TWB to link the default command line application to the prover. In principle it would be possible to specify different routine, for example to run the prover as a cgi from the web. This is still work in progress.
```
CONNECTIVES [ "~" ; "&" ; "v" ; "->" ; "<->" ; "=>"]
GRAMMAR
formula :=
ATOM | Verum | Falsum
| formula & formula
| formula v formula
| formula -> formula
| formula <-> formula
| ~ formula
;;
expr := formula ;;
node := set => set ;;
END
SEQUENT
RULE Id Close === { A } => { A } END
RULE False Close === { Falsum } => END
RULE True Close === => { Verum } END
RULE AndL A ; B => === { A & B } => END
RULE AndR => A | => B === => { A & B } END
RULE OrL A => | B => === { A v B } => END
RULE OrR => A ; B === => { A v B } END
RULE NegR A => === => { ~ A } END
RULE NegL => A === { ~ A } => END
RULE ImpL => A | B => === { A -> B } => END
RULE ImpR A => B === => { A -> B } END
RULE IffL (A -> B) & (B -> A) => === { A <-> B } => END
RULE IffR => (A -> B) & (B -> A) === => { A <-> B } END
END
let exit = function
|"Open" -> "Not Derivable"
|"Close" -> "Derivable"
|s -> assert(false)
EXIT := exit(status@1)
STRATEGY := tactic ( ( Id
! True ! False
! NegL ! NegR
! AndL ! AndR
! ImpL ! ImpR
! OrL ! OrR
! IffL ! IffR )* )
MAIN
```

```
source Pc
let neg = function formula ( a ) -> formula ( ~ a )
let rec nnf = function
|formula ( a & b ) -> formula ( {nnf a} & {nnf b} )
|formula ( ~ ( a & b ) ) ->
formula ( {nnf formula ( ~ a )} v {nnf formula ( ~ b )} )
|formula ( a v b ) -> formula ({nnf a} v {nnf b})
|formula ( ~ ( a v b ) ) ->
formula ( {nnf formula ( ~ a )} & {nnf formula ( ~ b )} )
|formula ( a <-> b ) ->
formula ( {nnf formula ( a -> b )} & {nnf formula ( b -> a )} )
|formula ( ~ ( a <-> b ) ) ->
formula ( {nnf formula ( ~ (a -> b) )} v {nnf formula ( ~ (b -> a) )} )
|formula ( a -> b ) -> nnf formula ( (~ a) v b )
|formula ( ~ (a -> b) ) -> nnf formula ( a & (~ b) )
|formula ( ~ ~ a ) -> nnf a
|formula (Verum) -> formula (Verum)
|formula (Falsum) -> formula (Falsum)
|formula (~ Verum) -> formula (Falsum)
|formula (~ Falsum) -> formula (Verum)
|formula ( ~ A ) as f -> f
| _ as f -> f
```

We assume this function to be in a file pclib.ml. The file is then included in the the main logic module by
using the directive `Open Pclib`

.```
CONNECTIVES [ "~";"&";"v";"->";"<->";"<>";"[]" ]
GRAMMAR
formula :=
ATOM | Verum | Falsum
| formula & formula | formula v formula
| formula -> formula | formula <-> formula
| [] formula | <> formula
| ~ formula
;;
expr := formula ;;
END
open Twblib
open Klib
TABLEAU
RULE K
{ <> A } ; [] X ; Z
--------------------
A ; X
END
RULE Id { a } ; { ~ a } === Close END
RULE False Falsum === Close END
RULE And { A & B } === A ; B END
RULE Or { A v B } === A | B END
END
STRATEGY := tactic ( (Id ! False ! And ! Or ! K)* )
PP := List.map nnf
NEG := List.map neg
MAIN
```

We focus on the definition of the '''K''' rule. Details regarding the propositional part of the tableau can be seen in [[pc_ml]].
```
RULE K
{ <> A } ; [] X ; Z
---------------------------------
A ; X
END
```

The '''K''' rule body is composed by a principal formula, a possibly empty set of box formulae '''[]X''' and an anonymous set '''Z'''.
Note that the K rule is written with a single line "----------" instead of a double line. Intuitively the single lines set an existential backtracking point.
In section [[rule_backtrack]] we explain in details the three types of backtracking that are allowed in the TWB. For the moment we focus on the semantic of the '''K''' rule. The numerator of the rule selects one principal formula, namely '''<> A'''. all other occurrences of <>-formulae are matched by the anonymous set '''Z''' . Since the set '''Z''' is not copied in the denominator (the '''K''' rule is not-invertible) once the choice is made, all other diamonds in the set '''Z''' will be lost. The single line "---------" set a backtracking point in case the choice of a particular diamonds didn't lead to a closed tableau. That is, imagine we the current node is composed by "<> a & <> b & [] ~ a". Then choosing <> a first will erroneously lead to an open tableau. But choosing <> b first will give a closed tableau. The TWB will backtrack over the choices of <>-formulae to avoid this problem.
====Example====
```
echo "<> b & <> a & [] ~ a" | ./k.twb --trace --noneg
And ( 0 -> 1 )
([ ] (~ a)) ; ((<> b) & (<> a))
And ( 1 -> 2 )
(<> a) ; (<> b) ; ([ ] (~ a))
K ( 2 -> 3 )
a ; (~ a)
Id ( 3 -> 4 )
Time:0.0000
Result:Close
Total Rules applications:4
```

===Strategy===
The strategy specifies the order in which rules are applied during proof search. In our example, for completeness, we need to apply all classical rule first and then the K rule. The bang '''!''' operator applies the first rule that is applicable. The star '''*''' iterates until one rule is applicable. Since the K rule is the last rule, this means that all the other rules are not applicable.
` STRATEGY := tactic ( (Id ! False ! And ! Or ! K)* ) `

This strategy is equivalent to the following strategy:
```
STRATEGY :=
let sat = tactic ( (Id ! False ! And ! Or) ) in
tactic ( ((sat)* ; K )* )
```

```
RULE K
{ <> A } ; [] X ; <> Y ; Z
===========================
A ; X || <> Y ; [] X
END
```

The body of the '''K''' is composed of a principal formula, a possibly empty set of box formulae []X, a possibly empty set of diamond formulae <>Y and an anonymous set Z. Note that now because of the presence of the schema <>Y, the set Z is diamond-formulae free.
The denominator has two branches.
* '''A ; X''' encodes the modal jump
* '''<> Y ; [] X''' encodes a recursion step to consider all other diamonds if the first branch didn't lead to a closed tableau.
Note also that we now use the double line as the rule has been determinised and no backtrack is needed to recover from a wrong choice. Moreover the double bar '''||''' set an existential branching whose semantic is exactly as outlined before. The second branch is explored if and only if the result of the tableau rooted with the node '''A ; X''' is open.
This formulation gives more control over the recursion and allows the user ... HELP ...```
source K
module FormulaSet = TwbSet.Make(
struct
type t = formula
let to_string = formula_printer
let copy s = s
end
)
HISTORIES
BOXES : FormulaSet.set := new FormulaSet.set
END
open Twblib
open Klib
TABLEAU
RULE T
{ [] A }
=========
A ; [] A
COND notin(A, BOXES)
ACTION [ BOXES := add(A,BOXES) ]
END
RULE K { <> A } ; [] X ; Z ------- A ; X
ACTION [ BOXES := clear(BOXES) ]
END
RULE Id { a } ; { ~ a } === Close END
RULE False Falsum === Close END
RULE And { A & B } === A ; B END
RULE Or { A v B } === A | B END
END
STRATEGY :=
let sat = tactic ( (Id ! False ! And ! Or ! T) ) in
tactic ( ((sat)* ; K )* )
PP := List.map nnf
NEG := List.map neg
MAIN
```

===Step by step explanation===
The module for the logic KT does not begin with a CONNECTIVES and GRAMMAR specification, but we recycle the definition in the file ''k.ml'' using the directive ` source K `

. The effect of this directive is to import the grammar definitions.
Since the principal formula []A of the T rule is copied into the denominator, a naive tableau can give
rise to a loop, that is an infinite sequence of T-rule applications. To avoid this misbehavior we use a history. We first declare the ocaml object, then we make the history '''BOXES''' known to the TWB engine.
```
module FormulaSet = TwbSet.Make(
struct
type t = formula
let to_string = formula_printer
let copy s = s
end
)
HISTORIES
BOXES : FormulaSet.set := new FormulaSet.set
END
```

See [[defining_histories_and_variables]] for a more detailed explanation on how to declare histories and variables.
The tableau calculus for KT is similar to the tableau calculus for K explained in the section [[k_ml_tableau_prover_normal_modal_logic_k]] . Here we focus on the rule '''T''' and in particular on the use and manipulation of the history.
```
RULE T
{ [] A }
============
A ; [] A
COND notin(A, BOXES)
ACTION [ BOXES := add(A,BOXES) ]
END
```

The body of the rule T simply matches a principal formula '''[] A''' and adds
'''A ; [] A''' to the denominator leaving all other formulae in the node untouched. Obviously, since we copied the formula [] A back in the denominator, the same rule will be again applicable to it, leading to a loop.
To stop the loop from happening we put a side-condition on the application of the rule via
the COND declaration. The side-condition is true iff the formula A is not in the set BOXES.
If the side-condition is true, then the T-rule will be applied. We now need to record
that this []A has had the T-rule applied to it so we specify an ACTION to add the formula
'''A''' to the history '''BOXES''' (which is of type a set of formulae).
Thus we use the history '''BOXES''' to record all the box formulae that we have
already encountered and apply the T-rule only to previously unencountered []-formulae.
The action part is introduced by the keyword '''ACTION'''. An action is an operation to modify a history or it is an arbitrary function that does not return any value (actually that returns the ocaml type `unit`

). In our example we assigned the result of the ocaml function ''add()'' to the history '''BOXES'''.
The function ''add()'' is specified in the file ''twblib.ml'' that contains a number of common functions. In particular it is defined as follows:
```
(* add : (formula list * Formula.set) -> Formula.set *)
let add (l,h) = h#addlist l
```

See [[twbset_api]] for an overview of the methods of the class TwbSet.
Since the logic is reflexive, but not transitive, we must empty the '''BOXES''' history after each modal jump. This is done in the action section of the K rule.
```
RULE K
{ <> A } ; [] X ; Z
----------------------------------
A ; X
ACTION [ BOXES := clear(BOXES) ]
END
```

the function ''clear'' is defined as follows:
```
(* Formula.set -> Formula.set *)
let clear h = h#empty
```

```
source K
module FormulaSet = TwbSet.Make(
struct
type t = formula
let to_string = formula_printer
let copy s = s
end
)
HISTORIES
DIAMONDS : FormulaSet.set := new FormulaSet.set;
BOXES : FormulaSet.set := new FormulaSet.set
END
open Twblib
open Klib
TABLEAU
RULE S4
{ <> A } ; Z --- A ; BOXES
COND notin(<> A, DIAMONDS)
ACTION [ DIAMONDS := add(<> A,DIAMONDS) ]
END
RULE T
{ [] A } === A
COND notin(A, BOXES)
ACTION [
BOXES := add(A,BOXES);
DIAMONDS := emptyset(DIAMONDS)]
END
RULE Id { a } ; { ~ a } === Close END
RULE False Falsum === Close END
RULE And { A & B } === A ; B END
RULE Or { A v B } === A | B END
END
STRATEGY :=
let sat = tactic ( (False ! Id ! And ! T ! Or) )
in tactic ( ( (sat)* ; S4 )* )
PP := List.map nnf
NEG := List.map neg
MAIN
```

In particular the (T)-rule is applied to a principal formula '''[] P''' only if its sub-formula '''P''' is not in the history '''BOXES'''. If '''notin(P,BOXES)''' , the denominator is created from the current rule by deleting '''[] P''' and adding '''P'''. The formula '''P''' is added to the history '''BOXES''' and the diamond history
'''DIAMONDS''' is emptied.
```
RULE T
{ [] A }
========
A
COND notin(A, BOXES)
ACTION [
BOXES := add(A,BOXES);
DIAMONDS := emptyset(DIAMONDS)]
END
```

Since the Kripke models for the logic S4 are transitive, box formulae always accumulate. In the calculus, the (T)-rule is applied only if the immediate sub-formulae '''P''' of the box formula '''[] P''' under consideration is "new" (not present in the box history) in the branch, thus exploiting transitivity. Intuitively, if a box formula is new in a branch, we force the procedure "to recompute", by forgetting (empting '''DIAMONDS''') any information about the diamond formulae found so far.
```
RULE S4
{ <> A } ; Z
-----------------
A ; BOXES
COND notin(<> A, DIAMONDS)
ACTION [ DIAMONDS := add(<> A,DIAMONDS) ]
END
```

Similarly, the S4 rule is applied only if its diamond formula '''<> P''' is not present in the diamond history '''DIAMONDS'''. If '''notin(<>P,DIAMONDS)''', then the formula '''P''' and the content of the box history '''DIAMONDS''' is added to the denominator. The context '''Z''' is discarded and the formula '''<> P''' is the diamond history '''DIAMONDS'''. The box history '''BOXES''' is unchanged.
====Functions====
In particular, we use three functions to handle histories:
```
let add (l,h) = h#addlist l
let notin (l,h) = not(h#mem (List.hd l))
let emptyset h = h#empty
```

* '''notin(formula list, history)''': accepts a list of formulae and a history, and returns a boolean indicating if the list of formulae is in the history.
* '''add(formula list, history)''': accepts a list of formulae and a history object and returns the history object with the formula list added to it.
* '''emptyset(history)''': returns an empty history object.
====Note====
The rules described in this section assume a decision procedure that first applies all classical rules and the (T)-rule until they are no longer applicable; and then which applies the modal rule S4. Therefore, in the (S4)-rule, the set '''Z''' will consist of all diamond formulae in the node except '''<> P''' and literals only. In particular, since the (T)-rule removes all box formulae from the node and stores their immediate sub-formulae in the box history '''BOXES''', then the set '''Z''' will be box-free.