Knowledge-based Cooperation between Theorem Provers by TECHS 

Dirk Fuchs, J\"org Denzinger
Fachbereich Informatik, Universitaet Kaiserslautern
Postfach 3049, 67653 Kaiserslautern
Germany
E-mail: dfuchs@informatik.uni-kl.de
        denzinge@informatik.uni-kl.de

Abstract
We present a methodology for coupling several saturation-based 
theorem provers (running on different computers).
The methodology is well-suited for realizing cooperation between
different incarnations of one basic prover. Moreover, also
different heterogeneous provers --that differ from each other 
in the calculus and in the heuristic they employ--
can be coupled.
Cooperation between the different provers is achieved by
periodically interchanging clauses which are selected by 
so-called referees.
We present theoretic results regarding the completeness of the 
system of cooperating provers as well as describe concrete 
heuristics for designing referees. Furthermore, we report on 
two experimental studies performed with
homogeneous and heterogeneous provers in the areas superposition 
and unfailing completion. The results reveal that the occurring 
synergetic effects lead to a significant improvement of 
performance.

Keywords
theorem proving, cooperation, heterogeneous teams