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/proposition.c | 17 +++++++++++++++++ 1 file changed, 17 insertions(+) (limited to 'src/proposition.c') 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 #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"; } -- cgit v1.3.1