Add comments for CL rules

CoAlgLogics.ml

@@ -134,6 +134,44 @@ let mkRule_MultiModalKD sort bs sl =
         res := None;
         AllInOne rules
 
+
+(*
+    CoalitionLogic: tableau rules for satisfiability
+
+    Rule 1:
+
+     /\  n
+    /  \i=1 [C_i] a_i       n ≥ 0,
+  ——————————————————————    C_i pairwise disjoint
+     /\  n
+    /  \i=1  a_i
+
+    Rule 2:
+
+     /\ n                         /\ m
+    /  \i=1 [C_i] a_i  /\ <D> b  /  \j=1 <N> c_j    n,m ≥ 0
+  ————————————————————————————————————————————————  C_i pairwise disjoint
+     /\ n                         /\ m              all C_i ⊆ D
+    /  \i=1 a_i        /\    b   /  \j=1 c_j
+*)
+
+
+let mkRule_CL sort bs sl =
+  assert (List.length sl = 1); (* TODO: Why? *)
+  let s1 = List.hd sl in (* [s1] = List.hd sl *)
+  (*
+    mkRule_CL sort bs [s1]
+    = { (λ[bs1]. { ∀R.D
+      | <D> b ∈ bs
+      }
+      ∪ { (λ[bs1].{ [C_i]a_i ∈ bs | a_i ∈ bs1}
+          , [(s1, { a_i | i∈I })]
+          )
+        | {[C_i]a_i | i∈I} ⊆ bs,
+          C_i pairwise disjoint and I maximal
+        }
+  *)
+
 let mkRule_Choice sort bs sl =
   assert (List.length sl = 2);
   let dep bsl =
@@ -211,5 +249,6 @@ let mkRule_Fusion sort bs sl =
 let getExpandingFunctionProducer = function
   | MultiModalK -> mkRule_MultiModalK
   | MultiModalKD -> mkRule_MultiModalKD
+  | CoalitionLogic -> mkRule_CL
   | Choice -> mkRule_Choice
   | Fusion -> mkRule_Fusion