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