added apiHEADmaster

12 files changed, 304 insertions, 332 deletions

diff --git a/lib/datatypes.ml b/lib/datatypes.ml
deleted file mode 100644
index 37c61b6..0000000
--- a/lib/datatypes.ml
+++ /dev/null
@@ -1,213 +0,0 @@
-(* -------------------------------------------------------------------------------------------------------------------- *)
-(* ----------------------------------- Data types useful for our theorem prover(s) ------------------------------------ *)
-(* -------------------------------------------------------------------------------------------------------------------- *)
-
-type proposition = (* logical proposition *)
-  | True
-  | False
-  | Lit of string
-  | Not of proposition
-  | And of proposition * proposition
-  | Or of proposition * proposition
-  | Implies of proposition * proposition
-  | Iff of proposition * proposition;;
-
-type interpretation = (string * bool) list;; (* interpretation *)
-
-type substitution = (string * proposition) list;; (* allows us to substitute any proposition for any atomic literal *)
-
-
-(* -------------------------------------------------------------------------------------------------------------------- *)
-(* ----------------------------------------- Utility functions for debugging ------------------------------------------ *)
-(* -------------------------------------------------------------------------------------------------------------------- *)
-
-let rec string_of_prop = function
-  | True -> "True"
-  | False -> "False"
-  | Lit symbol -> symbol
-  | Not p -> "¬" ^ (string_of_prop p)
-  | And (p1, p2) -> "(" ^ (string_of_prop p1) ^ " ∧ " ^ (string_of_prop p2) ^ ")"
-  | Or (p1, p2) -> "(" ^ (string_of_prop p1) ^ " ∨ " ^ (string_of_prop p2) ^ ")"
-  | 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
-    | [] -> ""
-    | (s, value) :: [] -> "(" ^ s ^ ": " ^ (string_of_bool value) ^ ")"
-    | (s, value) :: tl -> "(" ^ s ^ ": " ^ (string_of_bool value) ^ "), " ^ (stringify tl)
-  in "[" ^ (stringify i) ^ "]";;
-
-let print_prop prop = print_endline (string_of_prop prop);;
-
-
-(* -------------------------------------------------------------------------------------------------------------------- *)
-(* ------------------------------ 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
-    | Not p' -> p'
-    | p' -> Not(p'))
-  | And (p1, p2) ->
-    (match simplify_true_false p1, simplify_true_false p2 with
-    | False, _ -> False
-    | _, False -> False
-    | True, p2' -> p2'
-    | p1', True -> p1'
-    | p1', p2' -> And(p1', p2'))
-  | Or (p1, p2) ->
-    (match simplify_true_false p1, simplify_true_false p2 with
-    | True, _ -> True
-    | _, True -> True
-    | False, p2' -> p2'
-    | p1', False -> p1'
-    | 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' -> Iff(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_interpretation prop i =
-  match interpret prop i with
-  | True -> Some true
-  | False -> Some false
-  | _ -> None;; (* return None if cannot be determined *)
-
-
-(* -------------------------------------------------------------------------------------------------------------------- *)
-(* --------------------------------- Sequent Calculus (TODO: move this to dif file) ----------------------------------- *)
-(* -------------------------------------------------------------------------------------------------------------------- *)
-
-type seq = Seq of proposition list * proposition list;; (* sequent *)
-
-type stree = (* tree of sequents *)
-  | Taut (* tautology of the form A, Gamma => A, Delta *)
-  | Br of stree * stree
-
-let string_of_seq (Seq (p1, p2)) =
-  let rec string_of_prop_list = function
-    | [] -> ""
-    | p :: ps -> (string_of_prop p) ^ ", " ^ (string_of_prop_list ps)
-  in
-  (string_of_prop_list p1) ^ "⇒" ^ (string_of_prop_list p2);;
-
-(* let rec reduce_seq s =
-  let rec not_lhs (Seq(p1s, p2s)) =
-    match p1s with
-    | [] -> Seq(p1s, p2s), None, false
-    | p::ps ->
-      (match p with
-      | Not(p') -> Seq(ps, p'::p2s), None, true
-      | _ -> let Seq(ps', p2s), _, found = not_lhs (Seq(ps, p2s)) in Seq(p::ps', p2s), None, found)
-  in
-  let rec not_rhs (Seq(p1s, p2s)) =
-    match p2s with
-    | [] -> Seq(p1s, p2s), None, false
-    | p::ps ->
-      (match p with
-      | Not(p') -> Seq(p'::p1s, ps), None, true
-      | _ -> let Seq(p1s, ps'), _, found = not_rhs (Seq(p1s, ps)) in Seq(p1s, p::ps'), None, found)
-  in
-  let rec and_lhs (Seq(p1s, p2s)) =
-    match p1s with
-    | [] -> Seq(p1s, p2s), None, false
-    | p::ps ->
-      (match p with
-      | And(p1, p2) -> Seq(p1::p2::ps, p2s), None, true
-      | _ -> let Seq(p1s, ps'), _, found = and_lhs (Seq(p1s, ps)) in Seq(p1s, p::ps'), None, found)
-  in
-  let rec and_rhs (Seq(p1s, p2s)) =
-    match p2s with
-    | [] -> Seq(p1s, p2s), None, false
-    | p::ps ->
-      (match p with
-      | And(p1, p2) -> Seq(p1s, p1::ps), Some (Seq(p1s, p2::ps)), true
-      | _ ->
-        (match and_rhs (Seq(p1s, ps)) with
-        | Seq(p1s, ps'), None, found -> Seq(p1s, p2s), None, false
-        | Seq(p1s, ps'), Some (Seq(p1s', ps'')), found -> Seq(p1s, p::ps'), Some (Seq(p1s', p::ps'')), true))
-  in
-  match s with
-  | Seq  *)
-
-  (*
-  Steps (repeat in this order):
-  - reduce AND on LHS
-  - reduce OR on RHS
-  - reduce NOT on LHS
-  - reduce NOT on RHS
-  - reduce -> (RHS)
-  - reduce <-> (both)
-  - reduce OR (LHS)
-  - reduce AND (RHS)
-  - reduce -> (LHS)
-  *)
-  
\ No newline at end of file
diff --git a/lib/dune b/lib/dune
index 5612af0..76acc9d 100644
--- a/lib/dune
+++ b/lib/dune
@@ -1,2 +1,4 @@
+(include_subdirs qualified)
+
 (library
- (name power_prover))
+ (name chadprover))
diff --git a/lib/exports.ml b/lib/exports.ml
new file mode 100644
index 0000000..f9baf73
--- /dev/null
+++ b/lib/exports.ml
@@ -0,0 +1,12 @@
+(* Functions we want to expose for usage within the api *)
+
+(* Read string input and convert to proposition *)
+let parse_input = Input_sanitization.Input_sanitizer.process
+
+(* Find a truth assignment satisfying the input proposition or return None *)
+let find_satisfying_interpretation = Satisfiability.Satisfiable.satisfy
+
+(* Find a sequent calculus proof or return None if proposition not provable *)
+let get_sequent_calculus_proof = Sequent_calculus.Sequent_proof.prove
+
+let get_tableau_calculus_proof = () (* TODO *)
diff --git a/lib/input_sanitization/input_sanitizer.ml b/lib/input_sanitization/input_sanitizer.ml
new file mode 100644
index 0000000..f5c483d
--- /dev/null
+++ b/lib/input_sanitization/input_sanitizer.ml
@@ -0,0 +1,6 @@
+(* Sanitize the inputs *)
+
+(* TODO: handle exceptions *)
+let process (input : string) : Types.proposition =
+  input |> Lexing.Lexer.lex |> Parsing.Parser.parse
+
diff --git a/lib/lib_utils.ml b/lib/lib_utils.ml
index e9a67b8..5dcbfd7 100644
--- a/lib/lib_utils.ml
+++ b/lib/lib_utils.ml
@@ -1,59 +1,82 @@
-(* Utility functions for dealing with our new data types *)
+(* Utility functions *)
 
 open 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);;
