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

DOI10.1006/JSCO.1995.1014zbMath0836.68105OpenAlexW1981878423MaRDI QIDQ1895413

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)

Related Items (4)

On subsumption in distributed derivations ⋮ Fine-grained concurrent completion ⋮ Octopus: combining learning and parallel search ⋮ Aquarius

Uses Software

• Unnamed Item

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