added nnf and cleaned up some utils

1 files changed, 100 insertions, 35 deletions

diff --git a/src/datatypes.ml b/src/datatypes.ml
index cb712ec..dcf3246 100644
--- a/src/datatypes.ml
+++ b/src/datatypes.ml
@@ -1,4 +1,6 @@
-(* Data types useful for our theorem prover(s) *)
+(* -------------------------------------------------------------------------------------------------------------------- *)
+(* ----------------------------------- Data types useful for our theorem prover(s) ------------------------------------ *)
+(* -------------------------------------------------------------------------------------------------------------------- *)
 
 type proposition = (* logical proposition *)
   | True
@@ -12,8 +14,12 @@ type proposition = (* logical proposition *)
 
 type interpretation = (string * bool) list;; (* interpretation *)
 
+type substitution = (string * proposition) list;; (* allows us to substitute any proposition for any atomic literal *)
 
-(* Utility functions to deal with the data types *)
+
+(* -------------------------------------------------------------------------------------------------------------------- *)
+(* ----------------------------------------- Utility functions for debugging ------------------------------------------ *)
+(* -------------------------------------------------------------------------------------------------------------------- *)
 
 let rec string_of_prop = function
   | True -> "True"
@@ -25,6 +31,13 @@ let rec string_of_prop = function
   | Implies (p1, p2) -> "(" ^ (string_of_prop p1) ^ " → " ^ (string_of_prop p2) ^ ")"
   | Iff (p1, p2) -> "(" ^ (string_of_prop p1) ^ " ↔ " ^ (string_of_prop p2) ^ ")";;
 
+  let string_of_sub sub =
+    let rec stringify = function
+      | [] -> ""
+      | (s, value) :: [] -> "(" ^ s ^ ": " ^ (string_of_prop value) ^ ")"
+      | (s, value) :: tl -> "(" ^ s ^ ": " ^ (string_of_prop value) ^ "), " ^ (stringify tl)
+    in "[" ^ (stringify sub) ^ "]";;
+
 let string_of_interpr (i : interpretation) =
   let rec stringify = function
     | [] -> ""
@@ -32,66 +45,115 @@ let string_of_interpr (i : interpretation) =
     | (s, value) :: tl -> "(" ^ s ^ ": " ^ (string_of_bool value) ^ "), " ^ (stringify tl)
   in "[" ^ (stringify i) ^ "]";;
 
-let print_prop prop = print_endline (string_of_prop prop)
+let print_prop prop = print_endline (string_of_prop prop);;
 
-let rec find (i : interpretation) symbol =
-  match i with
-  | [] -> None
-  | (s, value) :: i ->
-    if s = symbol then
-      (if value then Some True else Some False)
-    else
-      find i symbol;;
 
-(* Apply all relevant mappings from an interpretation to the symbols of a proposition *)
-let rec interpret prop i =
-  match prop with
-  | True -> prop
-  | False -> prop
-  | Lit symbol ->
-    (match find i symbol with
-    | None -> prop
-    | Some a -> a)
-  | Not prop' ->
-    (match interpret prop' i with
+(* -------------------------------------------------------------------------------------------------------------------- *)
+(* ------------------------------ Utility functions for dealing with our new data types ------------------------------- *)
+(* -------------------------------------------------------------------------------------------------------------------- *)
+
+(* Converts an interpretation to a substitution *)
+let rec sub_of_interpr = function
+  | [] -> []
+  | (s, b) :: tl -> (s, if b then True else False) :: (sub_of_interpr tl);;
+
+(* Removes instances of True or False literals via simplification *)
+let rec simplify_true_false = function
+  | True -> True
+  | False -> False
+  | Lit symbol -> Lit symbol
+  | Not p ->
+    (match simplify_true_false p with
     | True -> False
     | False -> True
-    | _ -> prop)
+    | Not p' -> p'
+    | p' -> Not(p'))
   | And (p1, p2) ->
-    (match interpret p1 i, interpret p2 i with
+    (match simplify_true_false p1, simplify_true_false p2 with
     | False, _ -> False
     | _, False -> False
     | True, p2' -> p2'
     | p1', True -> p1'
-    | _ -> prop)
+    | p1', p2' -> And(p1', p2'))
   | Or (p1, p2) ->
