added contradiction introduction rule

1 files changed, 17 insertions, 0 deletions

diff --git a/src/proposition.c b/src/proposition.c
index 6f28fbe..4d4b473 100644
--- a/src/proposition.c
+++ b/src/proposition.c
@@ -1,3 +1,4 @@
+#include <stdlib.h>
 #include "proposition.h"
 /* a proposition defines a relation between two propositions */
 prop_t init_prop(char isNegative, prop_t* propA, prop_t* propB, tokenType_t relation) {
@@ -7,6 +8,7 @@ prop_t init_prop(char isNegative, prop_t* propA, prop_t* propB, tokenType_t rela
 	prop.propB = propB;
 	prop.relation = relation;
 	prop.isSimple = 0;
+	prop.isContradiction = 0;
 	return prop;
 }
 /* a simple proposition is one with only a name */
@@ -15,6 +17,15 @@ prop_t init_simple_prop(char isNegative, char* name) {
 	prop.isNegative = isNegative;
 	prop.name = name;
 	prop.isSimple = 1;
+	prop.isContradiction = 0;
+	return prop;
+}
+prop_t init_contradiction_prop() {
+	prop_t prop;
+	prop.isNegative = 0;
+	prop.name = NULL;
+	prop.isSimple = 1;
+	prop.isContradiction = 1;
 	return prop;
 }
 char* jrtos(justRule_t rule) {
@@ -29,12 +40,18 @@ char* jrtos(justRule_t rule) {
 			return "DISJUNCTION INTRODUCTION";
 		case IMPLICATION_INTRO:
 			return "IMPLICATION INTRODUCTION";
+		case NEGATION_INTRO:
+			return "NEGATION INTRODUCTION";
+		case CONTRADICTION_INTRO:
+			return "CONTRADICTION INTRODUCTION";
 		case CONJUNCT_ELIM:
 			return "CONJUNCTION ELIMINATION";
 		case DISJUNCT_ELIM:
 			return "DISJUNCTION ELIMINATION";
 		case IMPLICATION_ELIM:
 			return "IMPLICATION ELIMINATION";
+		case NEGATION_ELIM:
+			return "NEGATION ELIMINATION";
 		default:
 			return "ERR";
 	}