Aquarius is a distributed theorem prover for first order logic with equality, developed for a network of workstations. Given in input a theorem proving problem and the number n of active nodes, Aquarius creates n deductive processes, one on each workstation, which work cooperatively toward the solution of the problem. Aquarius realizes a specific variant of a general methodology for distributed deduction, which we have called deduction by Clause-Diffusion and described in full in the first author's PhD thesis. The subdivision of the work among the processes, their activities and their cooperation are defined by the Clause-Diffusion method. Aquarius incorporates the sequential theorem prover Otter, in such a way that Aquarius implements the parallelization, according to the Clause-Diffusion methodology, of all the strategies provided in Otter. In this paper we give first an outline of the Clause-Diffusion methodology. Next, we consider in more detail the problem of distributed global contraction, e.g. normalization with respect to a distributed data base. The Clause-Diffusion methodology comprises a number of schemes for performing distributed global contraction, which avoid the backward contraction bottleneck of purely shared memory approaches to parallel deduction. Then, we describe Aquarius, its features and we analyze some of the experiments conducted so far. We conclude with some comparison and discussion.

Distributed deduction by Clause-Diffusion: the Aquarius prover

BONACINA, Maria Paola;
1993

Abstract

Aquarius is a distributed theorem prover for first order logic with equality, developed for a network of workstations. Given in input a theorem proving problem and the number n of active nodes, Aquarius creates n deductive processes, one on each workstation, which work cooperatively toward the solution of the problem. Aquarius realizes a specific variant of a general methodology for distributed deduction, which we have called deduction by Clause-Diffusion and described in full in the first author's PhD thesis. The subdivision of the work among the processes, their activities and their cooperation are defined by the Clause-Diffusion method. Aquarius incorporates the sequential theorem prover Otter, in such a way that Aquarius implements the parallelization, according to the Clause-Diffusion methodology, of all the strategies provided in Otter. In this paper we give first an outline of the Clause-Diffusion methodology. Next, we consider in more detail the problem of distributed global contraction, e.g. normalization with respect to a distributed data base. The Clause-Diffusion methodology comprises a number of schemes for performing distributed global contraction, which avoid the backward contraction bottleneck of purely shared memory approaches to parallel deduction. Then, we describe Aquarius, its features and we analyze some of the experiments conducted so far. We conclude with some comparison and discussion.
9783540572350
Automated theorem proving, Distributed deduction, Clause-Diffusion, Aquarius theorem prover
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: http://hdl.handle.net/11562/16055
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 10
  • ???jsp.display-item.citation.isi??? ND
social impact