Abstract
With random competition we propose a method for parallelizing arbitrary theorem provers. We can prove high efficiency (compared with other parallel theorem provers) of random competition on highly parallel architectures with thousands of processors. This method is suited for all kinds of distributed memory architectures, particularly for large networks of high performance workstations since no communication between the processors is necessary during run-time. On a set of examples we show the performance of random competition applied to the model elimination theorem prover SETHEO.
Besides the speedup results for random competition our theoretical analysis gives fruitful insight in the interrelation between search-tree structure, run-time distribution and parallel performance of OR-parallel search in general.
This is a preview of subscription content, log in via an institution.
We’re sorry, something doesn't seem to be working properly.
Please try refreshing the page. If that doesn't work, please contact support so we can address the problem.
Preview
Unable to display preview. Download preview PDF.
References
K. A. M. Ali. Or-parallel execution of PROLOG on a multi-sequential machine. Int. Journal of Parallel Programming, 15(3):189–214, 1987.
W. Ertel. Random Competition: A Simple, but Efficient Method for Parallelizing Inference Systems. In B. Fronhöfer and G. Wrightson, editors, Parallelization in Inference Systems. LNAI 590, Springer-Verlag, 1992.
B. Fronhöfer and F. Kurfeß. Cooperative Competition: A Modest Proposal Concerning the Use of Multi-Processor Systems for Automated Reasoning. Technical Report ATP-74-VTI-87, Institut für Informatik, Technische Universität München, 1987.
V. K. Janakiram, D. P. Agrawal, and R. Mehrotra. Randomized Parallel Algorithms for Prolog Programs and Backtracking Applications. In Int. Conf. on Parallel Processing, pages 278–281, 1987.
V. Kumar and V. N. Rao. Scalable Parallel Formulations of Depth-First Search. In Vipin Kumar, P.S. Gopalakrishnan, and Laveen N. Kanal, editors, Parallel Algorithmus for Maschine Intelligence and Vision, pages 1–41. Springer Verlag, New York, 1990.
R. Letz, J. Schumann, S. Bayerl, and W. Bibel. SETHEO, A High-Performance Theorem Prover. to appear in Journal of Automated Reasoning, 1992. available as Technical Report TUM-I9008 from Technical University Munich.
F. Pfenning. Single axioms in the implicational prepositional calculus. In 9th Int. Conf. on Automated Deduction, pages 710–713, Berlin, 1988. Springer Verlag, LNCS 310.
J. Schumann and R. Letz. PARTHEO: a High Performance Parallel Theorem Prover. In 10th Int. Conf. on Automated Deduction, pages 40–56. Springer Verlag, LNAI 449, 1990.
E. Speckenmeyer, B. Monien, and O. Vornberger. Superlinear speedup for parallel backtracking. In Supercomputing, LNCS 297, pages 985–994. Springer Verlag, 1988.
L. Wos. Automated Reasoning: 33 Basic Research Problems. Prentice-Hall, 1988.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1992 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Ertel, W. (1992). OR-parallel theorem proving with random competition. In: Voronkov, A. (eds) Logic Programming and Automated Reasoning. LPAR 1992. Lecture Notes in Computer Science, vol 624. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0013064
Download citation
DOI: https://doi.org/10.1007/BFb0013064
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-55727-2
Online ISBN: 978-3-540-47279-7
eBook Packages: Springer Book Archive