diff options
Diffstat (limited to 'src/eval.c')
| -rw-r--r-- | src/eval.c | 18 |
1 files changed, 18 insertions, 0 deletions
@@ -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; |
