]> mj.ucw.cz Git - misc.git/blob - proof.c
Merge branch 'master' of git+ssh://git.ucw.cz/home/mj/GIT/misc
[misc.git] / proof.c
1 #include <stdio.h>
2 #include <stdlib.h>
3 #include <string.h>
4
5 typedef struct formula fmla;
6
7 struct formula {
8         fmla *next;
9         int op;
10         int key;
11         fmla *arg[2];
12 };
13
14 #define OP_X 0
15 #define OP_Y 1
16 #define OP_NOT 2
17 #define OP_IMP 3
18
19 static void putf(fmla *a)
20 {
21         switch (a->op)
22         {
23         case OP_X:
24                 putchar('X');
25                 break;
26         case OP_Y:
27                 putchar('Y');
28                 break;
29         case OP_NOT:
30                 putchar('^');
31                 putf(a->arg[0]);
32                 break;
33         default:
34                 putchar('(');
35                 putf(a->arg[0]);
36                 putchar('>');
37                 putf(a->arg[1]);
38                 putchar(')');
39         }
40 }
41
42 static void duf(fmla *f)
43 {
44         putf(f);
45         putchar('\n');
46 }
47
48 static inline fmla *newf(int op, fmla *l, fmla *r)
49 {
50         fmla *f = malloc(sizeof(fmla));
51         f->op = op;
52         f->arg[0] = l;
53         f->arg[1] = r;
54         f->next = NULL;
55         switch (op) {
56         case OP_IMP:
57                 f->key = 313*l->key + 17*r->key + 2;
58                 break;
59         case OP_NOT:
60                 f->key = 1733*l->key + 5;
61                 break;
62         default:
63                 f->key = op + 1;
64         }
65         return f;
66 }
67
68 static inline int match(fmla *a, fmla *b)
69 {
70         int i;
71
72         if (a->op != b->op || a->key != b->key)
73                 return 0;
74         switch (a->op)
75         {
76         case OP_IMP:
77                 if (!match(a->arg[1], b->arg[1]))
78                         return 0;
79         case OP_NOT:
80                 if (!match(a->arg[0], b->arg[0]))
81                         return 0;
82         }
83         return 1;
84 }
85
86 #define G_DEPTH 3
87
88 fmla *head_depth[G_DEPTH+1];
89
90 void gen(void)
91 {
92         int i, j, k;
93         fmla *x, *y, *z, **h;
94
95         puts("Generator...");
96         duf(head_depth[1] = newf(OP_X, NULL, NULL));
97         duf(head_depth[1]->next = newf(OP_Y, NULL, NULL));
98         for(i=2; i<=G_DEPTH; i++) {
99                 printf("### depth %d\n", i);
100                 h = head_depth + i;
101                 x = head_depth[i-1];
102                 while (x) {
103                         z = newf(OP_NOT, x, NULL);
104                         duf(z);
105                         z->next = *h;
106                         *h = z;
107                         x = x->next;
108                 }
109                 for(j=1; j<i; j++) {
110                         x = head_depth[j];
111                         while (x) {
112                                 y = head_depth[i-j];
113                                 while (y) {
114                                         z = newf(OP_IMP, x, y);
115                                         duf(z);
116                                         z->next = *h;
117                                         *h = z;
118                                         y = y->next;
119                                 }
120                                 x = x->next;
121                         }
122                 }
123         }
124 }
125
126 fmla *flist;
127
128 #define A_DEPTH 20
129
130 void axi(void)
131 {
132         int i,j,k;
133         fmla *x, *y, *z, *w;
134
135         puts("Axiom #1...");
136         /* A->(B->A) */
137         for(i=1; i<=G_DEPTH; i++)
138                 for(j=1; j<=G_DEPTH; j++)
139                         if (2*i+j+2 <= A_DEPTH)
140                                 for(x = head_depth[i]; x; x=x->next)
141                                         for(y = head_depth[j]; y; y=y->next) {
142                                                 z = newf(OP_IMP, x, newf(OP_IMP, y, x));
143                                                 duf(z);
144                                                 z->next = flist;
145                                                 flist = z;
146                                         }
147
148         puts("Axiom #2...");
149         /* (A->(B->C)) -> ((A->B) -> (A->C)) */
150         for(i=1; i<=G_DEPTH; i++)
151                 for(j=1; j<=G_DEPTH; j++)
152                         for(k=1; k<=G_DEPTH; k++)
153                                 if (3*i+2*j+2*k+6 <= A_DEPTH)
154                                         for(x=head_depth[i]; x; x=x->next)
155                                                 for(y=head_depth[j]; y; y=y->next)
156                                                         for(z=head_depth[k]; z; z=z->next) {
157                                                                 w = newf(OP_IMP,
158                                                                         newf(OP_IMP, x, newf(OP_IMP, y, z)),
159                                                                         newf(OP_IMP,
160                                                                                 newf(OP_IMP, x, y),
161                                                                                 newf(OP_IMP, x, z)));
162                                                                 duf(w);
163                                                                 w->next = flist;
164                                                                 flist = w;
165                                                         }
166
167         puts("Axiom #3...");
168         /* (^A->^B)->(B->A) */
169         for(i=1; i<=G_DEPTH; i++)
170                 for(j=1; j<=G_DEPTH; j++)
171                         if (2*i+2*j+5 <= A_DEPTH)
172                                 for(x = head_depth[i]; x; x=x->next)
173                                         for(y = head_depth[j]; y; y=y->next) {
174                                                 z = newf(OP_IMP,
175                                                         newf(OP_IMP, newf(OP_NOT, x, NULL), newf(OP_NOT, y, NULL)),
176                                                         newf(OP_IMP, y, x));
177                                                 duf(z);
178                                                 z->next = flist;
179                                                 flist = z;
180                                         }
181 }
182
183 void derive(void)
184 {
185         fmla *x, *y, *last, *z;
186         int flag;
187
188         puts("Derived:");
189         for(last=flist; last->next; last=last->next)
190                 ;
191         do {
192                 puts("PASS");
193                 flag = 0;
194                 /* Modus Ponens: A, A->B =] B */
195                 for(x=flist; x; x=x->next)
196                         for(y=flist; y; y=y->next) {
197                                 if (x->op == OP_IMP &&
198                                     match(x->arg[0], y)) {
199                                         z = x->arg[1];
200                                         if (!z->next && z != last) {
201                                                 duf(z);
202                                                 last->next = z;
203                                                 last = z;
204                                                 flag = 1;
205                                         }
206                                 }
207                         }
208         } while (flag);
209 }
210
211 int main(void)
212 {
213         gen();
214         axi();
215         derive();
216         return 0;
217 }