The Tableau WorkBench (TWB)

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