-    (match interpret p1 i, interpret p2 i with
+    (match simplify_true_false p1, simplify_true_false p2 with
     | True, _ -> True
     | _, True -> True
     | False, p2' -> p2'
     | p1', False -> p1'
-    | _ -> prop)
-  | Implies (p1, p2) -> interpret (Or(Not(p1), p2)) i
-  | Iff (p1, p2) -> interpret (And(Implies(p1, p2), Implies(p2, p1))) i;;
+    | p1', p2' -> Or(p1', p2'))
+  | Implies (p1, p2) ->
+    (match simplify_true_false p1, simplify_true_false p2 with
+    | False, _ -> True
+    | True, p2' -> p2'
+    | p1', p2' -> Implies(p1', p2'))
+  | Iff (p1, p2) ->
+    (match simplify_true_false p1, simplify_true_false p2 with
+    | True, p2' -> p2'
+    | p1', True -> p1'
+    | False, p2' -> simplify_true_false (Not(p2'))
+    | p1', False -> simplify_true_false (Not(p1'))
+    | p1', p2' -> Implies(p1', p2'));;
+
+(* Finds a symbol in a list of substitutions and returns the value to substitute for that symbol *)
+let rec replace sub symbol =
+  match sub with
+  | [] -> Lit symbol
+  | (s, value) :: sub -> if s = symbol then value else replace sub symbol;;
+
+(* Substitutes propositions for symbols as specified by the sub argument *)
+let rec substitute (prop : proposition) (sub : substitution) =
+  match prop with
+  | True -> True
+  | False -> False
+  | Lit s -> replace sub s
+  | Not p -> Not (substitute p sub)
+  | And(p1, p2) -> And(substitute p1 sub, substitute p2 sub)
+  | Or(p1, p2) -> Or(substitute p1 sub, substitute p2 sub)
+  | Implies(p1, p2) -> Implies(substitute p1 sub, substitute p2 sub)
+  | Iff(p1, p2) -> And(substitute p1 sub, substitute p2 sub);;
+
+(* Converts a proposition to negation normal form *)
+let to_nnf prop =
+  let rec to_nnf = function
+    | True -> True
+    | False -> False
+    | Lit symbol -> Lit symbol
+    | Not p ->
+      (match to_nnf p with
+      | And(p1, p2) -> Or(to_nnf (Not(p1)), to_nnf (Not(p2)))
+      | Or(p1, p2) -> And(to_nnf (Not(p1)), to_nnf (Not(p2)))
+      | p' -> simplify_true_false (Not p'))
+    | And(p1, p2) -> And(to_nnf p1, to_nnf p2)
+    | Or(p1, p2) -> Or(to_nnf p1, to_nnf p2)
+    | Implies(p1, p2) -> to_nnf (Or(Not(p1), p2))
+    | Iff(p1, p2) -> to_nnf (And(Implies(p1, p2), Implies(p2, p1)))
+  in
+  simplify_true_false (to_nnf prop);;
+
+(* Applies an interpretation to a proposition and returns the resulting proposition *)
+let interpret prop i = simplify_true_false (substitute prop (sub_of_interpr i));;
 
 (* Tests whether a proposition holds under a given interpretation *)
-let test prop i =
+let test_interpretation prop i =
   match interpret prop i with
   | True -> Some true
   | False -> Some false
   | _ -> None;; (* return None if cannot be determined *)
 
-(* Convert a proposition to negation normal form *)
-let to_nnf prop = "TODO"
 
+(* -------------------------------------------------------------------------------------------------------------------- *)
+(* ------------------------------------------------------ Examples ---------------------------------------------------- *)
+(* -------------------------------------------------------------------------------------------------------------------- *)
 
-(* Examples *)
 let show_example p i =
   print_endline ("Proposition p:     " ^ (string_of_prop p));
+  print_endline ("p in NNF:          " ^ (string_of_prop (to_nnf p)));
   print_endline ("Interpretation i:  " ^ (string_of_interpr i));
   print_endline ("p under i:         " ^ (string_of_prop (interpret p i)) ^ "\n");;
 
-let p1 = Iff(Not(Implies(Or(Lit "a", Lit "b"), And(Lit "b", Lit "c"))), True);;
+let p1 = Not(Not(Not(And(Lit "a", Lit "b"))));;
+let p2 = Iff(Not(Implies(Or(Lit "a", Lit "b"), And(Lit "b", Lit "c"))), True);;
 let i1 = [("a", false); ("b", true); ("c", false)];;
 let i2 = [("a", false); ("b", false)];;
 let i3 = [("c", true)];;
@@ -99,4 +161,7 @@ let i3 = [("c", true)];;
 show_example p1 i1;;
 show_example p1 i2;;
 show_example p1 i3;;
-(* print_endline (match test p i with None -> "None" | Some a -> string_of_bool a);; *)
+
+show_example p2 i1;;
+show_example p2 i2;;
+show_example p2 i3;;