Distributed deduction by clause-diffusion: Distributed contraction and the Aquarius prover

DOI10.1006/JSCO.1995.1014MaRDI QIDQ1895413zbMATHOpenAlexFDO

Authors Maria Paola Bonacina, Jieh Hsiang

Publication date 11 April 1996

Published in Journal of Symbolic Computation (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1006/jsco.1995.1014

zbMATH Keywords

theorem proverAquariusbackward contraction bottleneckclause-diffusiondistributed global construction

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Recommendations

• scientific article; zbMATH DE number 794244
• PARTHENON: A parallel theorem prover for non-horn clauses
• scientific article; zbMATH DE number 1254024
• The clause-diffusion theorem prover Peers-mcd (system description)
• scientific article; zbMATH DE number 512823

Cited in

(7)

• scientific article; zbMATH DE number 794244 (Why is no real title available?)
• On subsumption in distributed derivations
• Octopus: combining learning and parallel search
• Aquarius
• Distributing equational theorem proving
• Fine-grained concurrent completion
• The clause-diffusion theorem prover Peers-mcd (system description)

Describes a project that uses

Uses Software

• OTTER

This page was built for publication: Distributed deduction by clause-diffusion: Distributed contraction and the Aquarius prover

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1895413)