## Coupling Saturation-Based Provers by Exchanging Positive/Negative Information

• We examine different possibilities of coupling saturation-based theorem pro-vers by exchanging positive/negative information. We discuss which positive ornegative information is well-suited for cooperative theorem proving and show inan abstract way how this information can be used. Based on this study, we in-troduce a basic model for cooperative theorem proving. We present theoreticalresults regarding the exchange of positive/negative information as well as practi-cal methods and heuristics that allow for a gain of efficiency in comparison withsequential provers. Finally, we report on experimental studies conducted in theareas condensed detachment, unfailing completion, and superposition.The author was supported by the Deutsche Forschungsgemeinschaft (DFG).

### Weitere Dienste

Verfasserangaben: Dirk Fuchs urn:nbn:de:hbz:386-kluedo-3782 SEKI Report (97,7) Preprint Englisch 1999 1999 Technische Universität Kaiserslautern 03.04.2000 Fachbereich Informatik 0 Allgemeines, Informatik, Informationswissenschaft / 004 Informatik Standard gemäß KLUEDO-Leitlinien vor dem 27.05.2011

$Rev: 13581$