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

DOI10.1006/JSCO.1995.1014zbMATH Open0836.68105OpenAlexW1981878423MaRDI QIDQ1895413FDOQ1895413

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

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

zbMATH Keywords

theorem proverAquariusbackward contraction bottleneckclause-diffusiondistributed global construction

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Cited In (7)

• Octopus: combining learning and parallel search
• The clause-diffusion theorem prover Peers-mcd (system description)
• Aquarius
• Distributing equational theorem proving
• Fine-grained concurrent completion
• On subsumption in distributed derivations
• Title not available (Why is that?)

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)