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). ...
Keywords for this software
References in zbMATH (referenced in 6 articles )
Showing results 1 to 6 of 6.
- Rager, David L.; Hunt, Warren A.jun.; Kaufmann, Matt: A parallelized theorem prover for a logic with parallel execution (2013)
- Melis, Erica; Meier, Andreas; Siekmann, Jörg: Proof planning with multiple strategies (2008)
- Newborn, Monty; Wang, Zongyan: Octopus: combining learning and parallel search (2004)
- Schumann, Johann: Automated theorem proving in high-quality software design (2000)
- Schumann, Johann M.: Automated theorem proving in software engineering. Foreword by Donald Loveland (2000)
- Schumann, Johann; Wolf, Andreas; Suttner, Christian: Parallel theorem provers based on SETHEO (1998)