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
|
#ifndef PROPOSITION
#define PROPOSITION
#include "lexer.h"
typedef struct Proposition {
char isSimple;
char isNegative;
char isContradiction;
struct Proposition* propA;
struct Proposition* propB;
tokenType_t relation;
char* name;
} 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,
ASSUMPTION_R,
CONJUNCT_INTRO,
DISJUNCT_INTRO,
IMPLICATION_INTRO,
BI_IMPLICATION_INTRO,
NEGATION_INTRO,
CONTRADICTION_INTRO,
CONJUNCT_ELIM,
DISJUNCT_ELIM,
IMPLICATION_ELIM,
BI_IMPLICATION_ELIM,
NEGATION_ELIM
} justRule_t;
char* jrtos(justRule_t rule);
typedef struct Justification {
justRule_t rule;
int* references;
int referencesCount;
} just_t;
just_t init_just(justRule_t rule, int* references, int referencesCount);
#endif
|
