swMATH ID: 9981
Software Authors: Schumann, J., Letz, R.
Description: PARTHEO: A high-performance parallel theorem prover. PARTHEO, a sound and complete or-parallel theorem prover for first-order logic is presented. The proof calculus is model elimination. PARTHEO consists of a uniform network of sequential theorem provers communicating via message passing. Each sequential prover is implemented as an extension of Warren’s abstract machine. PARTHEO is written in parallel C and is running on a network of 16 transputers. The paper comprises a description of the system architecture, the theoretical background, details of the implementation, and results of performance measurements.
Homepage: http://link.springer.com/chapter/10.1007/3-540-52885-7_78
Related Software: SETHEO; METEOR; TPTP; SicoTHEO; OTTER; PARTHENON; Isabelle; ACL2; DISCOUNT; E-MaLeS; E Theorem Prover; Sledgehammer; VAMPIRE; APS; APS-1; Maude; PVS; HOT; Roo; Nuprl
Cited in: 13 Publications

Standard Articles

1 Publication describing the Software, including 1 Publication in zbMATH Year
PARTHEO: A high-performance parallel theorem prover. Zbl 0708.68076
Schumann, J.; Letz, R.

Citations by Year