We present a methodology for achieving cooperation between already existing theorem provers employing different proof paradigms and/or different search controls, and using different but related logics. Cooperation between the provers is achieved by periodically interchanging clauses which are selected by so-called referees. By employing referees both on the side of a sending prover and a receiving prover the communication is both success- and demand-driven, which results in a rather small communication overhead and synergetical effects.
We report on experiments regarding the cooperation of the provers SPASS, SETHEO and \discount\ in domains of the TPTP library and with problems stemming from an application in software component retrieval. The experiments show significant improvements in the number of problems solved as well as in the solution times.
Generated: 29/10/99