Knowledge-based Cooperation between Theorem Provers by TECHS

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.