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.