/* * @(#) nlogprov.c - Automatic formula prover for natural logic. * (c) 1996 Ivan Maidanski http://ivmai.chat.ru * Freeware program source. All rights reserved. ** * Language: ANSI C * Tested with: Watcom C compiler v10 * Last modified: 1996-05-18 19:35:00 GMT+04:00 */ /* Logic basis: (1 > (2 > 1)), ((1 > (2 > 3)) > ((1 > 2) > (1 > 3))), (((1 > 0) > 0) > 1). Reduction rules: |- A, |- (A > B) => |- B (modus ponens) |- A => |- S(A) |b/B */ #include #include #include #define MAXDEPTH 30 struct tform { struct tform *p; /* antecedent sub-tree */ union { struct tform *p; /* consequent sub-tree */ int v; /* leaf value */ } u; }; struct tlist { struct tform *form; struct tlist *next; }; char *axioms[]= { "(1 > (2 > 1))", "((1 > (2 > 3)) > ((1 > 2) > (1 > 3)))", "(((1 > 0) > 0) > 1)", "(0 > 1)", /* additional */ 0 }; void printformula(struct tform *form) { if (form->p) { printf("("); printformula(form->p); printf(">"); printformula(form->u.p); printf(")"); } else printf("%d",form->u.v); } void delformula(struct tform *form) { if (form->p) { delformula(form->p); delformula(form->u.p); } free((void *)form); } void delformlist(struct tlist *list) { struct tlist *p; while (list) { p=list; list=list->next; if (p->form) delformula(p->form); free((void *)p); } } struct tform *allocleaf(void) { struct tform *form=(struct tform *)malloc(sizeof(struct tform)); if (!form) { fprintf(stderr,"\nNo memory!\n"); exit(1); } return (form); } struct tlist *preparelist() { struct tlist *list=(struct tlist *)malloc(sizeof(struct tlist)); if (!list) { fprintf(stderr,"\nNo memory!\n"); exit(1); } list->form=0; list->next=0; return (list); } void addtolist(struct tlist *list) { struct tlist *p=(struct tlist *)malloc(sizeof(struct tlist)); if (!p) { fprintf(stderr,"\nNo memory!\n"); exit(1); } p->form=0; p->next=list->next; list->next=p; } struct tform *dubformula(struct tform *form) { struct tform *copy=allocleaf(); if (form->p) { copy->p=dubformula(form->p); copy->u.p=dubformula(form->u.p); } else { copy->p=0; copy->u.v=form->u.v; } return (copy); } struct tform *convertformula(char *s,char **last) { struct tform *form=allocleaf(); while (*s==' ') s++; if (*s==')') { fprintf(stderr,"\nUnexpected symbol \")\"!\n"); exit(2); } if (*s=='(') { form->p=convertformula(s+1,last); if (!(s=strchr(*last+1,'>'))) { fprintf(stderr,"\nSymbol \">\" not found!\n"); exit(2); } form->u.p=convertformula(s+1,last); if (!(*last=strchr(*last+1,')'))) { fprintf(stderr,"\nSymbol \")\" not found!\n"); exit(2); } } else { int v=0; if (*s<'0' || *s>'9') { fprintf(stderr,"\nNumeric value expected!\n"); exit(2); } while (*s>='0' && *s<='9') v=v*10+*s-'0',s++; form->p=0; form->u.v=v; *last=s-1; } return (form); } struct tlist *prepareformhist() { int i; char *pc; struct tlist *list=preparelist(); for (i=0;axioms[i];i++) { addtolist(list); list->next->form=convertformula(axioms[i],&pc); } addtolist(list); return (list); } int isdifferent(struct tform *form1,struct tform *form2) { if (form1->p && form2->p) return (isdifferent(form1->p,form2->p)+ isdifferent(form1->u.p,form2->u.p)); if (!form1->p && !form2->p) return (form1->u.v!=form2->u.v); return (1); } int isunique(struct tform *form,struct tlist *list) { while (list) if (!list->form || isdifferent(form,list->form)) list=list->next; else return (0); return (1); } void changeleaves(struct tform *form,struct tlist *list) { if (form->p) { changeleaves(form->p,list); changeleaves(form->u.p,list); } else if (form->u.v) { int n=form->u.v-1; struct tlist *scan; for (scan=list->next;n && scan;n--,scan=scan->next); if (scan && scan->form) if (scan->form->p) { form->p=dubformula(scan->form->p); form->u.p=dubformula(scan->form->u.p); } else form->u.v=scan->form->u.v; } } struct tlist *seeklist(struct tlist *list,int n) { for (;n>1 && list->next;n--,list=list->next); if (list->next) return (list->next); for (;n>0;n--,list=list->next) addtolist(list); return (list); } int createleaveslist(struct tform *pattern,struct tform *antecedent, struct tlist *leaves) { struct tlist *found; if (pattern->p) if (antecedent->p) return (createleaveslist(pattern->p,antecedent->p,leaves) && createleaveslist(pattern->u.p,antecedent->u.p,leaves)); else return (0); else if (!pattern->u.v) return (!antecedent->p && !antecedent->u.v); else if (!(found=seeklist(leaves,pattern->u.v))->form) { found->form=dubformula(antecedent); return (1); } else return (!isdifferent(found->form,antecedent)); } int createnameslist(struct tform *form,struct tlist *leaves,int start) { struct tlist *found; if (form->p) return (createnameslist(form->u.p,leaves, createnameslist(form->p,leaves,start))); if (form->u.v && !(found=seeklist(leaves,form->u.v))->form) { found->form=allocleaf(); found->form->p=0; found->form->u.v=start; start++; } return (start); } struct tform *reduceformula(struct tform *form,struct tform *antecedent) { struct tform *consequent; struct tlist *leaves=preparelist(); if (!createleaveslist(form->p,antecedent,leaves)) { delformlist(leaves); return (0); } consequent=dubformula(form->u.p); changeleaves(consequent,leaves); delformlist(leaves); leaves=preparelist(); createnameslist(consequent,leaves,1); changeleaves(consequent,leaves); delformlist(leaves); return (consequent); } int comparewithgoal(struct tform *tested,struct tform *goal) { struct tlist *leaves=preparelist(); int res=createleaveslist(tested,goal,leaves); delformlist(leaves); return (res); } int getmarksingle(struct tform *tested,struct tform *goal,int height) { int mark=0; { struct tlist *leaves=preparelist(); if (createleaveslist(tested,goal,leaves)) { int cnt=0; struct tlist *cur; for (cur=leaves->next;cur;cur=cur->next) cnt+=cur->form->p? 3 : 1; mark=cnt*100/height; } delformlist(leaves); } if (tested->p) mark+=getmarksingle(tested->u.p,goal,height+1); return (mark); } int getmark(struct tlist *list, struct tform *goal) { int mark=0; while ((list=list->next)->form) mark+=getmarksingle(list->form->u.p,goal,1); return (mark); } void applyaxiom(struct tlist *list,struct tlist *cur) { struct tlist *p=cur->next; cur->next=p->next; p->next=list->next; list->next=p; } int applyrule(struct tlist *list,int rule) { struct tlist *cur; for (cur=list->next;rule>0 && cur->form;rule--,cur=cur->next); if (cur->form) { struct tform *form=reduceformula(list->next->form,cur->form); if (form) if (isunique(form,list->next)) { addtolist(list); list->next->form=form; return (1); } else delformula(form); return (0); } for (;rule>0;rule--,cur=cur->next); if (!cur->next) return (-1); applyaxiom(list,cur); return (1); } void undoapplyrule(struct tlist *list,int rule) { struct tlist *cur; for (cur=list->next;rule>=0 && cur->form;rule--,cur=cur->next); if (cur->form) { delformula(list->next->form); cur=list->next; list->next=cur->next; free((void *)cur); } else { for (;rule>=0;rule--,cur=cur->next); applyaxiom(cur,list); } } int provegoal(struct tlist *list,struct tform *goal,int *rulerec,int depth) { int r; int top=0; int mark=0; int best[MAXDEPTH]; level: rulerec[top]=0; add: r=applyrule(list,rulerec[top]); if (r<0) rulerec[top]=-1; if (r!=1) goto other; top++; if (!comparewithgoal(list->next->form,goal)) goto test; r=-top; if (mark>=0 || mark=(r=getmark(list,goal))) goto undo; save: mark=r; printf("(Mark: %d)\n",mark); for (r=0;r0) goto undo; if (!mark) { printf("\nCannot prove!\n"); exit(0); } mark=mark<0? -mark : depth; for (r=0;rnext; for (step=0;cur->form;step++,cur=cur->next); for (n=0;nnext->form); printf("\n"); } for(cur=list;cur->next->form;cur=cur->next); applyaxiom(list,cur); printf("\n"); } struct tform *inputformula() { char *pc; char str[255]; struct tform *form; struct tlist *leaves=preparelist(); gets(str); form=convertformula(str,&pc); createnameslist(form,leaves,1); changeleaves(form,leaves); delformlist(leaves); return (form); } int main(int argc,char *argv[]) { struct tform *goal; struct tlist *history=prepareformhist(); int rulerec[MAXDEPTH]; int depth=argc>1? atoi(argv[1]) : 0; if (depth<5 || depth>MAXDEPTH) depth=10; printf("Natural Logic Formula Prover.\n"); printf(" (Depth of search: %d)\n",depth); printf("\nInput goal: "); goal=inputformula(); printf("\nSolution:\n"); do printsequence(history,&rulerec[0], provegoal(history,goal,&rulerec[0],depth)); while (!comparewithgoal(history->next->next->form,goal)); delformula(goal); delformlist(history); return (0); }