From 69de932f9116b30adfd689d38e35ace63aef0e2d Mon Sep 17 00:00:00 2001 From: filip <“filip.rabiega@gmail.com”> Date: Fri, 16 Aug 2024 14:11:00 +0200 Subject: added api --- lib/sequent_calculus/sequent_rules.ml | 64 +++++++++++++++++++++++++++++++++++ 1 file changed, 64 insertions(+) create mode 100644 lib/sequent_calculus/sequent_rules.ml (limited to 'lib/sequent_calculus/sequent_rules.ml') 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 *) +] -- cgit v1.2.3