+  | (s, b) :: tl -> (s, if b then True else False) :: (sub_of_interpr tl)
 
-(* Removes instances of True or False literals via simplification *)
+(* Removes instances of True or False literals via simplification as well as repeated Nots *)
 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
-    | Not p' -> p'
-    | p' -> Not(p'))
+    begin
+      match simplify_true_false p with
+      | True -> False
+      | False -> True
+      | Not p' -> p'
+      | p' -> Not(p')
+    end
   | And (p1, p2) ->
-    (match simplify_true_false p1, simplify_true_false p2 with
-    | False, _ -> False
-    | _, False -> False
-    | True, p2' -> p2'
-    | p1', True -> p1'
-    | p1', p2' -> And(p1', p2'))
+    begin
+      match simplify_true_false p1, simplify_true_false p2 with
+      | False, _ -> False
+      | _, False -> False
+      | True, p2' -> p2'
+      | p1', True -> p1'
+      | p1', p2' -> And(p1', p2')
+    end
   | Or (p1, p2) ->
-    (match simplify_true_false p1, simplify_true_false p2 with
-    | True, _ -> True
-    | _, True -> True
-    | False, p2' -> p2'
-    | p1', False -> p1'
-    | p1', p2' -> Or(p1', p2'))
+    begin
+      match simplify_true_false p1, simplify_true_false p2 with
+      | True, _ -> True
+      | _, True -> True
+      | False, p2' -> p2'
+      | p1', False -> p1'
+      | p1', p2' -> Or(p1', p2')
+    end
   | Implies (p1, p2) ->
