Fourth Annual IEEE Symposium on

Logic in Computer Science (LICS 1989)

Paper: PARTHENON: a parallel theorem prover for nonHorn clauses (at LICS 1989)

Authors: Bose, S. Clarke, E.M. Long, D.E. Michaylov, S.


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


    author = 	 {Bose, S. and Clarke, E.M. and Long, D.E. and Michaylov, S.},
    title = 	 {PARTHENON: a parallel theorem prover for nonHorn clauses},
    booktitle =  {Proceedings of the Fourth Annual IEEE Symp. on Logic in Computer Science, {LICS} 1989},
    year =	 1989,
    editor =	 {Rohit Parikh},
    month =	 {June}, 
    pages =      {80--89},
    location =   {Pacific Grove, CA, USA}, 
    publisher =	 {IEEE Computer Society Press}