Introduction

In [7] Slaney and Lusk described a parallel algorithm for computing the closure of a set under an operation and presented several application areas. In this paper we describe the application to automated theorem proving, which can be viewed as the computation of the closure of a set of clauses under a set of inference rules. In particular, we have applied the parallel closure algorithm to OTTER [5], currently the fastest sequential theorem proving system for large problems. The result is ROO (Radical Otter Optimization, with Australian origins), a parallel theorem prover compatible with OTTER and capable of near-linear speedup over OTTER on shared memory multiprocessors.

OTTER's collection of theorem-proving tools includes both back subsumption and back demodulation, which are crucial for Knuth-Bendix completion runs. Each of these in turn involves deletion from the central database, a operation not contemplated in [7]. We describe here the problems engendered by deletion and our solution to these problems, which not only allows the back subsumption and back demodulation operations, but allows them to proceed in parallel with the other operations of ROO.

An unanticipated problem that arose during the implementation was that of balancing memory usage among several processes. We describe the problem and its solution.

We present results on a variety of difficult theorem-proving problems, comparing ROO running on multiple processors with ROO on one processor, OTTER, and (where possible) with other theorem provers, both sequential and parallel. We use some newly-developed graphical tools to provide insight into both the good and bad performance of ROO. We attempt to identify the classes of problems for which sub-linear speedups can expected as well as those for which ROO appears to perform systematically well.

The paper is organized as follows. In Section we treat the case without deletion. This is a straightforward application of the parallel closure algorithm described in [7] to OTTER. We present a simplified version of OTTER's theorem-proving algorithm and present the parallel closure algorithm in the theorem-proving context. This yields a simplified version of ROO. We then present some results obtained with this version.

In Section we describe the problems introduced by deletion and their solutions. We then present some results using the full-featured ROO.

In the final section we draw conclusions and discuss problems remaining in the area of parallel automated deduction.