PARTHEO
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.
Keywords for this software
References in zbMATH (referenced in 14 articles , 1 standard article )
Showing results 1 to 14 of 14.
Sorted by year (- Reger, Giles; Tishkovsky, Dmitry; Voronkov, Andrei: Cooperating proof attempts (2015)
- Rager, David L.; Hunt, Warren A.jun.; Kaufmann, Matt: A parallelized theorem prover for a logic with parallel execution (2013)
- 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)
- Letz, Reinhold; Stenz, Gernot: Model elimination and connection tableau procedures (2001)
- Bonacina, Maria Paola: A taxonomy of parallel strategies for deduction (2000)
- 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)
- Sturgill, David; Segre, Alberto Maria: Nagging: A distributed, adversarial search-pruning technique applied to first-order inference (1997)
- Reed, David W.; Loveland, Donald W.: Near-Horn Prolog and the ancestry family of procedures (1995)
- Bonacina, Maria Paola; Hsiang, Jieh: Parallelization of deduction strategies: An analytical study (1994) ioport
- Schumann, J.: Tableau-based theorem provers: Systems and implementations (1994) ioport
- McCune, William; Wos, Larry: Experiments in automated deduction with condensed detachment (1992)
- Stickel, Mark E.: A Prolog technology theorem prover: A new exposition and implementation in Prolog (1992)
- Schumann, J.; Letz, R.: PARTHEO: A high-performance parallel theorem prover (1990)