The Tableau WorkBench (TWB)

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