Carnegie Mellon University

sorry, we can't preview this file

file.pdf (868.33 kB)

Parthenon: A Parallel Theorem Prover for Non-horn Clauses

Download (868.33 kB)
journal contribution
posted on 1986-01-01, 00:00 authored by Soumitra Bose, Edmund M Clarke, David E Long, Spiro Michaylov
A parallel resolution theorem prover, called Parthenon, that handles first-order logic is described. Parthenon is apparently the first general-purpose theorem prover to be developed for a multiprocessor. The system is based on a modification of D.H.D. Warren's SRI model (Int. Symp. on Logic Prog., pp.92-101, 1987) for OR-parallelism and implements a variant of D.W. Loveland's (J. ACM, vol.15, pp.236-51, 1968) model elimination procedure. It has been evaluated on various shared memory multiprocessors, including a 16-processor Encore Multimax. The authors have found that typical theorem-proving problems exhibit a great deal of potential parallelism. Parthenon has been able to exploit much of this parallelism, producing both impressive absolute run times and near-linear speed-up curves


Publisher Statement

All Rights Reserved



Usage metrics