Stephanie Weirich
Research Apprentice, 1993 NPAC REU Program
Computer Science Major, Rice University

Chilukuri K. Mohan
Associate Professor, School of Computer and Information Science, Syracuse University
mohan@top.syr.edu

Propositional Logic

The object of propositional logic is to represent the connections between propositions or formulas and from them draw conclusions about them. A typical proposition might be "Lenin is alive." or "This is a proposition." Single propositions are represented as literals and the connection of literals is a clause. For example: Let P represent "Lenin is alive" and let Q represent "This is a proposition." P or Q represents the clause, "Lenin is alive or this is a proposition." Furthermore, the literal not P represents the clause, "Lenin is not alive." 




 Proof by Contradiction 
 

Given a set of clauses and a goal, it is possible to prove the goal clause 
is derivable from the given clauses if the negation of the goal clause 
implies a contradiction. Suppose I wanted to prove Lenin is alive. To 
do so I would assume that Lenin is dead and try to find a contradiction 
from that, i.e. He's standing here next to me, only living people stand 
next to me, living people are not dead, so Lenin can't be dead, he must 
be alive, etc.






 Genetic Algorithms 


Genetic Algorithms are used in optimization to find the best solution based on 
a number of parameters. They are, in essence, a metaphor to the natural
biological process of evolution.
A program utilizing such an algorithm will encode its 
parameters in "genes" which will make up many "chromosomes."Each chromosome 
will represent an entire solution to a problem, based upon the variations
within its genes.
The algorithm will then perform operations on the chromosomes to find the 
most optimal solution. Typical operations include crossover and mutation. 
Crossover is analogous to the biological process of mating, where the genes 
between two individuals are randomly combined to form an offspring. The new 
chromosome has a complete set of genes, some from each parent. Mutation is 
carried out by randomly changing a gene in an individual to form a new one 
asexually. Once a new population is formed, it is evaluated with the old one 
and each chromosome is assigned a fitness, describing how close it is to the 
optimal solution. Only the most fit individuals are retained for the next
generation, in a method similar to "survival of the fittest."












 Using Genetic Algorithms in Propositional Logic 


With proof by contradiction, propositional logic becomes a 
search problem. Automated reasoning programs search for the 
contradiction derived from a set of clauses. Such a contradiction 
arises from resolving two unit clauses such as  
P 
and 
not P.
Resolving clauses is simply comparing two with such opposite 
literals and drawing inferences from them. As a search problem, 
automated reasoning becomes suitable for some of the 
methodology of genetic algorithms. Each clause can be thought 
of as an individual chromosome, each literal a gene. Resolution 
becomes crossover as the new resultant clause will contain 
literals found in the parent clauses. e.g.  
not P or Q
and  
P or S
will resolve to 
Q or S. 
Since the contradiction arises from resolving 
two short unit length clauses together, the length of the clause 
serves as a measure of fitness. All clauses must be kept, but not 
all need to be resolved every generation, only the most fit ones. 
To simulate mutation, the clauses can't be changed either, but 
longer clauses which would not ordinarily have a high 
probability of being resolved can be considered.






 Parallel Processing 


Each processor contains chromosomes which mate with each other in parallel.
Diversity is maintained by passing new chromosomes between the processors.









Research paper

"Proof by Contradiction for Parallel Genetic Algorithms for Automated Reasoning"
 
in Bogucz, E.A., and Weinman, V.E., editors, 
"Journal of Undergraduate Research in High-Performance Computing," 
Volume 3, NPAC technical report SCCS-576, November 1993. 







 
1993 Research Experiences for Undergraduates Program
in High-Performance Computing,
Northeast Parallel Architectures Center, Syracuse University,
reu-info@npac.syr.edu