Coupling Saturation-Based Provers by Exchanging Positive/Negative Information

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.