-    (match simplify_true_false p1, simplify_true_false p2 with
-    | False, _ -> True
-    | True, p2' -> p2'
-    | p1', p2' -> Implies(p1', p2'))
+    begin
+      match simplify_true_false p1, simplify_true_false p2 with
+      | False, _ -> True
+      | True, p2' -> p2'
+      | p1', p2' -> Implies(p1', p2')
+    end
   | 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' -> Iff(p1', p2'));;
+    begin
+      match simplify_true_false p1, simplify_true_false p2 with
+      | True, p2' -> p2'
+      | p1', True -> p1'
+      | False, p2' ->
+        begin (* need to simplify Not(p2'), which depends on the form of p2' *)
+          match p2' with
+          | True -> False
+          | False -> True
+          | Not p -> p
+          | p -> Not(p)
+        end
+      | p1', False ->
+        begin (* need to simplify Not(p1') *)
+          match p1' with
+          | True -> False
+          | False -> True
+          | Not p -> p
+          | p -> Not(p)
+        end
+      | p1', p2' -> Iff(p1', p2')
+    end
 
 (* 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;;
+  | (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) =
+let rec substitute (prop : proposition) (sub : substitution) : proposition =
   match prop with
   | True -> True
   | False -> False
@@ -62,7 +85,7 @@ let rec substitute (prop : proposition) (sub : substitution) =
   | 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);;
+  | Iff(p1, p2) -> Iff(substitute p1 sub, substitute p2 sub)
 
 (* Converts a proposition to negation normal form *)
 let to_nnf prop =
@@ -71,23 +94,30 @@ let to_nnf prop =
     | 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'))
+      begin
+        match p with
+        | True -> False
+        | False -> True
+        | Lit s -> Not(Lit s)
+        | Not p' -> to_nnf p'
+        | And(p1, p2) -> Or(to_nnf (Not(p1)), to_nnf (Not(p2))) (* De Morgan's Laws *)
+        | Or(p1, p2) -> And(to_nnf (Not(p1)), to_nnf (Not(p2)))
+        | Implies(p1, p2) -> And(to_nnf p1, to_nnf (Not(p2))) (* not (A -> B) = A and not B*)
+        | Iff(p1, p2) -> Or(And(to_nnf p1, to_nnf (Not(p2))), And(to_nnf (Not(p1)), to_nnf p2))
+      end
     | 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);;
+  to_nnf (simplify_true_false 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));;
+let interpret prop i = simplify_true_false (substitute prop (sub_of_interpr i))
 
 (* Tests whether a proposition holds under a given interpretation *)
 let test_interpretation prop i =
   match interpret prop i with
   | True -> Some true
   | False -> Some false
-  | _ -> None;; (* return None if cannot be determined *)
+  | _ -> None (* return None if cannot be determined *)
diff --git a/lib/satisfiability/satisfiable.ml b/lib/satisfiability/satisfiable.ml
new file mode 100644
index 0000000..6eccc27
--- /dev/null
+++ b/lib/satisfiability/satisfiable.ml
@@ -0,0 +1,74 @@
+(* Find a satisfying interpretation via brute force *)
+
+open Types
+open Lib_utils
+
+(* lazy list *)
+type 'a seq = Nil | Cons of 'a * (unit -> 'a seq)
+
+let head = function
+  | Nil -> None
+  | Cons(x, _) -> Some x
+
+let tail = function
+  | Nil -> None
+  | Cons(_, tl) -> Some tl
+
+let rec get k s =
+  match k, s with
+  | 0, _ -> []
+  | _, Nil -> []
+  | k, Cons(x, f) -> x :: get (k - 1) (f ())
+
+(* Find all the literals in a formula *)
+let extract_symbols (prop : proposition) =
+  let rec search prop acc =
+    match prop with
+    | True -> acc
+    | False -> acc
+    | Lit s -> Lit s :: acc
+    | Not p -> search p acc
+    | And(p1, p2) -> search p1 (search p2 acc)
+    | Or(p1, p2) -> search p1 (search p2 acc)
+    | Implies(p1, p2) -> search p1 (search p2 acc)
+    | Iff(p1, p2) -> search p1 (search p2 acc)
+  in
+  search prop []
+
+(* Generate all possible truth assignments for a list of symbols *)
+let rec generate_truth_vals symbols =
+  let rec prepend_all x llist = (* prepend x to each item in the lazy list *)
+    match llist with
+    | Nil -> Nil
+    | Cons(xs, fn) -> Cons(x::xs, fun () -> prepend_all x (fn ()))
+  in
+  let rec interleave s1 s2 =
+    match s1, s2 with
+    | _, Nil -> s1
+    | Nil, _ -> s2
+    | Cons(x1, f1), _ -> Cons(x1, fun () -> interleave s2 (f1 ()))
+  in
+  match symbols with
+  | [] -> Cons ([], fun () -> Nil)
+  | Lit s :: tl ->
+      let tl_vals = generate_truth_vals tl in
+      let s_true = prepend_all (s, true) tl_vals in
+      let s_false = prepend_all (s, false) tl_vals in
+      interleave s_true s_false
+  | _ -> failwith "discovered a bug"
+
+(* brute force search for a satisfying interpretation *)
+let satisfy prop =
+  let symbols = extract_symbols prop in
+  let truth_vals = generate_truth_vals symbols in
+  let rec try_next truth_vals =
+    match truth_vals with
+    | Nil -> None
+    | Cons(i, f) ->
+      begin
+        match test_interpretation prop i with
+        | Some true -> Some i
+        | _ -> try_next (f ())
+      end
+  in
+  try_next truth_vals
diff --git a/lib/sequent_calculus/headers.ml b/lib/sequent_calculus/headers.ml
new file mode 100644
index 0000000..0bef07a
--- /dev/null
+++ b/lib/sequent_calculus/headers.ml
@@ -0,0 +1,5 @@
+(* Sequent calculus: types and exceptions *)
+
+(* exceptions that can occur when attempting a sequent proof *)
+exception RuleNotApplicable
+exception NotProvable of string
diff --git a/lib/sequent_calculus/sequent_proof.ml b/lib/sequent_calculus/sequent_proof.ml
new file mode 100644
index 0000000..7d8c0f9
--- /dev/null
+++ b/lib/sequent_calculus/sequent_proof.ml
@@ -0,0 +1,41 @@
+(* Sequent Calculus *)
+
+open Types
+open Headers
+open Sequent_rules
+
+(* returns true if arg is the basic tautological sequent *)
+let rec is_basic_sequent (Seq(l1, l2)) =
+  match l1 with
+  | [] -> false
+  | p :: ps -> List.mem p l2 || is_basic_sequent (Seq (ps, l2))
+
+(* gives list of sequents that need to be proved for this to be true *)
+let get_dependencies (s : seq) : seq list =
+  let rec apply_each fns s = (* apply each fn to s and return first result *)
+    match fns with
+    | [] -> raise (NotProvable "Couldn't find proof")
+    | fn :: fns ->
+      try
+        fn s
+      with
+      | RuleNotApplicable -> apply_each fns s
+  in
+  if is_basic_sequent s then
+    []
+  else
+    apply_each rule_precedence_list s
+
+(* generates a proof for a sequent in stree form or throws an exception *)
+(* TODO: deal with <-> case *)
+let rec prove_sequent (s : seq) : stree =
+  let dependencies = get_dependencies s in
+  let proofs = List.map prove_sequent dependencies in
+  Concl(s, proofs)
+
+(* Prove a proposition via the sequent calculus or return None if not provable *)
+let prove (p : proposition): stree option =
+  try
+    Some (prove_sequent (Seq ([], [p])))
+  with NotProvable _ ->
+    None
diff --git a/lib/sequent_calculus/sequent_rules.ml b/lib/sequent_calculus/sequent_rules.ml
new file mode 100644
index 0000000..68f2b63
--- /dev/null
+++ b/lib/sequent_calculus/sequent_rules.ml
@@ -0,0 +1,64 @@
+(* Logic for applying sequent calculus rules *)
+
+open Types
+open Headers
+
+(* apply NOT rule for LHS if possible *)
+let rec not_lhs = function
+  | Seq([], _) -> raise RuleNotApplicable
+  | Seq(Not(p1) :: p1s, p2s) -> [Seq(p1s, p1 :: p2s)]
+  | Seq(_ :: p1s, p2s) -> not_lhs (Seq(p1s, p2s))
+
+(* apply NOT rule for RHS if possible *)
+let rec not_rhs = function
+  | Seq(_, []) -> raise RuleNotApplicable
+  | Seq(p1s, Not(p2) :: p2s) -> [Seq(p2 :: p1s, p2s)]
+  | Seq(p1s, _ :: p2s) -> not_rhs (Seq(p1s, p2s))
+
+(* apply AND rule for LHS if possible *)
+let rec and_lhs = function
+  | Seq([], _) -> raise RuleNotApplicable
+  | Seq(And(p1, p1') :: p1s, p2s) -> [Seq(p1 :: p1' :: p1s, p2s)]
+  | Seq(_ :: p1s, p2s) -> and_lhs (Seq(p1s, p2s))
+
+(* apply AND rule for RHS if possible *)
+let rec and_rhs = function
+  | Seq(_, []) -> raise RuleNotApplicable
+  | Seq(p1s, And(p2, p2') :: p2s) -> [Seq(p1s, p2 :: p2s); Seq(p1s, p2' :: p2s)]
+  | Seq(p1s, _ :: p2s) -> and_rhs (Seq(p1s, p2s))
+
+(* apply OR rule for LHS if possible *)
+let rec or_lhs = function
+  | Seq([], _) -> raise RuleNotApplicable
+  | Seq(Or(p1, p1') :: p1s, p2s) -> [Seq(p1 :: p1s, p2s); Seq(p1' :: p1s, p2s)]
+  | Seq(_ :: p1s, p2s) -> or_lhs (Seq(p1s, p2s))
+
+(* apply OR rule for RHS if possible *)
+let rec or_rhs = function
+  | Seq(_, []) -> raise RuleNotApplicable
+  | Seq(p1s, Or(p2, p2') :: p2s) -> [Seq(p1s, p2 :: p2' :: p2s)]
+  | Seq(p1s, _ :: p2s) -> or_rhs (Seq(p1s, p2s))
+
+(* apply -> rule for LHS if possible *)
+let rec implies_lhs = function
+  | Seq([], _) -> raise RuleNotApplicable
+  | Seq(Implies(p1, p1') :: p1s, p2s) -> [Seq(p1s, p1 :: p2s); Seq(p1' :: p1s, p2s)]
+  | Seq(_ :: p1s, p2s) -> implies_lhs (Seq(p1s, p2s))
+
+(* apply -> rule for RHS if possible *)
+let rec implies_rhs = function
+  | Seq(_, []) -> raise RuleNotApplicable
+  | Seq(p1s, Implies(p2, p2') :: p2s) -> [Seq(p2 :: p1s, p2' :: p2s)]
+  | Seq(p1s, _ :: p2s) -> implies_rhs (Seq(p1s, p2s))
+
+(* precedence rules for applying rules *)
+let rule_precedence_list = [ 
+  and_lhs;        (* reduce AND on LHS *)
+  or_rhs;         (* reduce OR on RHS  *)
+  not_lhs;        (* reduce NOT on LHS *)
+  not_rhs;        (* reduce NOT on RHS *)
+  implies_rhs;    (* reduce -> on RHS  *)
+  or_lhs;         (* reduce OR on LHS  *)
+  and_rhs;        (* reduce AND on RHS *)
+  implies_lhs     (* reduce -> on LHS  *)
+]
diff --git a/lib/sequent_calculus/sequents.ml b/lib/sequent_calculus/sequents.ml
deleted file mode 100644
index 0b4a33a..0000000
--- a/lib/sequent_calculus/sequents.ml
+++ /dev/null
@@ -1,72 +0,0 @@
-
-(* Sequent Calculus *)
-
-open Types
-open To_string
-
-
-type seq = Seq of proposition list * proposition list;; (* sequent *)
-
-type stree = (* tree of sequents *)
-  | Taut (* tautology of the form A, Gamma => A, Delta *)
-  | Br of stree * stree
-
-let string_of_seq (Seq (p1, p2)) =
-  let rec string_of_prop_list = function
-    | [] -> ""
-    | p :: ps -> (string_of_prop p) ^ ", " ^ (string_of_prop_list ps)
-  in
-  (string_of_prop_list p1) ^ "⇒" ^ (string_of_prop_list p2);;
-
-(* let rec reduce_seq s =
-  let rec not_lhs (Seq(p1s, p2s)) =
-    match p1s with
-    | [] -> Seq(p1s, p2s), None, false
-    | p::ps ->
-      (match p with
-      | Not(p') -> Seq(ps, p'::p2s), None, true
-      | _ -> let Seq(ps', p2s), _, found = not_lhs (Seq(ps, p2s)) in Seq(p::ps', p2s), None, found)
-  in
-  let rec not_rhs (Seq(p1s, p2s)) =
-    match p2s with
-    | [] -> Seq(p1s, p2s), None, false
-    | p::ps ->
-      (match p with
-      | Not(p') -> Seq(p'::p1s, ps), None, true
-      | _ -> let Seq(p1s, ps'), _, found = not_rhs (Seq(p1s, ps)) in Seq(p1s, p::ps'), None, found)
-  in
-  let rec and_lhs (Seq(p1s, p2s)) =
-    match p1s with
-    | [] -> Seq(p1s, p2s), None, false
-    | p::ps ->
-      (match p with
-      | And(p1, p2) -> Seq(p1::p2::ps, p2s), None, true
-      | _ -> let Seq(p1s, ps'), _, found = and_lhs (Seq(p1s, ps)) in Seq(p1s, p::ps'), None, found)
-  in
-  let rec and_rhs (Seq(p1s, p2s)) =
-    match p2s with
-    | [] -> Seq(p1s, p2s), None, false
-    | p::ps ->
-      (match p with
-      | And(p1, p2) -> Seq(p1s, p1::ps), Some (Seq(p1s, p2::ps)), true
-      | _ ->
-        (match and_rhs (Seq(p1s, ps)) with
-        | Seq(p1s, ps'), None, found -> Seq(p1s, p2s), None, false
-        | Seq(p1s, ps'), Some (Seq(p1s', ps'')), found -> Seq(p1s, p::ps'), Some (Seq(p1s', p::ps'')), true))
-  in
-  match s with
-  | Seq  *)
-
-  (*
-  Steps (repeat in this order):
-  - reduce AND on LHS
-  - reduce OR on RHS
-  - reduce NOT on LHS
-  - reduce NOT on RHS
-  - reduce -> (RHS)
-  - reduce <-> (both)
-  - reduce OR (LHS)
-  - reduce AND (RHS)
-  - reduce -> (LHS)
-  *)
-  
\ No newline at end of file
diff --git a/lib/to_string.ml b/lib/to_string.ml
index 30e909b..5d74adf 100644
--- a/lib/to_string.ml
+++ b/lib/to_string.ml
@@ -1,3 +1,5 @@
+(* Various to_string and print functions *)
+
 open Types
 
 let rec string_of_prop = function
@@ -8,23 +10,24 @@ let rec string_of_prop = function
   | And (p1, p2) -> "(" ^ (string_of_prop p1) ^ " ∧ " ^ (string_of_prop p2) ^ ")"
   | Or (p1, p2) -> "(" ^ (string_of_prop p1) ^ " ∨ " ^ (string_of_prop p2) ^ ")"
   | Implies (p1, p2) -> "(" ^ (string_of_prop p1) ^ " → " ^ (string_of_prop p2) ^ ")"
-  | Iff (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) ^ "]";;
+    in "[" ^ (stringify sub) ^ "]"
 
 let string_of_interpr (i : interpretation) =
   let rec stringify = function
     | [] -> ""
     | (s, value) :: [] -> "(" ^ s ^ ": " ^ (string_of_bool value) ^ ")"
     | (s, value) :: tl -> "(" ^ s ^ ": " ^ (string_of_bool value) ^ "), " ^ (stringify tl)
-  in "[" ^ (stringify i) ^ "]";;
+  in "[" ^ (stringify i) ^ "]"
 
-let print_prop prop = print_endline (string_of_prop prop);;
+let print string_of_x x = x |> string_of_x |> print_endline
+let print_prop prop = print string_of_prop prop
 
 let string_of_tok = function
   | TRUE -> "TRUE"
@@ -42,3 +45,16 @@ let string_of_tok = function
 let rec string_of_tokens = function
   | [] -> ""
   | t :: ts -> "[" ^ string_of_tok t ^ "] " ^ string_of_tokens ts
+
+let string_of_seq (Seq (p1s, p2s)) =
+  let p1_string = String.concat ", " (List.map string_of_prop p1s) in
+  let p2_string = String.concat ", " (List.map string_of_prop p2s) in
+  p1_string ^ " ⇒ " ^ p2_string
+
+let rec string_of_stree = function
+  | Concl(s, []) -> "[" ^ string_of_seq s ^ "]"
+  | Concl(s, trees) -> "Seq(" ^ string_of_seq s ^ "| " ^ (String.concat "; " (List.map string_of_stree trees))  ^ ")"
+
+let rec json_string_of_stree = function
+  | Concl(s, []) -> "[\"" ^ string_of_seq s ^ "\", []]"
+  | Concl(s, trees) -> "[\"" ^ string_of_seq s ^ "\", [" ^ (String.concat ", " (List.map json_string_of_stree trees)) ^ "]]"
diff --git a/lib/types.ml b/lib/types.ml
index bf6a34d..a069cbd 100644
--- a/lib/types.ml
+++ b/lib/types.ml
@@ -12,7 +12,7 @@ type proposition =
   | Iff of proposition * proposition
 
 (* interpretation of propositional symbols *)
-type interpretation = (string * bool) list
+type interpretation = (string * bool) list (* note: we're using OCaml booleans here *)
 
 (* allows us to substitute any proposition for any atomic literal *)
 type substitution = (string * proposition) list
@@ -30,3 +30,10 @@ type tok =
   | LEFT_PAREN
   | RIGHT_PAREN
   | SKIP
+
+(* sequent *)
+type seq = Seq of proposition list * proposition list 
+
+(* tree of sequents where Conclusion(s, l) represents a sequent s and a list l of
+ * strees that together prove s *)
+type stree = Concl of seq * stree list