Cooperation in Theorem Proving by Loosely Coupled Heuristics

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.