From a7d426c3d5b72b57131c5ca2e6efbf0a7c2b8df9 Mon Sep 17 00:00:00 2001 From: Kai Stevenson Date: Sat, 17 Jun 2023 20:11:37 -0700 Subject: added contradiction introduction rule --- src/eval.c | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) (limited to 'src/eval.c') diff --git a/src/eval.c b/src/eval.c index 0c5d1db..26d1629 100644 --- a/src/eval.c +++ b/src/eval.c @@ -55,6 +55,24 @@ char just_is_sound(line_t line, lineSet_t lines) { } /* ensure that the arguments are in the correct scope */ return as.scope.id == res.scope.id && as.scope.depth == line.scope.depth + 1; + case CONTRADICTION_INTRO: + if (!prop.isContradiction) { + return 0; + } + 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; + } + if (!pbeq(w, x) ) { + return 0; + } + if (w.isNegative == x.isNegative) { + return 0; + } + return 1; case CONJUNCT_ELIM: wl = lines.lines[just.references[0] - 1]; w = wl.proposition; -- cgit v1.3.1