Cooperation in Theorem Proving by Loosely Coupled Heuristics

Dirk Fuchs, Joerg Denzinger
Fachbereich Informatik
Universitaet Kaiserslautern
Postfach 3049
67653 Kaiserslautern
Germany
E-mail: dfuchs@informatik.uni-kl.de
        denzinge@informatik.uni-kl.de

Abstract
We present a cooperation concept for automated theorem provers 
that is based on a periodical interchange of selected results
between several incarnations of a prover. These incarnations
differ from each other in the search heuristic they employ 
for guiding the search of the prover.  Depending on the 
strengths' and weaknesses of these heuristics different
knowledge and different communication structures are used 
for selecting the results to interchange.

Our concept is easy to implement and can easily be integrated 
into already existing theorem provers. Moreover, the 
resulting cooperation allows the distributed system to find 
proofs much faster than single heuristics working
alone. We substantiate these claims by two case studies: 
experiments with the \dicode\ system that is based on the 
condensed detachment rule and experiments with the \spass\ 
system, a prover for first order logic with equality based on
the superposition calculus. Both case studies show the 
improvements by our cooperation concept.

Keywords
theorem proving, cooperation, heuristicsSource
anonymous FTP server ftp.uni-kl.de [131.246.94.94]
path: /reports_uni-kl/computer_science/SEKI/1997/
file: Fuchs.SR-97-03.ps.gz