commit 72cc7d4b486a26e5340dcda7488c8bb727a53a4e
parent bf3ea81e5285fe18edfbd74ac05dfb361f83f003
Author: erai <erai@omiltem.net>
Date: Fri, 24 Jan 2025 15:46:09 +0000
Add attic check.py
Diffstat:
| A | attic/check.py | | | 176 | +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ |
1 file changed, 176 insertions(+), 0 deletions(-)
diff --git a/attic/check.py b/attic/check.py
@@ -0,0 +1,176 @@
+class Sequent:
+ def __init__(self, hyp, con):
+ hyp = tuple(sorted(hyp, key=str))
+ con = tuple(sorted(con, key=str))
+ self.hyp = hyp
+ self.con = con
+
+ def __repr__(self):
+ hyp = " ".join(map(str, self.hyp))
+ con = " ".join(map(str, self.con))
+ return f'{hyp} :- {con}'
+
+ def occurs(self, t):
+ return any(p.occurs(t) for p in self.hyp + self.con)
+
+ def sub(self, x, t):
+ hyp = [p.sub(x, t) for p in self.hyp]
+ con = [p.sub(x, t) for p in self.con]
+ return Sequent(hyp, con)
+
+class Axiom(Proof):
+ def __init__(self, a):
+ hyp = [a]
+ con = [a]
+ self.conclude = Sequent(hyp, con)
+
+class Cut(Proof):
+ def __init__(self, left, right, a):
+ hyp = set(right.hyp)
+ hyp.remove(a)
+ hyp.extend(left.hyp)
+ con = set(left.con)
+ con.remove(a)
+ con.extend(right.con)
+ self.conclude = Sequent(hyp, con)
+
+class AndHyp1(Proof):
+ def __init__(self, left, a, b):
+ hyp = set(left.hyp)
+ hyp.remove(a)
+ hyp.add(AndProp(a, b))
+ con = left.con
+ self.conclude = Sequent(hyp, con)
+
+class AndHyp2(Proof):
+ def __init__(self, left, a, b):
+ hyp = set(left.hyp)
+ hyp.remove(a)
+ hyp.add(AndProp(b, a))
+ con = left.con
+ self.conclude = Sequent(hyp, con)
+
+class OrHyp(Proof):
+ def __init__(self, left, right, a, b):
+ hyp = set(left.hyp)
+ hyp.remove(a)
+ right_hyp = set(right.hyp)
+ right_hyp.remove(b)
+ hyp.add(OrProp(a, b))
+ con = right.con
+ self.conclude = Sequent(hyp, con)
+
+class ImpHyp(Proof):
+ def __init__(self, left, right, a, b):
+ left_hyp = set(left.hyp)
+ left_con = set(left.con)
+ right_hyp = set(right.hyp)
+ right_con = set(right.con)
+ left_con.remove(a)
+ right_hyp.remove(b)
+ hyp = left_hyp + right_hyp
+ hyp.add(ImpProp(a, b))
+ con = left_con + right_con
+ self.conclude = Sequent(hyp, con)
+
+class NotHyp(Proof):
+ def __init__(self, left, a):
+ hyp = set(left.hyp)
+ con = set(left.con)
+ con.remove(a)
+ hyp.add(NotProp(a))
+ self.conclude = Sequent(hyp, con)
+
+class AllHyp(Proof):
+ def __init__(self, left, a, x, t):
+ hyp = set(left.hyp)
+ b = a.sub(x, t)
+ hyp.remove(b)
+ c = AllProp(x, a)
+ hyp.add(c)
+ con = left.con
+ self.conclude = Sequent(hyp, con)
+
+class ExistHyp(Proof):
+ def __init__(self, left, a, x, y):
+ hyp = set(left.hyp)
+ b = a.sub(x, y)
+ hyp.remove(b)
+ c = ExistProp(x, a)
+ hyp.add(c)
+ con = left.con
+ self.conclude = Sequent(hyp, con)
+
+class WeakHyp(Proof):
+ def __init__(self, left, a):
+ hyp = set(left.hyp)
+ hyp.add(a)
+ con = left.con
+ self.conclude = Sequent(hyp, con)
+
+class OrCon1(Proof):
+ def __init__(self, left, a, b):
+ hyp = left.hyp
+ con = set(left.con)
+ con.remove(a)
+ con.add(OrProp(a, b))
+ self.conclude = Sequent(hyp, con)
+
+class OrCon2(Proof):
+ def __init__(self, left, a, b):
+ hyp = left.hyp
+ con = set(left.con)
+ con.remove(a)
+ con.add(OrProp(b, a))
+ self.conclude = Sequent(hyp, con)
+
+class AndCon(Proof):
+ def __init__(self, left, right, a, b):
+ hyp = left.hyp
+ left_con = set(left.con)
+ right_con = set(right.con)
+ left_con.remove(a)
+ right_con.remove(b)
+ con = set(left_con)
+ con.add(AndProp(a, b))
+ self.conclude = Sequent(hyp, con)
+
+class ImpCon(Proof):
+ def __init__(self, left, a, b):
+ hyp = set(left.hyp)
+ con = set(left.con)
+ hyp.remove(a)
+ con.remove(b)
+ con.add(ImpProp(a, b))
+ self.conclude = Sequent(hyp, con)
+
+class NotCon(Proof):
+ def __init__(self, left, a):
+ hyp = set(left.hyp)
+ con = set(left.con)
+ hyp.remove(a)
+ con.add(NotProp(a))
+ self.conclude = Sequent(hyp, con)
+
+class AllCon(Proof):
+ def __init__(self, left, a, x, y):
+ hyp = left.hyp
+ con = set(left.con)
+ b = a.sub(x, y)
+ con.remove(b)
+ c = AllProp(x, a)
+ con.add(c)
+ self.conclude = Sequent(hyp, con)
+
+class ExistCon(Proof):
+ def __init__(self, left, a, x, t):
+ hyp = left.hyp
+ con = set(left.con)
+ b = a.sub(x, t)
+ con.remove(b)
+ c = ExistProp(x, a)
+ con.add(c)
+ self.conclude = Sequent(hyp, con)
+
+# WeakCon
+# A:-B ==> A:-B,c
