Abstract
We present a new way to use planning in automated theorem proving by means of distribution. To overcome the problem that often subtasks of a problem cannot be detected a priori (which prevents the use of known planning and distribution techniques) we use the teamwork approach: A team of experts independently works on the problem with different heuristics. After a certain amount of time referees judge their results using the impact of the results on the behaviour of the experts. Then a supervisor combines the selected results to a new starting point. The supervisor also selects the experts that will work on the problem in the next round. This selection is a reactive planning task. We outline which information the supervisor can use to fulfill this task and how this information is processed to result in a plan or in revising a plan. Experimental results show that this planning approach for the assignment of experts to a team enables the system to solve many different examples in an acceptable time with the same start configuration and without any intervention by the user.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Avenhaus, J.; Denzinger, J.: Distributing equational theorem proving, Proc. 5th RTA, Montreal, LNCS 690, 1993, pp. 62–76.
Boddy, M.; Dean, T.: An Analysis of Time-Dependent Planning, Proc. 7. National Conf. on AI, Minneapolis, 1988, pp. 49–54.
Bachmair, L.; Dershowitz, N.; Plaisted, D.A.: Completion without Failure, Coll. on the Resolution of Equations in Algebraic Structures, Austin (1987), Academic Press, 1989.
Beetz, M.: Decision-theoretic Transformational Planning, Internal report, Yale University, 1991.
Bundy, A.: The use of explicit plans to guide inductive proofs, Proc. 9th CADE, 1988.
Chang, C.L.; Lee, R.C.: Symbolic Logic and Mechanical Theorem Proving, Academic Press, 1973.
Denzinger, J.: Knowledge-Based Distributed Search Using Teamwork, Proc. ICMAS-95, San Francisco, AAAI-Press, 1995, pp. 81–88.
Denzinger, J.; Fuchs, M.: Goal oriented equational theorem proving using teamwork, Proc. KI-94, Saarbrücken, LNAI 861, 1994, pp. 343–354.
Durfee, E.H.; Lesser, V.R.: Using Partial Global Plans to Coordinate Distributed Problem Solvers, Proc. IJCAI-87, 1987, pp.875–883.
Denzinger, J.; Schulz, S.: Recording and Analyzing Knowledge-Based Distributed Deduction Processes, to appear in Journal of Symbolic Computation, 1996.
Fikes, R.E.; Hart, P.E.; Nilsson, N.J.: Learning and executing generalized robot plans, in Webber, Nilsson (eds.) Readings in AI, 1981, pp.231–249.
Hsiang, J.; Rusinowitch, M.: On word problems in equational theories, Proc. 14th ICALP, Karlsruhe, LNCS 267, 1987, pp. 54–71.
McCune, W.W.: OTTER 3.0 Reference manual and Guide, Tech. Rep. ANL-94/6, Argonne National Laboratory, 1994.
Mc Dermott, D.: Planning reactive behaviour: A progress report, in J. Allen, J.Handler, A. Tate: Innovative Approaches to Planning, Scheduling and Control, Kaufmann, 1990, pp.450–458.
Rosenschein, J.S.: Synchronization of Multi-Agent Plans, Proc. AAAI-82, 1982, pp.115–119.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1996 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Denzinger, J., Kronenburg, M. (1996). Planning for distributed theorem proving: The teamwork approach. In: Görz, G., Hölldobler, S. (eds) KI-96: Advances in Artificial Intelligence. KI 1996. Lecture Notes in Computer Science, vol 1137. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-61708-6_45
Download citation
DOI: https://doi.org/10.1007/3-540-61708-6_45
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-61708-2
Online ISBN: 978-3-540-70669-4
eBook Packages: Springer Book Archive