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 }