The Tableau WorkBench (TWB)

In this section we give a tableau calculus for the logic KT.

The logic KT is obtained by adding the axiom []A -> A to the standard Hilbert calculus for K. Semanticall it is characterised by Kripke frames where the reachability relation R is reflexive: that is, every world is reachable from itself.


source K

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

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

open Twblib
open Klib

TABLEAU

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

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

  RULE K  { <> A } ; [] X ;  Z ------- A ; X
  ACTION [ BOXES := clear(BOXES) ]
  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 ( (Id ! False ! And ! Or ! T) ) in
    tactic ( ((sat)* ; K )* )

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

MAIN


Step by step explanation

The module for the logic KT does not begin with a CONNECTIVES and GRAMMAR specification, but we recycle the definition in the file k.ml using the directive source K. The effect of this directive is to import the grammar definitions.

Since the principal formula []A of the T rule is copied into the denominator, a naive tableau can give rise to a loop, that is an infinite sequence of T-rule applications. To avoid this misbehavior we use a history. We first declare the ocaml object, then we make the history BOXES known to the TWB engine. 
module FormulaSet = TwbSet.Make(
    struct
        type t = formula
        let to_string = formula_printer
        let copy s = s
    end
)

HISTORIES
BOXES    : FormulaSet.set := new FormulaSet.set
END
 See defining_histories_and_variables for a more detailed explanation on how to declare histories and variables.

The tableau calculus for KT is similar to the tableau calculus for K explained in the section k_ml_tableau_prover_normal_modal_logic_k . Here we focus on the rule T and in particular on the use and manipulation of the history.


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

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


The body of the rule T simply matches a principal formula [] A and adds A ; [] A to the denominator leaving all other formulae in the node untouched. Obviously, since we copied the formula [] A back in the denominator, the same rule will be again applicable to it, leading to a loop. To stop the loop from happening we put a side-condition on the application of the rule via the COND declaration. The side-condition is true iff the formula A is not in the set BOXES. If the side-condition is true, then the T-rule will be applied. We now need to record that this []A has had the T-rule applied to it so we specify an ACTION to add the formula A to the history BOXES (which is of type a set of formulae). Thus we use the history BOXES to record all the box formulae that we have already encountered and apply the T-rule only to previously unencountered []-formulae.

The action part is introduced by the keyword ACTION. An action is an operation to modify a history or it is an arbitrary function that does not return any value (actually that returns the ocaml type unit). In our example we assigned the result of the ocaml function add() to the history BOXES.

The function add() is specified in the file twblib.ml that contains a number of common functions. In particular it is defined as follows:


(* add : (formula list * Formula.set) -> Formula.set *)
let add (l,h) = h#addlist l


See twbset_api for an overview of the methods of the class TwbSet.

Since the logic is reflexive, but not transitive, we must empty the BOXES history after each modal jump. This is done in the action section of the K rule.


  RULE K  
      { <> A } ; [] X ;  Z 
      ---------------------------------- 
            A ; X
      ACTION [ BOXES := clear(BOXES) ]
  END


the function clear is defined as follows: 
(* Formula.set  -> Formula.set *)
let clear h = h#empty