Abstract
Humans have different problem solving strategies at their disposal and they can flexibly employ several strategies when solving a complex problem, whereas previous theorem proving and planning systems typically employ a single strategy or a hard coded combination of a few strategies. We introduce multi-strategy proof planning that allows for combining a number of strategies and for switching flexibly between strategies in a proof planning process. Thereby proof planning becomes more robust since it does not necessarily fail if one problem solving mechanism fails. Rather it can reason about preference of strategies and about failures. Moreover, our strategies provide a means for structuring the vast amount of knowledge such that the planner can cope with the otherwise overwhelming knowledge in mathematics.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Gandalf. In CASC-14 http://www.cs.jcu.edu.au/~tptp/casc-14/, 1997.
R.G. Bartle and D.R. Sherbert. Introduction to Real Analysis. John Wiley & Sons, New York, 1982.
C. Benzmüller, L. Cheikhrouhou, D. Fehrer, A. Fiedler, X. Huang, M. Kerber, M. Kohlhase, K. Konrad, A. Meier, E. Melis, W. Schaarschmidt, J. Siekmann, and V. Sorge. OMEGA: Towards a mathematical assistant. In Proc. CADE-14, pages 252–255. Springer-Verlag, 1997.
C. Benzmüller, M. Jamnik, M. Kerber, and V. Sorge. Agent Based Mathematical Reasoning? In 7th CALCULEMUS Workshop, pages 21–32, 1999.
W.W. Bledsoe, R.S. Boyer, and W.H. Henneman. Computer proofs of limit theorems. Artificial Intelligence, 3(1):27–60, 1972.
A. Bundy. The use of explicit plans to guide inductive proofs. In Proc. of CADE-9, pages 111–120, 1988.
A. Bundy, A. Stevens, F. Van Harmelen, A. Ireland, and A. Smaill. A heuristic for guiding inductive proofs. Artificial Intelligence, 63:185–253, 1993.
A. Bundy, F. van Harmelen, J. Hesketh, and A. Smaill. Experiments with proof plans for induction. Journal of Automated Reasoning, 7:303–324, 1991.
J. Denzinger and M. Fuchs. Cooperation of heterogeneous provers. In Proc. of IJCAI, pages 10–15. Morgan Kaufmann, 1999.
B. Hayes-Roth. A blackboard architecture for control. Artificial Intelligence, pages 251–321, 1985.
A. Ireland and A. Bundy. Productive use of failure in inductive proof. Journal of Automated Reasoning, 16(1–2):79–111, 1996.
W.W. McCune. Otter 2.0 users guide. Technical Report ANL-90/9, Argonne National Laboratory, 1990.
E. Melis. AI-techniques in proof planning. In Proc. of European Conference on Artificial Intelligence, pages 494–498. Kluwer, 1998.
E. Melis. Combining proof planning with constraint solving. In Proc. of Calculemus and Types’98, 1998.
E. Melis. The“limit” domain. In Proc. of the Fourth International Conference on Artificial Intelligence in Planning Systems (AIPS’98), pages 199–206, 1998.
E. Melis and A. Meier. Proof planning with multiple strategies. Seki report SR-99-06, Universität des Saarlandes, FB Informatik, 1999.
E. Melis and A. Meier. Proof planning with multiple strategies II. In FLoC’99 workshop on Strategies in Automated Deduction, pages 61–72, 1999.
E. Melis and J.H. Siekmann. Knowledge-based proof planning. Artificial Intelligence, 1999.
E. Melis and C. Ullrich. Flexibly interleaving processes. In K.-D. Althoff and R. Bergmann, editors, International Conference on Case-Based Reasoning, volume 1650 of Lecture Notes in Artificial Intelligence, pages 263–275. Springer, 1999.
G. Polya. How to Solve it. Princeton University Press, Princeton, 1945.
A.H. Schoenfeld. Mathematical Problem Solving. Academic Press, New York, 1985.
D.S. Weld. An introduction to least committment planning. AI magazine, 15(4):27–61, 1994.
D.E. Wilkins and K.L. Myers. A multiagent planning architecture. In Proc. of the Fourth International Conference on AI Planning Systems (AIPS’98), pages 154–162, 1998.
A. Wolf. Strategy selection for automated theorem proving. In Proc. of AIMSA’ 98, pages 452–465, 1998.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2000 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Melis, E., Meier, A. (2000). Proof Planning with Multiple Strategies. In: Lloyd, J., et al. Computational Logic — CL 2000. CL 2000. Lecture Notes in Computer Science(), vol 1861. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44957-4_43
Download citation
DOI: https://doi.org/10.1007/3-540-44957-4_43
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-67797-0
Online ISBN: 978-3-540-44957-7
eBook Packages: Springer Book Archive