This is the abstract of the paper:
Ewing L Lusk, William W McCune and John K Slaney.
ROO: A Parallel Theorem Prover.
Proceedings of the eleventh Conference on Automated Deduction (CADE-11) 15 (1992): 731-734
In [CADE-10] 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, 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.
Parallelizing the Closure Computation
This is the abstract of the paper:
John Slaney and Ewing Lusk.
Parallelizing the Closure Computation in Automated Deduction.
Proceedings of the tenth Conference on Automated Deduction (CADE-10) (1992): 28-39
In this paper we present a parallel algorithm for computing the closure of a set under an operation. This particular type of computation appears in a variety of disguises, and has been used in automated theorem proving, abstract algebra and formal logic. The algorithm we give here is particularly suited for shared-memory parallel computers, where it makes possible economies of space. Implementations of the algorithm in two application contexts are described and experimental results given.
Automated Reasoning Group
Computer Sciences Laboratory
Research School of Information Sciences and Engineering
Australian National University