Exploitation of parallelism in prototypical deduction problems

Abstract

In this paper we consider two computations: the calculation of the elements in a finite semigroup and a theorem prover for propositional logic. As a first step towards exploitation of multiprocessors for more general deduction systems, we implemented portable programs to perform each of these tasks. The programs utilize both loosely-coupled multiprocessors (using message passing) and tightly-coupled multiprocessors using shared-memory. We believe that the basic algorithms developed here will carry over to the more general case of deduction systems for the predicate calculus and to rewrite systems as well. Indeed, the algorithms have been applied to a first-order deduction system developed by William McCune. In one experiment on that system we successfully derived a proof of Sam's lemma (a classic benchmark problem) in under 13 seconds using 12 processors on an Encore Multimax.