check.py (4570B)
1 class Sequent: 2 def __init__(self, hyp, con): 3 hyp = tuple(sorted(hyp, key=str)) 4 con = tuple(sorted(con, key=str)) 5 self.hyp = hyp 6 self.con = con 7 8 def __repr__(self): 9 hyp = " ".join(map(str, self.hyp)) 10 con = " ".join(map(str, self.con)) 11 return f'{hyp} :- {con}' 12 13 def occurs(self, t): 14 return any(p.occurs(t) for p in self.hyp + self.con) 15 16 def sub(self, x, t): 17 hyp = [p.sub(x, t) for p in self.hyp] 18 con = [p.sub(x, t) for p in self.con] 19 return Sequent(hyp, con) 20 21 class Axiom(Proof): 22 def __init__(self, a): 23 hyp = [a] 24 con = [a] 25 self.conclude = Sequent(hyp, con) 26 27 class Cut(Proof): 28 def __init__(self, left, right, a): 29 hyp = set(right.hyp) 30 hyp.remove(a) 31 hyp.extend(left.hyp) 32 con = set(left.con) 33 con.remove(a) 34 con.extend(right.con) 35 self.conclude = Sequent(hyp, con) 36 37 class AndHyp1(Proof): 38 def __init__(self, left, a, b): 39 hyp = set(left.hyp) 40 hyp.remove(a) 41 hyp.add(AndProp(a, b)) 42 con = left.con 43 self.conclude = Sequent(hyp, con) 44 45 class AndHyp2(Proof): 46 def __init__(self, left, a, b): 47 hyp = set(left.hyp) 48 hyp.remove(a) 49 hyp.add(AndProp(b, a)) 50 con = left.con 51 self.conclude = Sequent(hyp, con) 52 53 class OrHyp(Proof): 54 def __init__(self, left, right, a, b): 55 hyp = set(left.hyp) 56 hyp.remove(a) 57 right_hyp = set(right.hyp) 58 right_hyp.remove(b) 59 hyp.add(OrProp(a, b)) 60 con = right.con 61 self.conclude = Sequent(hyp, con) 62 63 class ImpHyp(Proof): 64 def __init__(self, left, right, a, b): 65 left_hyp = set(left.hyp) 66 left_con = set(left.con) 67 right_hyp = set(right.hyp) 68 right_con = set(right.con) 69 left_con.remove(a) 70 right_hyp.remove(b) 71 hyp = left_hyp + right_hyp 72 hyp.add(ImpProp(a, b)) 73 con = left_con + right_con 74 self.conclude = Sequent(hyp, con) 75 76 class NotHyp(Proof): 77 def __init__(self, left, a): 78 hyp = set(left.hyp) 79 con = set(left.con) 80 con.remove(a) 81 hyp.add(NotProp(a)) 82 self.conclude = Sequent(hyp, con) 83 84 class AllHyp(Proof): 85 def __init__(self, left, a, x, t): 86 hyp = set(left.hyp) 87 b = a.sub(x, t) 88 hyp.remove(b) 89 c = AllProp(x, a) 90 hyp.add(c) 91 con = left.con 92 self.conclude = Sequent(hyp, con) 93 94 class ExistHyp(Proof): 95 def __init__(self, left, a, x, y): 96 hyp = set(left.hyp) 97 b = a.sub(x, y) 98 hyp.remove(b) 99 c = ExistProp(x, a) 100 hyp.add(c) 101 con = left.con 102 self.conclude = Sequent(hyp, con) 103 104 class WeakHyp(Proof): 105 def __init__(self, left, a): 106 hyp = set(left.hyp) 107 hyp.add(a) 108 con = left.con 109 self.conclude = Sequent(hyp, con) 110 111 class OrCon1(Proof): 112 def __init__(self, left, a, b): 113 hyp = left.hyp 114 con = set(left.con) 115 con.remove(a) 116 con.add(OrProp(a, b)) 117 self.conclude = Sequent(hyp, con) 118 119 class OrCon2(Proof): 120 def __init__(self, left, a, b): 121 hyp = left.hyp 122 con = set(left.con) 123 con.remove(a) 124 con.add(OrProp(b, a)) 125 self.conclude = Sequent(hyp, con) 126 127 class AndCon(Proof): 128 def __init__(self, left, right, a, b): 129 hyp = left.hyp 130 left_con = set(left.con) 131 right_con = set(right.con) 132 left_con.remove(a) 133 right_con.remove(b) 134 con = set(left_con) 135 con.add(AndProp(a, b)) 136 self.conclude = Sequent(hyp, con) 137 138 class ImpCon(Proof): 139 def __init__(self, left, a, b): 140 hyp = set(left.hyp) 141 con = set(left.con) 142 hyp.remove(a) 143 con.remove(b) 144 con.add(ImpProp(a, b)) 145 self.conclude = Sequent(hyp, con) 146 147 class NotCon(Proof): 148 def __init__(self, left, a): 149 hyp = set(left.hyp) 150 con = set(left.con) 151 hyp.remove(a) 152 con.add(NotProp(a)) 153 self.conclude = Sequent(hyp, con) 154 155 class AllCon(Proof): 156 def __init__(self, left, a, x, y): 157 hyp = left.hyp 158 con = set(left.con) 159 b = a.sub(x, y) 160 con.remove(b) 161 c = AllProp(x, a) 162 con.add(c) 163 self.conclude = Sequent(hyp, con) 164 165 class ExistCon(Proof): 166 def __init__(self, left, a, x, t): 167 hyp = left.hyp 168 con = set(left.con) 169 b = a.sub(x, t) 170 con.remove(b) 171 c = ExistProp(x, a) 172 con.add(c) 173 self.conclude = Sequent(hyp, con) 174 175 # WeakCon 176 # A:-B ==> A:-B,c