Aquarius is a distributed theorem prover for first order logic with equality, developed for a network of workstations. Given as input a theorem proving problem and a 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 number of variants of a general methodology for distributed deduction, called deduction by Clause-Diffusion, which appeared first in (Bonacina, 1992). 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 a brief outline of the Clause-Diffusion methodology, with emphasis on the problem of distributed global contraction, e.g. normalization with respect to a distributed data base. We describe the schemes for performing distributed global contraction implemented in Aquarius, which avoid the backward contraction bottleneck of purely shared memory approaches to parallel deduction. Then, we describe Aquarius, its design, its features and user interface. We present a set of experiments conducted with Aquarius and we analyze the results. We conclude with some comparison and discussion.

Distributed deduction by Clause-Diffusion: distributed contraction and the Aquarius prover

BONACINA, Maria Paola
;
1995-01-01

Abstract

Aquarius is a distributed theorem prover for first order logic with equality, developed for a network of workstations. Given as input a theorem proving problem and a 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 number of variants of a general methodology for distributed deduction, called deduction by Clause-Diffusion, which appeared first in (Bonacina, 1992). 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 a brief outline of the Clause-Diffusion methodology, with emphasis on the problem of distributed global contraction, e.g. normalization with respect to a distributed data base. We describe the schemes for performing distributed global contraction implemented in Aquarius, which avoid the backward contraction bottleneck of purely shared memory approaches to parallel deduction. Then, we describe Aquarius, its design, its features and user interface. We present a set of experiments conducted with Aquarius and we analyze the results. We conclude with some comparison and discussion.
1995
Automated theorem proving; contraction-based theorem proving; asynchronous deductive processes
File in questo prodotto:
File Dimensione Formato  
JSC1995aquarius.pdf

accesso aperto

Descrizione: Articolo
Tipologia: Documento in Post-print
Licenza: Creative commons
Dimensione 203.03 kB
Formato Adobe PDF
203.03 kB Adobe PDF Visualizza/Apri

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: https://hdl.handle.net/11562/300527
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 9
  • ???jsp.display-item.citation.isi??? 6
social impact