diff options
Diffstat (limited to 'lib/sequent_calculus/sequents.ml')
| -rw-r--r-- | lib/sequent_calculus/sequents.ml | 72 |
1 files changed, 72 insertions, 0 deletions
diff --git a/lib/sequent_calculus/sequents.ml b/lib/sequent_calculus/sequents.ml new file mode 100644 index 0000000..0b4a33a --- /dev/null +++ b/lib/sequent_calculus/sequents.ml @@ -0,0 +1,72 @@ + +(* 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 |