home *** CD-ROM | disk | FTP | other *** search
/ Simtel MSDOS 1992 June / SIMTEL_0692.cdr / msdos / ddjmag / ddj8804.arc / REIS.ARC / REIS.LST
File List  |  1980-01-01  |  10KB  |  200 lines
  1.  
  2.  
  3.  
  4.  
  5.  
  6.      /*      A Theorem Prover for Propositional Logic
  7.       *
  8.       *      This program uses the resolution principle restricted to
  9.       *  semantic clashes to prove theorems in propositional logic.
  10.       *  The premises and the negation of the conclusion must be entered
  11.       *  using 1, 0, and -1 to represent, respectively, the presence of a
  12.       *  variable in true form, the absence of a variable, and the
  13.       *  presence of a variable in negated form.  For example, a run
  14.       *  in which the following four clauses are used
  15.       *
  16.       *       p v ¬q v  r
  17.       *            q
  18.       *      ¬p v ¬q
  19.       *                ¬r
  20.       *
  21.       *  would look as follows:
  22.       *
  23.       *  enter number of clauses and variables
  24.       *  4 3
  25.       *  enter clauses
  26.       *  1  -1  1
  27.       *  0   1  0
  28.       * -1  -1  0
  29.       *  0   0 -1
  30.       *
  31.       *  The program would then respond with
  32.       *
  33.       *  initial clauses
  34.       *    1 -1  1      (1)
  35.       *    0  1  0      (2)
  36.       *   -1 -1  0      (3)
  37.       *    0  0 -1      (4)
  38.       *  resolvents
  39.       *    0 -1  0      (5 from 1, 3, 4)
  40.       *    0  0  0      (6 from 2, 5)
  41.       *  proof complete--empty clause generated
  42.       *
  43.       *      For each nucleus, the program searches for a set of electrons
  44.       *  that make up a semantic clash.  When it finds a semantic clash, it
  45.       *  generates the resolvent and then uses a recursive technique called
  46.       *  backtracking to find other sets of electrons that also make up
  47.       *  a semantic clash.  This implementation is compact but quite
  48.       *  slow.
  49.       *
  50.       *  Author:  A. J. Dos Reis
  51.       *           Dept. of Mathematics and Computer Science
  52.       *           College at New Paltz
  53.       *           New Paltz, N.Y. 12561
  54.       *--------------------------------------------------------------------
  55.       *     CONSTANTS
  56.       */
  57.      #define TRUE 1
  58.      #define FALSE 0
  59.      #define MAXCLAUSES 100
  60.      #define MAXVARS 10
  61.      #define ELECTRON -1
  62.      #define NUCLEUS 1
  63.      /*--------------------------------------------------------------------
  64.       *     GLOBAL VARIABLES
  65.       */
  66.      int clause[MAXCLAUSES][MAXVARS];     /* Holds clauses               */
  67.      int clausetype[MAXCLAUSES];          /* Holds type:  nuc or elec    */
  68.      int clashelec[MAXVARS];              /* Holds row numbers of electrons
  69.                                              that form a semantic clash  */
  70.      int nvars;                           /* Number of variables         */
  71.      int avail;                           /* Index of next avail row     */
  72.      int newclauses;                      /* TRUE if new resolvents
  73.                                              generated on last pass      */
  74.      int noemptyclause;                   /* TRUE if empty clause not
  75.                                              generated                   */
  76.      /*-------------------------------------------------------------------
  77.       *     main prompts for and inputs the clauses.  It then calls
  78.       *     findsemclash for each nucleus.  It continues until the
  79.       *     empty clause is generated or until no new resolvents are
  80.       *     generated.
  81.       */
  82.      main()
  83.      {
  84.         int nclauses;                     /* Number of clauses           */
  85.         int nuc;                          /* Index of nucleus            */
  86.         int i,j;                          /* Utility indices             */
  87.         printf("enter number of clauses and variables\n");
  88.         scanf("%d%d",&nclauses,&nvars);
  89.         printf("enter clauses\n");
  90.         for (i=0; i<nclauses; i++)        /* Read in clauses             */
  91.            {clausetype[i]=ELECTRON;
  92.             for (j=0; j<nvars; j++)
  93.                {scanf("%d",&clause[i][j]);
  94.                 if (clause[i][j]==1)
  95.                    clausetype[i]=NUCLEUS; /* Set clausetype accordingly  */
  96.                }
  97.            }
  98.         avail=nclauses;                   /* Keep track of next avail row*/
  99.         printf("initial clauses\n");      /* Print out initial clauses   */
  100.         for (i=0; i<nclauses; i++)
  101.            {for (j=0; j<nvars; j++)
  102.               printf("%3d",clause[i][j]);
  103.             printf("     (%1d)\n",i+1);
  104.            }
  105.         printf("resolvents\n");
  106.         noemptyclause=TRUE;               /* Initialize flag             */
  107.         do
  108.            {newclauses=FALSE;             /* Initialize flag             */
  109.             nuc=0;                        /* Start search from row 0     */
  110.             do
  111.                {if (clausetype[nuc]==NUCLEUS) /* Search for nucleus      */
  112.                   {for (i=0; i<nvars; i++) /* Initialize clashelec       */
  113.                       clashelec[i]=-99;
  114.                    findsemclash(0,nuc);   /* Look for all sem clashes    */
  115.                   }
  116.                 nuc++;                    /* Repeat for next clause      */
  117.                } while ((nuc<nclauses) && noemptyclause);
  118.            } while (newclauses && noemptyclause);
  119.         if (noemptyclause)                /* Failed to gen empty clause? */
  120.            printf("argument not valid\n");
  121.         else
  122.            printf("proof complete--empty clause generated\n");
  123.      }
  124.      /*-------------------------------------------------------------------
  125.       *     findsemclash searches for an electron which under semantic
  126.       *     resolution will eliminate the true literal in column truecol
  127.       *     of the nucleus in row nuc.  When it finds a satisfactory
  128.       *     electron, it recursively calls itself to find a electron that
  129.       *     eliminates the next true literal.  When a set of electrons
  130.       *     that forms a semantic clash is found, findsemclash generates
  131.       *     the resolvent instead of making a recursive call.  Then
  132.       *     it backtracks to find other sets that also form semantic clashes.
  133.       */
  134.      findsemclash(truecol,nuc)
  135.      {int col;                            /* Column index                */
  136.       int elec;                           /* Row number of electron      */
  137.       int goodelec;                       /* True if elec ok under
  138.                                              semantic resolution         */
  139.       int i,j;                            /* Utility indices             */
  140.       while (truecol<nvars)               /* Checked all columns of nuc? */
  141.         if (clause[nuc][truecol]==1)      /* Is this a true literal      */
  142.            {elec=0;                       /* Search for appropriate elec */
  143.             do
  144.                {if (clausetype[elec]==ELECTRON)
  145.                    {col=0;                /* check col-by-col if elec ok */
  146.                     goodelec=TRUE;
  147.                     while ((col<nvars) && goodelec)
  148.                        {if (              /* Satisfies sem resolution?   */
  149.                             ( (col<truecol) && (clause[elec][col]!=0))
  150.                                             ||
  151.                             ( (clause[nuc][col] * clause[elec][col]==-1)
  152.                                             !=
  153.                               (truecol==col))
  154.                            )
  155.                            goodelec=FALSE; /* Electron fails test        */
  156.                         col++;             /* Test next column           */
  157.                        }
  158.                     if (goodelec)         /* Electron passed test?       */
  159.                        {clashelec[truecol]=elec; /* Remember row number  */
  160.                         findsemclash(truecol+1,nuc); /* Recursive call   */
  161.                        }
  162.                    }
  163.                  elec++;                  /* Try next electron           */
  164.                } while ((elec<avail) && noemptyclause);
  165.             return;                       /* Backtrack                   */
  166.            }
  167.         else
  168.            truecol++;                     /* Continue search for true lit
  169.                                               in the nucleus             */
  170.       newclauses=TRUE;                    /* Get here only when a sem
  171.                                               clash is found             */
  172.       for (i=0; i<nvars; i++)             /* Copy nuc to new avail row   */
  173.         clause[avail][i]=clause[nuc][i];
  174.       for (i=0; i<nvars; i++)
  175.         {elec=clashelec[i];               /* Get row number of electron  */
  176.          if (elec!=-99)                   /* -99 means electron not needed
  177.                                               for the ith col            */
  178.             for (j=0; j<nvars; j++)       /* Generate the resolvent      */
  179.                {clause[avail][j]+=clause[elec][j];
  180.                 if (clause[avail][j]!=0)
  181.                    noemptyclause=TRUE;
  182.                 if (clause[avail][j]==-2)
  183.                     clause[avail][j]=-1;
  184.                }
  185.         }
  186.      noemptyclause=FALSE;                 /* Initialize flag            */
  187.      for (j=0; j<nvars; j++)              /* Check for empty clause     */
  188.         {printf("%3d",clause[avail][j]);
  189.          if (clause[avail][j])
  190.             noemptyclause=TRUE;           /* Reset if no empty clause   */
  191.         }
  192.      printf("     (%1d from %1d",avail+1,nuc+1); /* Print resolvent     */
  193.      for (i=0;i<nvars; i++)
  194.         if (clashelec[i]!=-99)            /* Print electron row numbers */
  195.                printf(", %1d",clashelec[i]+1);
  196.      printf(")\n");
  197.      clausetype[avail]=ELECTRON;          /* Set type of resolvent      */
  198.      avail++;                             /* Increment avail row index  */
  199.      }
  200.