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.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
Butler, R. M., and N. T. Karonis, “Exploitation of Parallelism in Prototypical Deduction Problems”, Proceedings of the 9th International Conference on Automated Deduction, E. L. Lusk and R. A. Overbeek, (Eds.) Springer-Verlag Lecture Notes in Computer Science #310 (1987), pp. 333–343.
Dunn, J. M., The Algebra of Intensional Logics, doctoral dissertation (unpublished), University of Pittsburg, 1966.
Dunn, J. M., “Relevance Logic and Entailment”, Gabbay, D, & Günthner, F (eds), Handbook of Philosophical Logic, Vol. 3, Dordrecht, Reidel, 1986.
Jindal, A., R. Overbeek, and W. Kabat, “Exploitation of Parallel Proceessing for Implementing High-Performance Deduction Systems”, Journal of Automated Reasoning, to appear.
Boyle, J., Butler, R., Disz, T., Glickfeld, B., Lusk, E., Overbeek, R., Patterson, J., and Stevens, R., Portable Programs for Parallel Processors, New York, Holt, Rinehart & Winston, 1987.
Lusk, E. and McFadden, R., “Using Automated Reasoning Tools: A Study of the Semigroup F2B2”, Semigroup Forum 36, no. 1 (1987), pp. 75–88.
McCune, W. W., “OTTER 1.0 Users' Guide”, Report ANL-88-44, Argonne National Laboratory, Argonne, Illinois.
Meyer, R. K., “Sentential Constants in R and R¬”, Studia Logica 45 (1986), pp. 301–327.
Slaney, J. K., “3088 Varieties: A Solution to the Ackermann Constant Problem”, Journal of Symbolic Logic 50 (1984), pp. 487–501.
Slaney, J. K., “On the Structure of DeMorgan Monoids, With Corollaries on Relevant Logic and Theories”, Notre Dame Journal of Formal Logic 30 (1989), pp. 117–129.
Slaney, J. K., “The Ackermann Constant Theorem: A Computer-Assisted Investigation”, Journal of Automated Reasoning, forthcoming.
Wos, L., D. Carson, and G. Robinson, “Efficiency and completeness of the set-of-support strategy in theorem proving,” Journal of the ACM 14, (1965), pp. 536–541.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1990 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Slaney, J.K., Lusk, E.L. (1990). Parallelizing the closure computation in automated deduction. In: Stickel, M.E. (eds) 10th International Conference on Automated Deduction. CADE 1990. Lecture Notes in Computer Science, vol 449. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-52885-7_77
Download citation
DOI: https://doi.org/10.1007/3-540-52885-7_77
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-52885-2
Online ISBN: 978-3-540-47171-4
eBook Packages: Springer Book Archive