k.ml: A Tableau Prover for Normal Modal Logic K

In this section we analyze two variants of a simple tableau calculus for mono-modal logic K. We use this example to explain various parts of the TWB tableau language in detail. ==Modal Logic K== The normal modal logic K (for Kripke) is the simplest normal modal extension of classical logic. In addition to the usual connectives from classical propositional logic, it contains two unary connectives which originally were intended to capture the notions of Necessary and Possibility. The connectives are usually called "box" and "diamond" nowadays and are often written as [] and <> respectively. The intended semantics of []A is that "A is necessary" and that of <>A is that "A is possible". These connectives are negation duals in that []A can be defined as ~ <> ~ A and <>A can be defined as ~ [] ~ A. Thus we can extend negation normal form to modal logic K simply by pushing negations inwards using these definitions. More precisely, we transform ~ [] A to <> ~ A and transform ~ <> A to [] ~ A (and then transform ~ A recursively). ==A simple tableau for K== 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 )* )

k.ml: explicit branching

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