This paper describes a methodology for parallel theorem proving in a distributed environment,called deduction by Clause-Diffusion. This methodology utilizes parallelism at the search level, by having concurrent, asynchronous deductive processes searching in parallel the search space of the problem. The search space is partitioned among the processes by distributing the clauses and by subdividing certain classes of inferences. The processes communicate by exchanging data. Policies for distributing the clauses and for scheduling inference and communication steps complete the picture. A distributed derivation is made of the collection of the derivations computed by the concurrent deductive processes and it halts successfully as soon as one of them does. While the Clause-Diffusion methodology applies to theorem proving in general, it has been designed to provide solutions to the problems in the parallelization of contraction-based strategies, such as rewriting-based methods. We identify backward contraction, i.e. the task of maintaining clauses reduced in a dynamically changing data base, as the main obstacle in parallel theorem proving with contraction. In parallel implementations of contraction-based strategies in shared memory, this difficulty appears as a write-bottleneck, which we have termed the backward contraction bottleneck. The Clause-Diffusion approach avoids this problem by adopting a mostly distributed memory and distributed global contraction schemes. We conclude by reporting some of our results with an implementation of Clause-Diffusion.

The Clause-Diffusion methodology for distributed deduction

BONACINA, Maria Paola
;
1995-01-01

Abstract

This paper describes a methodology for parallel theorem proving in a distributed environment,called deduction by Clause-Diffusion. This methodology utilizes parallelism at the search level, by having concurrent, asynchronous deductive processes searching in parallel the search space of the problem. The search space is partitioned among the processes by distributing the clauses and by subdividing certain classes of inferences. The processes communicate by exchanging data. Policies for distributing the clauses and for scheduling inference and communication steps complete the picture. A distributed derivation is made of the collection of the derivations computed by the concurrent deductive processes and it halts successfully as soon as one of them does. While the Clause-Diffusion methodology applies to theorem proving in general, it has been designed to provide solutions to the problems in the parallelization of contraction-based strategies, such as rewriting-based methods. We identify backward contraction, i.e. the task of maintaining clauses reduced in a dynamically changing data base, as the main obstacle in parallel theorem proving with contraction. In parallel implementations of contraction-based strategies in shared memory, this difficulty appears as a write-bottleneck, which we have termed the backward contraction bottleneck. The Clause-Diffusion approach avoids this problem by adopting a mostly distributed memory and distributed global contraction schemes. We conclude by reporting some of our results with an implementation of Clause-Diffusion.
1995
Mechanical theorem proving; parallelization; search parallelism; contraction-based theorem proving; eager contraction
File in questo prodotto:
File Dimensione Formato  
FI1995cldif.pdf

accesso aperto

Descrizione: Articolo
Tipologia: Documento in Post-print
Licenza: Creative commons
Dimensione 279.18 kB
Formato Adobe PDF
279.18 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/300533
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 15
  • ???jsp.display-item.citation.isi??? ND
social impact