Abstract
Knowledge-based proof planning is a new paradigm in automated theorem proving. Its motivation partly comes from an increasing disillusionment by many researchers in the field of automated deduction, who feel that traditional techniques have been pushed to their limit and — as important as these developments have been in the past — will not be sufficient to reach the goal of a mathematical assistant system. Human mathematicians — among other differences — have a long term plan for a complex proof which is clearly not represented at the calculus-level of individual inference steps. Moreover a mathematician in a well established field has a whole battery of proof strategies, techniques, and tricks of the trade at his disposal.
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
Bartle, R. and Sherbert, D. (1982). Introduction to Real Analysis. John Wiley Sons.
Benzmueller, C., Cheikhrouhou, L., Fehrer, D., Fiedler, A., Huang, X., Kerber, M., Kohlhase, M., Konrad, K., Meier, A., Melis, E., Schaarschmidt, W., Siekmann, J., and Sorge, V. (1997). OMEGA: Towards a mathematical assistant. In McCune, W., editor, CADE-14,pages 252–255, Springer.
Bledsoe, W., Boyer, R., and Henneman, W. (1972). Computer proofs of limit theorems. Artificial Intelligence, 3 (1): 27–60.
Bundy, A. (1988). The use of explicit plans to guide inductive proofs. In Lusk, E. and Overbeek, R., editors, CADE-9,pages 111–120, Springer.
Bundy, A., van Harmelen, F., Hesketh, J., and Smaill, A. (1991). Experiments with proof plans for induction. Journal of Automated Reasoning, 7: 303–324.
Bundy, A., van Harmelen, F., Ireland, A., and Smaill, A. (1990). Extensions to the rippling-out tactic for guiding inductive proofs. In Stickel, M., editor, CADE-10,Springer.
Chang, C.-L. and Lee, C.-T. (1973). Symbolic Logic and Mechanical Theorem Proving. Computer Science Classics. Academic Press.
Cheikbrouhou, L. and Siekmann, J. (1998). Planning diagonalization proofs. InAIMSA-98,Springer.
Davis, W., Porta, H., and Uhl, J. (1994). Calculus Mathematica. Addison-Wesley.
Fikes, R. and Nilsson, N. (1971). STRIPS: A new approach to the application of theorem proving to problem solving. Artificial Intelligence, 2: 189–208.
Gordon, M., Milner, R., and Wadsworth, C. (1979). Edinburgh LCF: A Mechanized Logic of Computation.
Huang, X., Kerber, M., Kohlbase, M., and Richts, J. (1994). Methods - the basic units for planning and verifying proofs. In Jahrestagung fir Künstliche Intelligenz KI-94,Springer.
Hutter, D. (1990). Guiding inductive proofs. In Stickel, M., editor, CADE-10,Springer.
Hutter, D., Langenstein, B., Sengler, C., Siekmann, J., Stephan, W., and Wolpers, A. (1996). Deduction in the verification support environment (VSE). Third International Symposium of Formal Methods Europe, pages 268–286.
Ireland, A. and Bundy, A. (1996). Productive use of failure in inductive proof. Journal of Automated Reasoning, 16 (1–2): 79–111.
Kambhampati, S. (1996). Refinement planning: Status and prospectus. In AAAI-96, pages 1331–1336.
Koehler, J. (1998). Solving complex tasks through extraction of subproblems. In Simmons, R., Veloso, M., and Smith, S. (eds), AIPS-98, pages 62–69.
Laird, J., Newell, A., and Rosenbloom, P. (1987). SOAR:an architecture for general intelligence. Artificial Intelligence, 33 (1): 1–64.
Leckie, C. and Zukerman, I. (1998). Inductive learning of search control rules for planning. Artificial Intelligence, 101(1–2):63–98.
Loveland, D. (1978). Automated Theorem Proving: A Logical Basis. North Holland, New York.
McCune, W. (1990). Otter 2.0 users guide. Technical Report ANL-90/9, Argonne National Laboratory, Maths and CS Division, Argonne, Illinois.
Melis, E. (1998a). AI-techniques in proof planning. In ECAI-98,pages 494–498, Wiley.
Melis, E. (1998b). The “limit” domain. In Simmons, R., Veloso, M., and Smith, S. (eds), AIPS-98, pages 199–206.
Melis, E. (1998c). Proof planning with multiple strategies. In workshop: Strategies in Automated Deduction.
Minton, S. (1989). Explanation-based learning: A problem solving perspective. Artificial Intelligence, 40: 63–118.
Minton, S., Knoblock, C., Koukka, D., Gil, Y., Joseph, R., and Carbonell, J. (1989). PRODIGY 2.0: The Manual and Tutorial. Carnegie Mellon University. CMU-CS-89–146.
Pollack, M., Joslin, D., and Paolucci, M. (1997). Flaw selection strategies for partial-order planning. Journal of Artificial Intelligence Research, 6: 223–262.
Sacerdoti, E. (1974). Planning in a hierarchy of abstraction spaces. Artificial Intelligence, 5 (2): 115–135.
Tate, A. (1977). Generating project networks. In IJCAI-77,pages 888–893. Morgan Kaufmann.
Veloso, M., Carbonell, J., Pérez, M. A., Borrajo, D., Fink, E., and Blythe, J. (1995). Integrating planning and learning: The PRODIGY architecture. JETAI Journal, pages 81–120.
Weld, D. (1994). An introduction to least committment planning. Al magazine, 15 (4): 27–61.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2000 Springer Science+Business Media Dordrecht
About this chapter
Cite this chapter
Melis, E., Siekmann, J.H. (2000). Concepts in Proof Planning. In: Hölldobler, S. (eds) Intellectics and Computational Logic. Applied Logic Series, vol 19. Springer, Dordrecht. https://doi.org/10.1007/978-94-015-9383-0_16
Download citation
DOI: https://doi.org/10.1007/978-94-015-9383-0_16
Publisher Name: Springer, Dordrecht
Print ISBN: 978-90-481-5438-8
Online ISBN: 978-94-015-9383-0
eBook Packages: Springer Book Archive