added contradiction introduction rule

1 files changed, 18 insertions, 0 deletions

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;