The Tableau WorkBench (TWB)

We now give an implementation of a tableau calculus for the basic modal logic S4. We use a tableau version of the sequent calculus from Heuerding.

In the following we use two histories, DIAMONDS for the diamond history and BOXES for the box history. Intuitively, the diamond history contains certain diamond formulae found in the branch from the root to the current node. The box history contains all the boxes found in the branch from the root to the current node.

The modal tableau rules shown below are an adaptation of Heuerding's sequent rules. 

source K

module FormulaSet = TwbSet.Make(
    struct
        type t = formula
        let to_string = formula_printer
        let copy s = s
    end
)

HISTORIES
  DIAMONDS : FormulaSet.set := new FormulaSet.set;
  BOXES    : FormulaSet.set := new FormulaSet.set
END

open Twblib
open Klib

TABLEAU

  RULE S4
  { <> A } ; Z --- A ; BOXES
  COND notin(<> A, DIAMONDS)
  ACTION [ DIAMONDS := add(<> A,DIAMONDS) ]
  END

  RULE T
  { [] A } === A
  COND notin(A, BOXES)
  ACTION [
      BOXES    := add(A,BOXES);
      DIAMONDS := emptyset(DIAMONDS)]
  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 :=
    let sat = tactic ( (False ! Id ! And ! T ! Or) )
    in tactic ( ( (sat)* ; S4 )* )

PP := List.map nnf
NEG := List.map neg

MAIN


In particular the (T)-rule is applied to a principal formula [] P only if its sub-formula P is not in the history BOXES. If notin(P,BOXES) , the denominator is created from the current rule by deleting [] P and adding P. The formula P is added to the history BOXES and the diamond history DIAMONDS is emptied.


  RULE T
      { [] A } 
    ======== 
          A

     COND notin(A, BOXES)
     ACTION [
         BOXES    := add(A,BOXES);
         DIAMONDS := emptyset(DIAMONDS)]
  END


Since the Kripke models for the logic S4 are transitive, box formulae always accumulate. In the calculus, the (T)-rule is applied only if the immediate sub-formulae P of the box formula [] P under consideration is "new" (not present in the box history) in the branch, thus exploiting transitivity. Intuitively, if a box formula is new in a branch, we force the procedure "to recompute", by forgetting (empting DIAMONDS) any information about the diamond formulae found so far.


  RULE S4
     { <> A } ; Z 
      ----------------- 
        A ; BOXES

     COND notin(<> A, DIAMONDS)
     ACTION [ DIAMONDS := add(<> A,DIAMONDS) ]
  END


Similarly, the S4 rule is applied only if its diamond formula <> P is not present in the diamond history DIAMONDS. If notin(<>P,DIAMONDS), then the formula P and the content of the box history DIAMONDS is added to the denominator. The context Z is discarded and the formula <> P is the diamond history DIAMONDS. The box history BOXES is unchanged.

Functions

In particular, we use three functions to handle histories: 
   let add (l,h) = h#addlist l
   let notin (l,h) = not(h#mem (List.hd l))
   let emptyset h = h#empty


• notin(formula list, history): accepts a list of formulae and a history, and returns a boolean indicating if the list of formulae is in the history.
• add(formula list, history): accepts a list of formulae and a history object and returns the history object with the formula list added to it.
• emptyset(history): returns an empty history object.

Note

The rules described in this section assume a decision procedure that first applies all classical rules and the (T)-rule until they are no longer applicable; and then which applies the modal rule S4. Therefore, in the (S4)-rule, the set Z will consist of all diamond formulae in the node except <> P and literals only. In particular, since the (T)-rule removes all box formulae from the node and stores their immediate sub-formulae in the box history BOXES, then the set Z will be box-free.