PARTHENON: A parallel theorem prover for non-horn clauses (Q1189725)
From MaRDI portal
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | PARTHENON: A parallel theorem prover for non-horn clauses |
scientific article |
Statements
PARTHENON: A parallel theorem prover for non-horn clauses (English)
0 references
27 September 1992
0 references
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.
0 references
resolution
0 references
Prolog
0 references
model elimination
0 references
or-parallelism
0 references