System description: cooperation in model elimination: CPTHEO

摘要

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 description we present a concept for a cooperative parallel theorem prover which combines goal oriented search with a saturating approach. This concept has been realized within a prototype of the automated theorem prover CPTHEO which is based on the Model Elimination (ME) prover SETHEO [5]. Moreover, we give a short assessment of the results of first experiments with CPTHEO, followed by a listing of topics planned for the future improvement of the prover.