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 )* )