From f4e43751338df09a77996eaf2820e4785d2ed88e Mon Sep 17 00:00:00 2001
From: Christoph Egger <Christoph.Egger@fau.de>
Date: Wed, 27 Apr 2016 19:42:24 +0200
Subject: [PATCH] Add Monotone neighbourhood logic
---
src/coalg/coalg.ml | 1 +
src/lib/CoAlgLogics.ml | 101 +++++++++++++++++++++++++++++++++++++++++
src/lib/CoAlgMisc.ml | 4 +-
src/lib/CoAlgMisc.mli | 1 +
4 files changed, 106 insertions(+), 1 deletion(-)
diff --git a/src/coalg/coalg.ml b/src/coalg/coalg.ml
index c87a7b1..30f4ec3 100644
--- a/src/coalg/coalg.ml
+++ b/src/coalg/coalg.ml
@@ -49,6 +49,7 @@ let printUsage () =
print_endline " <task> in { sat print verify nnf prov (is »not.(sat ¬f)«) }";
print_endline " <functor> in { MultiModalK (or equivalently K)";
print_endline " MultiModalKD (or equivalently KD)";
+ print_endline " Monotone";
print_endline " CoalitionLogic (or equivalently CL)";
print_endline " Const id1 ... idn (or equivalently Constant id1 ... idn)";
print_endline " Id (or equivalently Identity)";
diff --git a/src/lib/CoAlgLogics.ml b/src/lib/CoAlgLogics.ml
index 853e5ae..ba65d2c 100644
--- a/src/lib/CoAlgLogics.ml
+++ b/src/lib/CoAlgLogics.ml
@@ -156,6 +156,106 @@ let mkRule_MultiModalKD sort bs defer sl : stateExpander =
lazylistFromList rules
+(** directly return a list of rules **)
+let mkRuleList_Monotone sort bs defer sl : rule list =
+ (* arguments:
+ sort: type of formulae in bs (needed to disambiguate hashing)
+ sl: sorts functor arguments, e.g. type of argument formulae
+ bs: tableau sequent consisting of modal atoms
+ (premiss, conjunctive set of formulae represented by hash values)
+ result: set R of (propagation function, rule conclusion) pairs
+ s.t. [ (premiss / conc) : (_, conc) \in R ] are all rules
+ applicable to premiss.
+ Propagation functions map unsatisfiable subsets of the
+ (union of all?) conclusion(s) to unsatisfiable subsets of
+ the premiss -- this is a hook for backjumping.
+ NB: propagating the whole premiss is always safe.
+ *)
+ assert (List.length sl = 1);
+ let refocusing = bsetCompare (bsetMakeRealEmpty ()) defer = 0 in
+ let dep f bsl = (* dependencies for formula f (f is a diamond) *)
+ assert (List.length bsl = 1); (* -+ *)
+ let bs1 = List.hd bsl in (* -+-> [bs1] := bsl *)
+ let res = bsetMake () in
+ bsetAdd res f;
+ let (role : int) = lfGetDest3 sort f in (* ♥R.? := f, ♥ ∈ {∃,∀} *)
+ let filterFkt f1 =
+ if lfGetType sort f1 = AxF && lfGetDest3 sort f1 = role
+ && bsetMem bs1 (lfGetDest1 sort f1)
+ then
+ (* if f1 = ∀R.C and C ∈ bs1 then res = res ∪ {∀R.C} *)
+ bsetAdd res f1
+ else ()
+ in
+ bsetIter filterFkt bs;
+ res
+ in
+ let getRules f acc =
+ if lfGetType sort f = ExF then (* f = ∃R.C,i.e. a diamond *)
+ let bs1base = bsetMake () in
+ let defer1base = bsetMakeRealEmpty () in
+ let nextf = (lfGetDest1 sort f) in
+ bsetAdd bs1base nextf; (* bs1 := { C } *)
+ if (refocusing && (lfGetDeferral sort nextf) != (Hashtbl.hash "ε")) ||
+ ((bsetMem defer f) && (lfGetDeferral sort f) = (lfGetDeferral sort nextf))
+ then
+ bsetAdd defer1base nextf
+ else ();
+ let (role : int) = lfGetDest3 sort f in (* role := R *)
+ let filterFkt f1 acc =
+ if lfGetType sort f1 = AxF && lfGetDest3 sort f1 = role then
+ let bs1 = bsetCopy bs1base in
+ let defer1 = bsetCopy defer1base in
+ (* if f1 = ∀R.D then bs1 = bs1 ∪ { D } *)
+ let nextf1 = (lfGetDest1 sort f1) in
+ bsetAdd bs1 nextf1;
+ if (refocusing && (lfGetDeferral sort nextf1) != (Hashtbl.hash "ε")) ||
+ ((bsetMem defer f1) && (lfGetDeferral sort f1) = (lfGetDeferral sort nextf1))
+ then
+ bsetAdd defer1 nextf1
+ else ();
+ let s1 = List.hd sl in (* [s1] := sl *)
+ let rle1 = (dep f, lazylistFromList [(s1, bs1, defer1)]) in
+ rle1::acc
+ else acc
+ in
+ let s1 = List.hd sl in (* [s1] := sl *)
+ let rle = (dep f, lazylistFromList [(s1, bs1base, defer1base)]) in
+ let fold = bsetFold filterFkt bs acc in (* bs1 := bs1 ∪ { D | some "∀R.D" ∈ bs } *)
+ rle::fold
+ else if lfGetType sort f = AxF then
+ let bs1 = bsetMake () in
+ let defer1 = bsetMakeRealEmpty () in
+ (* if f1 = ∀R.D then bs1 = bs1 ∪ { D } *)
+ let nextf1 = (lfGetDest1 sort f) in
+ bsetAdd bs1 nextf1;
+ if (refocusing && (lfGetDeferral sort nextf1) != (Hashtbl.hash "ε")) ||
+ ((bsetMem defer f) && (lfGetDeferral sort f) = (lfGetDeferral sort nextf1))
+ then
+ bsetAdd defer1 nextf1
+ else ();
+ let s1 = List.hd sl in (* [s1] := sl *)
+ let rle1 = (dep f, lazylistFromList [(s1, bs1, defer1)]) in
+ rle1::acc
+ else acc
+ in
+ (* effectively:
+ mkRule_MultiModalK sort bs [s1]
+ = { ( λ[bs1]. { ∃R.C } ∪ { ∀R.D
+ | ∀R.D ∈ bs, D ∈ bs1
+ , [(s1, {C}∪{D | "∀R.D" ∈ bs)]
+ )
+ | "∃R.C" ∈ bs
+ }
+ *)
+ bsetFold getRules bs []
+
+let mkRule_Monotone sort bs defer sl : stateExpander =
+ let rules = mkRuleList_Monotone sort bs defer sl in
+ lazylistFromList rules
+
+
+
(* CoalitionLogic: helper functions *)
(*val subset : bitset -> bitset -> bool*)
let bsetlen (a: bset) : int =
@@ -498,6 +598,7 @@ let mkRule_Fusion sort bs defer sl : stateExpander =
let getExpandingFunctionProducer = function
| MultiModalK -> mkRule_MultiModalK
| MultiModalKD -> mkRule_MultiModalKD
+ | Monotone -> mkRule_Monotone
| CoalitionLogic -> mkRule_CL
| GML -> mkRule_GML
| PML -> mkRule_PML
diff --git a/src/lib/CoAlgMisc.ml b/src/lib/CoAlgMisc.ml
index 3cae45e..0332f39 100644
--- a/src/lib/CoAlgMisc.ml
+++ b/src/lib/CoAlgMisc.ml
@@ -79,6 +79,7 @@ module NHt = Hashtbl.Make(
type functors =
| MultiModalK
| MultiModalKD
+ | Monotone
| CoalitionLogic
| GML
| PML
@@ -100,6 +101,7 @@ type functorName =
let unaryfunctor2name : (functorName*string) list =
[ (NPa MultiModalK , "MultiModalK")
; (NPa MultiModalKD , "MultiModalKD")
+ ; (NPa Monotone , "Monotone")
; (NPa GML , "GML")
; (NPa PML , "PML")
; (NPa CoalitionLogic , "CoalitionLogic")
@@ -944,7 +946,7 @@ let rec detClosure vars nomTbl hcF fset vset atset nomset s f =
detClosure_ nomTbl hcF fset vset atset nomset s f2
| C.HCEX (_, f1)
| C.HCAX (_, f1) ->
- if (func <> MultiModalK && func <> MultiModalKD)
+ if (func <> MultiModalK && func <> MultiModalKD && func <> Monotone)
|| List.length sortlst <> 1
then raise (C.CoAlgException "Ex/Ax-formula is used in wrong sort.")
else ();
diff --git a/src/lib/CoAlgMisc.mli b/src/lib/CoAlgMisc.mli
index 33a95f8..b93b94e 100644
--- a/src/lib/CoAlgMisc.mli
+++ b/src/lib/CoAlgMisc.mli
@@ -12,6 +12,7 @@
type functors =
| MultiModalK
| MultiModalKD
+ | Monotone
| CoalitionLogic
| GML
| PML
--
GitLab