PARTHENON: A parallel theorem prover for non-horn clauses (Q1189725)

The paper describes a parallel resolution theorem prover, PARTHENON, which is able to handle first order formulas in clause form. PARTHENON is the first general theorem prover based on or-parallel versions of Prolog. As the inference mechanism the Loveland's model elimination procedure was chosen for the theorem prover. The model elimination procedure is fully described in Section 2. Section 3 discusses various implementations of or-parallelism on shared memory multiprocessors. An overview of the system is given in Section 4. The following three sections describe key elements of the design in more detail. Section 8 discusses the performance of PARTHENON on some examples. The concluding Section 9 contains some observations on the role of parallelism in automatic theorem proving for future research.