Abstract
We propose the use of explicit proof plans to guide the search for a proof in automatic theorem proving. By representing proof plans as the specifications of LCF-like tactics, [Gordon et al 79], and by recording these specifications in a sorted meta-logic, we are able to reason about the conjectures to be proved and the methods available to prove them. In this way we can build proof plans of wide generality, formally account for and predict their successes and failures, apply them flexibly, recover from their failures, and learn them from example proofs.
We illustrate this technique by building a proof plan based on a simple subset of the implicit proof plan embedded in the Boyer-Moore theorem prover, [Boyer & Moore 79].
Space restrictions have forced us to omit many of the details of our work. These are included in a longer version of this paper which is available from: The Documentation Secretary, Department of Artificial Intelligence, University of Edinburgh, Forrest Hill, Edinburgh EH1 2QL, Scotland.
I am grateful for many long conversations with other members of the mathematical reasoning group, from which many of the ideas in this paper emerged. In particular, I would like to thank Frank van Harmelen, Jane Hesketh and Andrew Stevens for feedback on this paper. The research reported in this paper was supported by SERC grant GR/D/44874 and Alvey/SERC grant GR/D/44270.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
R.S. Boyer and J.S. Moore. A Computational Logic. Academic Press, 1979. ACM monograph series.
A. Bundy and B. Welham. Using meta-level inference for selective application of multiple rewrite rules in algebraic manipulation. Artificial Intelligence, 16(2):189–212, 1981. Also available as DAI Research Paper 121.
A. Bundy. The derivation of tactic specifications. Blue Book Note 356, Department of Artificial Intelligence, March 1987.
R.L. Constable, S.F. Allen, H.M. Bromley, et al. Implementing Mathematics with the Nuprl Proof Development System. Prentice Hall, 1986.
R.V. Desimone. Learning control knowledge within an explanation-based learning framework. In I. Bratko and N. Lavrač, editors, Progress in Machine Learning — Proceedings of 2nd European Working Session on Learning, EWSL-87, Bled, Yugoslavia, Sigma Press, May 1987. Also available as DAI Research Paper 321.
M.J. Gordon, A.J. Milner, and C.P. Wadsworth. Edinburgh LCF — A mechanised logic of computation. Volume 78 of Lecture Notes in Computer Science, Springer-Verlag, 1979.
T. B. Knoblock and R.L. Constable. Formalized metareasoning in type theory. In Proceedings of LICS, pages 237–248, IEEE, 1986.
B. Silver. Precondition analysis: learning control information. In Machine Learning 2, Tioga Publishing Company, 1984.
A. Stevens. A Rational Reconstruction of Boyer-Moore Recursion Analysis. Research Paper forthcoming, Dept. of Artificial Intelligence, Edinburgh, 1987. submitted to ECAI-88.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1988 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bundy, A. (1988). The use of explicit plans to guide inductive proofs. In: Lusk, E., Overbeek, R. (eds) 9th International Conference on Automated Deduction. CADE 1988. Lecture Notes in Computer Science, vol 310. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0012826
Download citation
DOI: https://doi.org/10.1007/BFb0012826
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-19343-2
Online ISBN: 978-3-540-39216-3
eBook Packages: Springer Book Archive