Abstract
In this paper we show that distributing the theorem proving task to several experts is a promising idea. We describe the team work method which allows the experts to compete for a while and then to cooperate. In the cooperation phase the best results derived in the competition phase are collected and the less important results are forgotten. We describe some useful experts and explain in detail how they work together. We establish fairness criteria and so prove the distributed system to be both complete and correct. We have implemented our system and show by non-trivial examples that drastical time speed-ups are possible for a cooperating team of experts compared to the time needed by the best expert in the team.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Avenhaus, J., Denzinger, J.: Distributing equational theorem proving, to appear as SEKI-Report, Universität Kaiserslautern, 1993.
Avenhaus, J., Madlener, K.: Term Rewriting and Equational Reasoning, in R.B. Banerji (ed): Formal Techniques in Artificial Intelligence, Elsevier, 1990, pp. 1–43.
Antoniou, G., Ohlbach, H.J.: Terminator, Proc. 8th IJCAI, Karlsruhe, 1983.
Bachmair, L., Dershowitz, N., Hsiang, J.: Orderings for equational proofs, Proc. Symposium on Logic in Computer Science, 1986, pp. 346–357.
Bachmair, L., Dershowitz, N., Plaisted, D.A.: Completion without Failure, Coll. on the Resolution of Equations in Algebraic Structures, Austin (1987), Academic Press, 1989.
Bonacina, M.P., Hsiang, J.: On fairness in distributed automated deduction, to be published.
Conry, S.E.; MacIntosh, D.J., Meyer, R.A.: DARES: A Distributed Automated REasoning System, Proc. AAAI-90, 1990, pp. 78–85.
Denzinger, J.: TEAMWORK: A method to design distributed knowledge based equational theorem provers, forthcoming Ph.D. thesis, University of Kaiserslautern, 1993.
Dershowitz, N., Jouannaud, J.P.: Rewriting systems, in J. van Leeuwen (Ed.): Handbook of theoretical computer science, Vol. B., Elsevier, 1990, pp. 241–320.
Ertel, W.: Random Competition: A Simple, but Efficient Method for Parallelizing Inference Systems, Int. Report TUM-19050, Technical University of Munich, 1990.
Garland, S.J., Yelick, K.A.: A Parallel Completion procedure for Term Rewriting Systems, Proc. 11th CADE, 1992, pp. 109–123.
Huet, G.: Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems, Journal of ACM, Vol. 27, No. 4, 1980, pp. 798–821.
Knuth, D.E., Bendix, P.B.: simple Word Problems in Universal Algebra, Computational Algebra, J. Leech, Pergamon Press, 1970, pp. 263–297.
Slaney, J.K., Lusk, E.L.: Parallelizing the Closure Computation in Automated Deduction, Proc. 10th CADE, LNAI 449, Springer, Kaiserslautern, 1990, pp. 28–39.
Stickel, M.E.: A Case Study of Theorem Proving by the Knuth-Bendix Method: Discovering that x3 = x implies Ring Commutativity, Proc. CADE-7, LNCS 170, Springer, 1984, pp. 248–258.
Tarski, A.: Logic, Semantics, Meta mathematics, Oxford University Press, 1956.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1993 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Avenhaus, J., Denzinger, J. (1993). Distributing equational theorem proving. In: Kirchner, C. (eds) Rewriting Techniques and Applications. RTA 1993. Lecture Notes in Computer Science, vol 690. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-21551-7_6
Download citation
DOI: https://doi.org/10.1007/978-3-662-21551-7_6
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-56868-1
Online ISBN: 978-3-662-21551-7
eBook Packages: Springer Book Archive