Coupling Saturation-Based Provers by Exchanging 
Positive/Negative Information

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

Abstract
We examine different possibilities of coupling 
saturation-based theorem provers by exchanging 
positive/negative information. We
discuss which positive or negative information is well-suited 
for cooperative theorem proving and show in an
abstract way how this information can be used. Based on this 
study, we introduce a basic model for cooperative theorem
proving. We present theoretical results regarding the exchange 
of positive/negative information as well as
practical methods and heuristics  that allow for a gain of 
efficiency in comparison with sequential provers.
Finally, we report on experimental studies conducted in the 
areas condensed detachment, unfailing completion,
and superposition.

Keywords
theorem proving, cooperation, positive/negative information