SPS-parallelism+SETHEO=SPTHEO. This paper describes the parallel automated theorem prover SPTHEO, a parallelization of the sequential first-order theorem prover SETHEO. The parallelization is based on the SPS-model (Static Partitioning with Slackness) for parallel search, an approach that minimizes the processor-to-processor communication. This model allows efficient computations on hardware with weak communication performance, such as workstation networks. SPTHEO offers the utilization of both OR- and independent-AND parallelism. In this paper, a detailed description and evaluation of the OR-parallel part are given.
Keywords for this software
References in zbMATH (referenced in 4 articles , 2 standard articles )
Showing results 1 to 4 of 4.
- Amir, Eyal; McIlraith, Sheila: Partition-based logical reasoning for first-order and propositional theories (2005)
- Newborn, Monty; Wang, Zongyan: Octopus: combining learning and parallel search (2004)
- Suttner, Christian B.: SPS-parallelism+SETHEO=SPTHEO (1999)
- Suttner, Christian B.: A parallel theorem prover SPTHEO. (1997) ioport