4 files changed, 110 insertions, 72 deletions
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