ROO: Radically Optimized Otter

ROO

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.

	      Dr J K Slaney                       Phone (Aus.):  (026) 125 8607
	      Theory Group                        Phone (Int.): +61 26 125 8607
	      Research School of Computer Science Fax (Aus.):    (026) 125 8651
	      Australian National University      Fax (Int.):   +61 26 125 8651
	      Canberra, ACT, 0200, AUSTRALIA