Abstract
Proof plans provide a technique for guiding the search for a proof in the context of tactical style reasoning. We propose an extension to this technique in which failure may be exploited in the search for a proof. This extension is based upon the concept of planning critics. In particular we illustrate how proof critics may be used to patch proof plans in the domain of inductive proofs.
The research reported in this paper was supported by SERC grant GR/F/71799.
This is a preview of subscription content, log in via an institution.
Preview
Unable to display preview. Download preview PDF.
References
R.S. Boyer and J.S. Moore. A Computational Logic Handbook. Academic Press, 1988. Perspectives in Computing, Vol 23.
A. Bundy. The use of explicit plans to guide inductive proofs. In R. Lusk and R. Overbeek, editors, 9th Conference on Automated Deduction, pages 111–120, Springer-Verlag, 1988. Longer version available from Edinburgh as DAI Research Paper No. 349.
A. Bundy, A. Smaill, and J. Hesketh. Turning eureka steps into calculations in automatic program synthesis. In S.L.H. Clarke, editor, Proceedings of UK IT 90, pages 221–6, 1990. Also available from Edinburgh as DAI Research Paper 448.
A. Bundy, F. van Harmelen, J. Hesketh, and A. Smaill. Experiments with proof plans for induction. Journal of Automated Reasoning, 7:303–324, 1991. Earlier version available from Edinburgh as DAI Research Paper No 413.
A. Bundy, F. van Harmelen, J. Hesketh, A. Smaill, and A. Stevens. A rational reconstruction and extension of recursion analysis. In N.S. Sridharan, editor, Proceedings of the Eleventh International Joint Conference on Artificial Intelligence, pages 359–365, Morgan Kaufmann, 1989. Also available from Edinburgh as DAI Research Paper 419.
A. Bundy, F. van Harmelen, A. Smaill, and A. Ireland. Extensions to the rippling-out tactic for guiding inductive proofs. In M.E. Stickel, editor, 10th International Conference on Automated Deduction, pages 132–146, Springer-Verlag, 1990. Lecture Notes in Artificial Intelligence No. 449. Also available from Edinburgh as DAI Research Paper 459.
E. Dijkstra. A Discipline of Programming. Prentice-Hall, 1976.
MJ.C. Gordon, R. Milner, and C.P. Wadsworth. Edinburgh LCF. Volume 78 of Lecture Notes in Computer Science, Springer-Verlag LNCS 78, 1979.
J.T. Hesketh. Using Middle-Out Reasoning to Guide Inductive Theorem Proving. PhD thesis, University of Edinburgh, 1991.
Per Martin-Löf. Constructive mathematics and computer programming. In 6th International Congress for Logic, Methodology and Philosophy of Science, pages 153–175, Hanover, August 1979. Published by North Holland, Amsterdam. 1982.
E. Sacerdoti. A Structure for Plans and Behavior. Artificial Intelligence Series, Elsevier North Holland, 1977. Also as SRI AI Technical note number 109, August 1975.
F. van Harmelen. The CLAM Proof Planner, User Manual and Programmer Manual. Technical Paper TP-4, Dept. of Artificial Intelligence, Edinburgh, 1989.
D.E. Wilkins. Practical Planning: Extending the Classical AI Planning Paradigm. Morgan Kaufmann, 1988.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1992 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Ireland, A. (1992). The use of planning critics in mechanizing inductive proofs. 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/BFb0013060
Download citation
DOI: https://doi.org/10.1007/BFb0013060
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