===Using || for K Rule===
In [[k_ml_tableau_prover_normal_modal_logic_k]] we specified the '''K''' rule using s single line and hence implicit backtracking. Now we specify the same rule by making the backtracking explicit. The '''K''' rule can also be written as follows:

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