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
    0 references
    0 references
    0 references
    0 references
    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
    0 references
    resolution
    0 references
    Prolog
    0 references
    model elimination
    0 references
    or-parallelism
    0 references