SPTHEO swMATH ID: 21561 Software Authors: Suttner, Christian B. Description: 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. Homepage: https://link.springer.com/article/10.1023/A:1005868304990 Keywords: SPTHEO; SETHEO Related Software: SETHEO; GETFOL; BREAKUP; OTTER; TPTP; Aquarius; METEOR; PARTHENON; Peers-mcd; HERBY; Bliksem; DISCOUNT; EQP; Roo; Octopus; SicoTHEO; SPASS; TGTP; PLAGIATOR Cited in: 3 Publications Standard Articles 2 Publications describing the Software, including 1 Publication in zbMATH Year SPS-parallelism+SETHEO=SPTHEO. Zbl 0929.68111Suttner, Christian B. 1999 A parallel theorem prover SPTHEO. Suttner, Christian B. 1997 Cited by 5 Authors 1 Amir, Eyal 1 McIlraith, Sheila A. 1 Newborn, Monty 1 Suttner, Christian B. 1 Wang, Zongyan Cited in 2 Serials 2 Journal of Automated Reasoning 1 Artificial Intelligence Cited in 1 Field 3 Computer science (68-XX) Citations by Year