blob: 4d4b47378cc51df0495339357c9a91d09e47ec9c (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
|
#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) {
prop_t prop;
prop.isNegative = isNegative;
prop.propA = propA;
prop.propB = propB;
prop.relation = relation;
prop.isSimple = 0;
prop.isContradiction = 0;
return prop;
}
/* a simple proposition is one with only a name */
prop_t init_simple_prop(char isNegative, char* name) {
prop_t prop;
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) {
switch (rule) {
case PREMISE_R:
return "PREMISE";
case ASSUMPTION_R:
return "ASSUMPTION";
case CONJUNCT_INTRO:
return "CONJUNCTION INTRODUCTION";
case DISJUNCT_INTRO:
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";
}
}
just_t init_just(justRule_t rule, int* references, int referencesCount) {
just_t just;
just.rule = rule;
just.references = references;
just.referencesCount = referencesCount;
return just;
}
|
