Affiliations: Department of Computer Science, University of Iowa, Iowa City, IA 52242-1419, U.S.A., bonacina@cs,uiowa.edu | Department of Computer Science, National Taiwan University, Taipei, Taiwan, hsiang@csie.ntu.edu.tw
Note: [] Supported in part by the GE Foundation Faculty Fellowship to the University of Iowa.
Note: [] Supported in part by grant NSC 83-0408-E-002-012T of the National Science Council of the Republic of China.
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.
