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.

References in zbMATH (referenced in 15 articles , 1 standard article )

Showing results 1 to 15 of 15.
Sorted by year (citations)

  1. Reger, Giles; Tishkovsky, Dmitry; Voronkov, Andrei: Cooperating proof attempts (2015)
  2. Rager, David L.; Hunt, Warren A. jun.; Kaufmann, Matt: A parallelized theorem prover for a logic with parallel execution (2013)
  3. Letichevsky, A. A.; German, V. N.; Morokhovets, M. K.; Shchogoleva, N. N.: Parallel inference search in logical calculus based on the algebraic programming system (2010)
  4. Letz, Reinhold; Stenz, Gernot: Model elimination and connection tableau procedures (2001)
  5. Bonacina, Maria Paola: A taxonomy of parallel strategies for deduction (2000)
  6. Schumann, Johann: Automated theorem proving in high-quality software design (2000)
  7. Schumann, Johann M.: Automated theorem proving in software engineering. Foreword by Donald Loveland (2000)
  8. Sturgill, David; Segre, Alberto Maria: Nagging: A distributed, adversarial search-pruning technique applied to first-order inference (1997)
  9. Reed, David W.; Loveland, Donald W.: Near-Horn Prolog and the ancestry family of procedures (1995)
  10. Bonacina, Maria Paola; Hsiang, Jieh: Parallelization of deduction strategies: An analytical study (1994) ioport
  11. Schumann, J.: Tableau-based theorem provers: Systems and implementations (1994) ioport
  12. Sturgill, David B.; Segre, Alberto Maria: A novel asynchronous parallelism scheme for first-order logic (1994)
  13. McCune, William; Wos, Larry: Experiments in automated deduction with condensed detachment (1992)
  14. Stickel, Mark E.: A Prolog technology theorem prover: A new exposition and implementation in Prolog (1992)
  15. Schumann, J.; Letz, R.: PARTHEO: A high-performance parallel theorem prover (1990)