(*
Prover for modal logic KD45.
Based on: Efficient Loop-Check for KD45 Logic
A Birstunas
Lithuanian Mathematics Journal 46(1):44-53 2006.
Author: Rajeev Gore 01 November 2007.
Logic KD45 is built from basic normal modal logic K by adding
the following extra axioms:
D = []p -> <>p which forces R to be serial or total
4 = []p -> [][]p which forces R to be transitive
5 = <>p -> []<>p which forces R to be euclidean.
It is often used as a logic for agents where:
[]p means "the agent believes p"
or
[]p means "the agent knows p".
Histories:
DIAS: accummulates diamond formulae so we can identify new ones
BOXS: accummulates box formulae so we can identify new ones
Inv 1: For every node N, both DIAS and BOXS are subsets of N.
Proof: no rule deletes diamond formulae or box formulae.
Inv 2: The sets DIAS and BOXS grow monotonically down a branch.
Proof: rules only add formulae to these histories.
Termination: Eventually, no new boxes or diamonds appear so
the side condition to the KD45Birstinas rule will evaluate to
false and this rule is not applicable.
Functions:
somethingnew(l, s)
returns true if list l contains an element
which is not in set s. The pre-defined function
is_in(xl, ys) checks whether the singleton list xl is in
the set ys. For each member h of l, we construct the
singleton list [h] and use is_in([h], s) to check whether
h is in the set s. We return true as soon as we find an
h that is not in s.
newdiamondorboxfound(diaa, diax, bxy, dias, boxs)
returns true if diaa or diax contain an element which is
not in dias or bxy contains an element which is not in boxs.
KD45Birstunas Rule:
This rule is taken directly from the paper mentioned above except
that the principal formula <>A is enclosed in parentheses i.e.
( <> A ) rather than braces i.e. { <> A }. The parentheses are understood
by the TWB to mean "the principal formula may be missing". But if
<> A is missing then <> X must be empty too so this rule creates a
successor even when there are no diamonds as required by Birstunas.
*)
CONNECTIVES [ "~";"&";"v";"->";"<->";"<>";"[]" ]
GRAMMAR
formula :=
ATOM | Verum | Falsum
| formula & formula
| formula v formula
| formula -> formula
| formula <-> formula
| [] formula
| <> formula
| ~ formula
;;
expr := formula ;;
END
module FormulaSet = TwbSet.Make(
struct
type t = formula
let to_string = formula_printer
let copy s = s
end
)
HISTORIES
DIAS : FormulaSet.set := new FormulaSet.set;
BOXS : FormulaSet.set := new FormulaSet.set
END
open Twblib
open Kd45Birstunaslib
let rec somethingnew(l, s) = match l with
[] -> false
| h::t -> if isin([h], s) then somethingnew(t, s) else true
;;
let newDiamondOrBoxFound(diaa, diax, bxy, dias, boxs) =
somethingnew(diaa, dias)
|| somethingnew(diax, dias)
|| somethingnew(bxy, boxs)
;;
TABLEAU
RULE KD45Birstunas
( <> A ) ; <> X ; [] Y ; Z
---------------------------------
A ; <> A ; <> X ; Y ; [] Y
COND [ newDiamondOrBoxFound(<> A, <> X, [] Y, DIAS, BOXS) ]
ACTION [ DIAS := add(<> A, DIAS);
DIAS := add(<> X, DIAS);
BOXS := add([] Y, BOXS) ]
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!Or) )
in tactic ( ( sat ! KD45Birstunas )* )
PP := List.map nnf
NEG := List.map neg
MAIN