SicoTHEO

SiCoTHEO - Simple Competitive parallel Theorem Provers based on SETHEO. In this paper, we present SiCoTHEO, a zoo of parallel theorem provers for first order predicate logic. They are based on the sequential prover SETHEO. Parallelism is exploited by competition: on each processor, an identical copy of SETHEO tries to prove the entire formula. However, certain parameters which influence SETHEO’s behavior are set differently for each processor. As soon as one processor finds a proof, the entire system is stopped. Three different versions of SiCoTHEO are presented in this paper. We have used competition on completeness mode (parallel iterative deepening, SiCoTHEO-PID) and completeness bounds (parameterized combination of completeness bounds, SiCoTHEO-CBC), and on the search mode (top-down combined with bottom-up, SiCoTHEO-DELTA). ...