Roo: a parallel theorem prover. 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.

Keywords for this software

Anything in here will be replaced on browsers that support the canvas element