diff --git a/CoAlgLogics.ml b/CoAlgLogics.ml
index 561ca96063273a0adbbf98696e0eba5d3b1927d9..fb717227fea6dc42001b6a0c7c48aa7a77f89206 100644
--- a/CoAlgLogics.ml
+++ b/CoAlgLogics.ml
@@ -152,6 +152,54 @@ let subset (a: bset) (b: bset) : bool =
     bsetIter f a;
     !res && (bsetlen a < bsetlen b)
 
+let bsetFilter (a: bset) (f: CoAlgMisc.localFormula -> bool) : bset =
+    let res = bsetMake () in
+    bsetIter (fun form -> if (f form) then bsetAdd res form else ()) a;
+    res
+
+let bsetForall (a: bset) (f: CoAlgMisc.localFormula -> bool) : bool =
+    let res = ref (true) in
+    let helper formula =
+        if (f formula) then () else res := false
+    in
+    bsetIter helper a;
+    !res
+
+let bsetExists (a: bset) (f: CoAlgMisc.localFormula -> bool) : bool =
+    not (bsetForall a (fun x -> not (f x)))
+
+let elemArray (x: 'a) (arr: 'a array) =
+    let res = ref (false) in
+    let f y = if (x == y) then res := true else () in
+    Array.iter f arr;
+    !res
+
+let disjointAgents sort (a: CoAlgMisc.localFormula) (b: CoAlgMisc.localFormula) : bool =
+    assert (lfGetType sort a = EnforcesF || lfGetType sort a = AllowsF);
+    assert (lfGetType sort b = EnforcesF || lfGetType sort b = AllowsF);
+    let la = lfGetDestAg sort a in
+    let lb = lfGetDestAg sort b in
+    let res = ref (true) in
+    let f idx =
+        if (elemArray idx lb) then res := false
+        else ()
+    in
+    Array.iter f la;
+    !res
+
+
+(*
+let maxDisjoints (a: bset) : bset list =
+    let f formula acc =
+        let g cc acc' =
+            if (compatible cc formula)
+            then new bset with formula and cc and then prepend it to acc'
+        in
+        List.fold acc g acc
+    in
+    bsetFold a f [bsetMake ()]
+*)
+
 (*
     CoalitionLogic: tableau rules for satisfiability