Parallelizing the closure computation in automated deduction
John K. Slaney1
and Ewing L. Lusk2 
| (1) |
Automated Reasoning Project, Australian National University, Australia |
| (2) |
Mathematics and Computer Science Division, Argonne National Laboratory, USA |
Abstract
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.
This work was supported by the Applied Mathematical Sciences subprogram of the Office of Energy Research, U.S. Department of Energy, under contract W-31-109-Eng-38.
References secured to subscribers.