/*
 * @(#) nlogprov.c - Automatic formula prover for natural logic.
 * (c) 1996 Ivan Maidanski <ivmai@chat.ru> 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 <stdlib.h>
#include <stdio.h>
#include <string.h>

#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)
   goto save;
  goto undo;
 test:
  if (top<depth)
   goto level;
  if (mark<0 || mark>=(r=getmark(list,goal)))
   goto undo;
 save:
  mark=r; printf("(Mark: %d)\n",mark);
  for (r=0;r<depth;r++)
   best[r]=rulerec[r];
 undo:
  top--;
  undoapplyrule(list,rulerec[top]);
 other:
  rulerec[top]++;
  if (rulerec[top])
   goto add;
  if (top>0)
   goto undo;
  if (!mark)
  {
   printf("\nCannot prove!\n");
   exit(0);
  }
  mark=mark<0? -mark : depth;
  for (r=0;r<mark;r++)
   rulerec[r]=best[r];
  return (mark);
}

void printsequence(struct tlist *list,int rulerec[],int count)
{
 int step,n;
 struct tlist *cur=list->next;
 for (step=0;cur->form;step++,cur=cur->next);
 for (n=0;n<count;n++,step++)
 {
  printf("%d. ",step+1);
  applyrule(list,rulerec[n]);
  if (rulerec[n]<step)
   printf("[%d] ",step-rulerec[n]);
   else printf("[axiom] ");
  printformula(list->next->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);
}