s4.ml: Modal Logic S4 Using Histories

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.