In this section we give a tableau calculus for the logic '''KT'''.
The logic KT is obtained by adding the axiom []A -> A to the standard Hilbert calculus
for K. Semanticall it is characterised by Kripke frames where the reachability relation R
is reflexive: that is, every world is reachable from itself.

```
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
```