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
References in zbMATH (referenced in 7 articles )
Showing results 1 to 7 of 7.
- Kazakov, Yevgeny; Krötzsch, Markus; Simančík, František: The incredible ELK. From polynomial procedures to efficient reasoning with $\mathcal EL$ ontologies (2014)
- Newborn, Monty; Wang, Zongyan: Octopus: combining learning and parallel search (2004)
- Voronkov, Andrei: Algorithms, datastructures, and other issues in efficient automated deduction (2001)
- Bonacina, Maria Paola: A taxonomy of parallel strategies for deduction (2000)
- Astrachan, Owen: METEOR: Exploring model elimination theorem proving (1994)
- Lusk, Ewing L.; McCune, William W.: Uniform strategies: The CADE-11 theorem proving contest (1993)
- McRobbie, Michael A.: Automated reasoning and nonclassical logics: Introduction (1991)