From c97957b76a6ff95aa413ed5cf1a39ec76aad9a60 Mon Sep 17 00:00:00 2001 From: Kai Stevenson Date: Tue, 13 Jun 2023 21:24:31 -0700 Subject: added implication elim rule --- src/eval.c | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) diff --git a/src/eval.c b/src/eval.c index 4e978b6..263e1c1 100644 --- a/src/eval.c +++ b/src/eval.c @@ -61,6 +61,24 @@ char just_is_sound(line_t line, lineSet_t lines) { return 0; } return peq(prop, *w.propA) || peq(prop, *w.propB); + case IMPLICATION_ELIM: + wl = lines.lines[just.references[0] - 1]; + xl = lines.lines[just.references[1] - 1]; + w = wl.proposition; + x = xl.proposition; + if (!seqlt(line.scope, wl.scope) || !seqlt(line.scope, xl.scope)) { + return 0; + } + /* find the positions of the arguments */ + if (!w.isSimple && peq(prop, *w.propB) && w.relation == IMPLICATION && peq(x, *w.propA)) { + return 1; + } + else if (!x.isSimple && peq(prop, *x.propB) && x.relation == IMPLICATION && peq(w, *x.propA)) { + return 1; + } + else { + return 0; + } default: return 0; } -- cgit v1.3.1