Cooperative Parallel Automated Theorem Proving

Automated Theorem Proving can be interpreted as the solution of search problems which comprise huge search spaces. Parallelization of the proof task as well as cooperation between the involved provers offer the possibility to develop more efficient search procedures. In this paper we want to investigate concepts for the development of cooperative parallel theorem provers. We deal with architectural questions as well as with possibilities of how to realize cooperation. Particularly, we discuss requirements on an efficient load distribution mechanism for cooperative parallel theorem provers. As a result of this discussion we develop the model of the new prover CPTHEO. This prover allows for a dynamic load distribution that fulfills the requirements introduced before. Furthermore, the cooperation possibilities of CPTHEO offer the potential for reaching superlinear speed-ups.     «

Automated Theorem Proving can be interpreted as the solution of search problems which comprise huge search spaces. Parallelization of the proof task as well as cooperation between the involved provers offer the possibility to develop more efficient search procedures. In this paper we want to investigate concepts for the development of cooperative parallel theorem provers. We deal with architectural questions as well as with possibilities of how to realize cooperation. Particularly, we discuss re...     »