summaryrefslogtreecommitdiff
path: root/src/proposition.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/proposition.h')
-rw-r--r--src/proposition.h7
1 files changed, 6 insertions, 1 deletions
diff --git a/src/proposition.h b/src/proposition.h
index 2d09688..09509ea 100644
--- a/src/proposition.h
+++ b/src/proposition.h
@@ -4,6 +4,7 @@
typedef struct Proposition {
char isSimple;
char isNegative;
+ char isContradiction;
struct Proposition* propA;
struct Proposition* propB;
tokenType_t relation;
@@ -11,6 +12,7 @@ typedef struct Proposition {
} prop_t;
prop_t init_prop(char isNegative, prop_t* propA, prop_t* propB, tokenType_t relation);
prop_t init_simple_prop(char isNegative, char* name);
+prop_t init_contradiction_prop(void);
typedef enum JustificationRule {
ERR_R,
PREMISE_R,
@@ -19,10 +21,13 @@ typedef enum JustificationRule {
DISJUNCT_INTRO,
IMPLICATION_INTRO,
BI_IMPLICATION_INTRO,
+ NEGATION_INTRO,
+ CONTRADICTION_INTRO,
CONJUNCT_ELIM,
DISJUNCT_ELIM,
IMPLICATION_ELIM,
- BI_IMPLICATION_ELIM
+ BI_IMPLICATION_ELIM,
+ NEGATION_ELIM
} justRule_t;
char* jrtos(justRule_t rule);
typedef struct Justification {