Category : C Source Code
Archive   : PROVER.ZIP
Filename : PROVER.C

/* A Theorem Prover for Propositional Logic
*
* This program uses the resolution principle restricted to
* semantic clashes to prove theorems in propositional logic.
* The premises and the negation of the conclusion must be entered
* using 1, 0, and -1 to represent, respectively, the presence of a
* variable in true form, the absence of a variable, and the
* presence of a variable in negated form. For example, a run
* in which the following four clauses are used
*
* p v ªq v r
* q
* ªp v ªq
* ªr
*
* would look as follows:
*
* enter number of clauses and variables
* 4 3
* enter clauses
* 1 -1 1
* 0 1 0
* -1 -1 0
* 0 0 -1
*
* The program would then respond with
*
* initial clauses
* 1 -1 1 (1)
* 0 1 0 (2)
* -1 -1 0 (3)
* 0 0 -1 (4)
* resolvents
* 0 -1 0 (5 from 1, 3, 4)
* 0 0 0 (6 from 2, 5)
* proof complete--empty clause generated
*
* For each nucleus, the program searches for a set of electrons
* that make up a semantic clash. When it finds a semantic clash, it
* generates the resolvent and then uses a recursive technique called
* backtracking to find other sets of electrons that also make up
* a semantic clash. This implementation is compact but quite
* slow.
*
* Author: A. J. Dos Reis
* Dept. of Mathematics and Computer Science
* College at New Paltz
* New Paltz, N.Y. 12561
*--------------------------------------------------------------------
* CONSTANTS
*/
#define TRUE 1
#define FALSE 0
#define MAXCLAUSES 100
#define MAXVARS 10
#define ELECTRON -1
#define NUCLEUS 1
/*--------------------------------------------------------------------
* GLOBAL VARIABLES
*/
int clause[MAXCLAUSES][MAXVARS]; /* Holds clauses */
int clausetype[MAXCLAUSES]; /* Holds type: nuc or elec */
int clashelec[MAXVARS]; /* Holds row numbers of electrons
that form a semantic clash */
int nvars; /* Number of variables */
int avail; /* Index of next avail row */
int newclauses; /* TRUE if new resolvents
generated on last pass */
int noemptyclause; /* TRUE if empty clause not
generated */
/*-------------------------------------------------------------------
* main prompts for and inputs the clauses. It then calls
* findsemclash for each nucleus. It continues until the
* empty clause is generated or until no new resolvents are
* generated.
*/
main()
{
int nclauses; /* Number of clauses */
int nuc; /* Index of nucleus */
int i,j; /* Utility indices */
printf("enter number of clauses and variables\n");
scanf("%d%d",&nclauses,&nvars);
printf("enter clauses\n");
for (i=0; i {clausetype[i]=ELECTRON;
for (j=0; j {scanf("%d",&clause[i][j]);
if (clause[i][j]==1)
clausetype[i]=NUCLEUS; /* Set clausetype accordingly */
}
}
avail=nclauses; /* Keep track of next avail row*/
printf("initial clauses\n"); /* Print out initial clauses */
for (i=0; i {for (j=0; j printf("%3d",clause[i][j]);
printf(" (%1d)\n",i+1);
}
printf("resolvents\n");
noemptyclause=TRUE; /* Initialize flag */
do
{newclauses=FALSE; /* Initialize flag */
nuc=0; /* Start search from row 0 */
do
{if (clausetype[nuc]==NUCLEUS) /* Search for nucleus */
{for (i=0; i clashelec[i]=-99;
findsemclash(0,nuc); /* Look for all sem clashes */
}
nuc++; /* Repeat for next clause */
} while ((nuc } while (newclauses && noemptyclause);
if (noemptyclause) /* Failed to gen empty clause? */
printf("argument not valid\n");
else
printf("proof complete--empty clause generated\n");
}
/*-------------------------------------------------------------------
* findsemclash searches for an electron which under semantic
* resolution will eliminate the true literal in column truecol
* of the nucleus in row nuc. When it finds a satisfactory
* electron, it recursively calls itself to find a electron that
* eliminates the next true literal. When a set of electrons
* that forms a semantic clash is found, findsemclash generates
* the resolvent instead of making a recursive call. Then
* it backtracks to find other sets that also form semantic clashes.
*/
findsemclash(truecol,nuc)
{int col; /* Column index */
int elec; /* Row number of electron */

int goodelec; /* True if elec ok under
semantic resolution */
int i,j; /* Utility indices */
while (truecol if (clause[nuc][truecol]==1) /* Is this a true literal */
{elec=0; /* Search for appropriate elec */
do
{if (clausetype[elec]==ELECTRON)
{col=0; /* check col-by-col if elec ok */
goodelec=TRUE;
while ((col {if ( /* Satisfies sem resolution? */
( (col ||
( (clause[nuc][col] * clause[elec][col]==-1)
!=
(truecol==col))
)
goodelec=FALSE; /* Electron fails test */
col++; /* Test next column */
}
if (goodelec) /* Electron passed test? */
{clashelec[truecol]=elec; /* Remember row number */
findsemclash(truecol+1,nuc); /* Recursive call */
}
}
elec++; /* Try next electron */
} while ((elec return; /* Backtrack */
}
else
truecol++; /* Continue search for true lit
in the nucleus */
newclauses=TRUE; /* Get here only when a sem
clash is found */
for (i=0; i clause[avail][i]=clause[nuc][i];
for (i=0; i {elec=clashelec[i]; /* Get row number of electron */
if (elec!=-99) /* -99 means electron not needed
for the ith col */
for (j=0; j {clause[avail][j]+=clause[elec][j];
if (clause[avail][j]!=0)
noemptyclause=TRUE;
if (clause[avail][j]==-2)
clause[avail][j]=-1;
}
}
noemptyclause=FALSE; /* Initialize flag */
for (j=0; j {printf("%3d",clause[avail][j]);
if (clause[avail][j])
noemptyclause=TRUE; /* Reset if no empty clause */
}
printf(" (%1d from %1d",avail+1,nuc+1); /* Print resolvent */
for (i=0;i if (clashelec[i]!=-99) /* Print electron row numbers */
printf(", %1d",clashelec[i]+1);
printf(")\n");
clausetype[avail]=ELECTRON; /* Set type of resolvent */
avail++; /* Increment avail row index */
}