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

DOI10.1006/JSCO.1995.1014MaRDI QIDQ1895413zbMATH OpenOpenAlexFDO

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

Aquariusbackward contraction bottleneckclause-diffusiondistributed global constructiontheorem prover

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

(9)

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

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)