kt.ml: Modal Logic KT Using Histories

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