+open List
+
+type predicate = string
+type ent = Alice | Bob | Carl
+type world = W1 | W2 | Hungry | Full
+type variable = string
+type term = Constant of ent | Var of variable
+type clause = Pred of predicate * term
+ | Eq of term * term
+ | Conj of clause * clause
+ | Neg of clause
+ | Poss of clause
+ | Ex of string * clause
+type assignment = (variable * ent) list
+type poss = world * assignment
+type infostate = poss list
+
+let rec referent (i:poss) (t:term):ent = match (i,t) with
+ (i, Constant e) -> e
+ | ((w,(v',a)::g), Var v) -> if 0 == compare v v' then a else referent (w,g) t
+ (* warning: no error checking *)
+
+let extension (w:world) (p:predicate) (e:ent) = match (w,p,e) with
+ _, "woman", Alice -> true
+ | _, "man", Bob -> true
+ | _, "man", Carl -> true
+ | Hungry, "hungry", Alice -> true
+ | _, "enter", Bob -> true
+ | _, "enter", Carl -> true
+ | _, "sit", Alice -> true
+ | _, "sit", Bob -> true
+ | W1, "closet", Alice -> true
+ | W1, "guilty", Bob -> true
+ | W2, "closet", Carl -> true
+ | W2, "guilty", Carl -> true
+ | _,_,_ -> false
+
+let domain = [Alice; Bob; Carl]
+
+let rec update (s:infostate) (c:clause) = match c with
+ Pred (p,t) -> filter (fun (w,g) -> extension w p (referent (w,g) t)) s
+ | Eq (t1, t2) -> filter (fun i -> (referent i t1) == (referent i t2)) s
+ | Conj (c1, c2) -> update (update s c1) c2
+ | Neg c -> filter (fun i -> update [i] c == []) s
+ | Poss c -> filter (fun i -> update s c != []) s
+ | Ex (v,c) -> concat (map (fun (a:ent) ->
+ update (map (fun (w,g) -> (w,(v,a)::g)) s) c)
+ domain)
+
+(* Basic examples *)
+let test1 = update [(W1,[])] (Ex ("x", (Pred ("man", Var "x"))))
+
+let test2 = update [(W1,[])] (Ex ("x", (Pred ("woman", Var "x"))))
+
+let test3 = update [(W1,[])]
+ (Ex ("x", (Ex ("y", (Conj (Pred ("man", (Var "x")),
+ Pred ("man", (Var "y"))))))))
+let test4 = update [(W1,[])] (Ex ("x", (Ex ("y", (Eq (Var "x", Var "y"))))))
+
+
+(* Alice isn't hungry. *)
+let test5 = update [(Hungry,[]);(Full,[])]
+ (Neg (Pred ("hungry", Constant Alice)))
+
+(* Alice isn't hungry. Alice might be hungry. *)
+let test6 = update [(Hungry,[]);(Full,[])]
+ (Conj (Neg (Pred ("hungry", Constant Alice)),
+ Poss (Pred ("hungry", Constant Alice))))
+
+(* Alice might be hungry. Alice isn't hungry. *)
+let test7 = update [(Hungry,[]);(Full,[])]
+ (Conj (Poss (Pred ("hungry", Constant Alice)),
+ Neg (Pred ("hungry", Constant Alice))))
+
+(* Someone^x entered. He_x sat. *)
+let test8 = update [(W1,[("x",Bob)])]
+ (Conj (Ex ("x", Pred ("enter", Var "x")),
+ Pred ("sit", Var "x")))
+
+(* He_x sat. Someone^x entered. *)
+let test9 = update [(W1,[("x",Bob)])]
+ (Conj (Pred ("sit", Var "x"),
+ Ex ("x", Pred ("enter", Var "x"))))
+
+(* Someone^x is in the closet. He_x might be guilty. *)
+let test10 = update [(W1,[]);(W2,[])]
+ (Conj (Ex ("x", Pred ("closet", Var "x")),
+ Poss (Pred ("guilty", Var "x"))))
+
+(* Someone^x is in the closet who_x might be guilty. *)
+let test11 = update [(W1,[]);(W2,[])]
+ (Ex ("x", Conj (Pred ("closet", Var "x"),
+ Poss (Pred ("guilty", Var "x")))))
+