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