git @ Cat's Eye Technologies Philomath / c334a69
Implementation of neg_elim() (untested). Chris Pressey 3 years ago
3 changed file(s) with 13 addition(s) and 1 deletion(s). Raw diff Collapse all Expand all
+1
-1
README.md less more
8282 - [x] Absurdum value
8383 - [x] absr_elim: if absurdum is proved, then anything is proved (absr |- phi)
8484 - [ ] demo proof showing absr_elim
85 - [ ] neg_elim: if x is proved, and not x is proved, then absurdum is proved (phi, not phi |- absr)
85 - [x] neg_elim: if x is proved, and not x is proved, then absurdum is proved (phi, not phi |- absr)
8686 - [ ] demo proof showing neg_elim
8787 - [ ] neg_intro: if gamma, phi proves absurdum, then gamma proves not phi (gamma |- not phi, discharging gamma, phi)
8888 - [ ] demo proof showing neg_intro
+1
-0
include/proof.h less more
2525 struct proof *conj_elim_rhs(struct proof *);
2626
2727 struct proof *absr_elim(struct proof *, struct formula *);
28 struct proof *neg_elim(struct proof *, struct proof *);
2829
2930 #endif /* ndef PROOF_H */
+11
-0
src/proof.c less more
159159 q
160160 );
161161 }
162
163 struct proof *
164 neg_elim(struct proof *p, struct proof *q)
165 {
166 assert(q->conclusion->type == NEG, "neg_elim: not a negation");
167 assert(formula_eq(p->conclusion, q->conclusion->lhs), "neg_elim: mismatched conclusions");
168 return mk_proof(
169 merge(p->assumptions, q->assumptions),
170 absr()
171 );
172 }