×

zbMATH — the first resource for mathematics

Experiments with proof plans for induction. (English) Zbl 0733.68069
Summary: The technique of proof plans is explained. This technique is used to guide automatic inference in order to avoid a combinatorial explosion. Empirical research is described to test this technique in the domain of theorem proving by mathematical induction. Heuristic, adapted from the work of Boyer and Moore, have been implemented as Prolog programs, called tactics, and used to guide an inductive proof checker, Oyster. These tactics have been partially specified in a meta-logic, and the plan formation program, CLAM, has been used to reason with these specifications and form plans. These plans are then executed by running their associated tactics and, hence, performing an Oyster proof. Results are presented of the use of this technique on a number of standard theorems from the literature. Searching in the planning space is shown to be considerably cheaper than searching directly in Oyster’s search space. The success rate on the standard theorems is high.

MSC:
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
68T20 Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.)
Software:
CLAM; Isabelle; Nuprl; Oyster
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Aubin, R., ?Some generalization heuristics in proofs by induction?. In Actes du Colloque Construction: Amelioration et verification de Programmes, Institut de recherche d’informatique et d’automatique, 1975.
[2] Boyer, R. S. and Moore, J S., A Computational Logic, Academic Press, 1979, ACM monograph series.
[3] Bundy, A. and Sterling, L. S., ?Meta-level inference: two application?, Journal of Automated Reasoning 4(1), 15-27 (1988). Also available from Edinburgh, Dept. of AI, as Research Paper No. 273. · doi:10.1007/BF00244511
[4] Bundy, A., ?The use of explicit plans to guide inductive proofs?. In 9th Conference on Automated Deduction, pages 111-120, Springer-Verlag, 1988. Longer version available as DAI Research Paper No. 349. · Zbl 0656.68106
[5] Bundy, A., van Harmelen, F., Hesketh, J., Smaill, A. and Stevens, A., ?A Rational Reconstruction and Extension of Recursion Analysis?, Proc. of IJCAI-89 (Sridharan, ed.), Morgan Kaufmann, 1989, 359-365. · Zbl 0708.68061
[6] Burstall, R. M. and Darlington, J., ?A transformation system for developing recursive programs?. Journal of the ACM 24(1), 44-67 (1977). · Zbl 0343.68014 · doi:10.1145/321992.321996
[7] Constable, R. L., Allen, S. F., Bromley, H. M. et al. Implementing Mathematics with the Nuprl Proof Development System. Prentice-Hall, 1986.
[8] Desimone, R. V., ?Explanation-based learning of proof plans?. In Y. Kodratoff (Ed.) Machine and Human Learning, Ellis Horwood, 1987. Also available as DAI Research Paper 304. Previous version in proceedings of EWSL-86.
[9] Gallaire, H. and Lasserre, C., ?Metalevel control for logic programs?. In Logic Programming, p. 173-185, Academic Press, 1982.
[10] Giunchiglia, F. and Walsh, T., ?Abstract Theorem Proving?. Proc. of IJCAI-89 (Shridharan, ed.), Morgan Kaufmann, 1989, pp. 372-377. · Zbl 0708.68066
[11] Gordon, M. J., Milner, A. J. and Wadsworth, C. P., Edinburgh LCF-A mechanised logic of computation. Volume 78 of Lecture Notes in Computer Science, Springer Verlag, 1979. · Zbl 0421.68039
[12] Horn, C., The Nur PRL Proof Development System. Working paper 214, Dept. of Artificial Intelligence, Edinburgh, 1988. The Edinburgh version of NurPRL has been renamed Oyster.
[13] Kanamori, T. and Fujita, H., ?Formulation of induction formulas in verification of Prolog programs. In 8th Conference on Automated Deduction, p. 281-299, Springer-Verlag, 1986. Springer Lecture Notes in Computer Science No. 230. · Zbl 0642.68023
[14] Knoblock, T. B. and Constable, R. L., ?Formalized metareasoning in type theory?. In Proceedings of LICS, p. 237-248, IEEE, 1986.
[15] Martin-Löf, Per, ?Constructive mathematics and computer programming?. In 6th International Congress for Logic, Methodology and Philosophy of Science, p. 153-175, Hanover, August 1979. Published by North Holland, Amsterdam, 1982.
[16] Paulson, L., ?Experience with Isabelle: a generic theorem prover?. In COLOG 88, Institute of Cybernetics of the Estonian SSR, 1988.
[17] Sacerdoti, E. D., ?Planning in a hierarchy of a abstraction spaces?. Artificial Intelligence 5, 115-135 (1974). · Zbl 0288.68052 · doi:10.1016/0004-3702(74)90026-5
[18] Silver, B., Meta-Level Inference: Representing and Learning Control Information in Artificial Intelligence. North Holland, 1985. Revised version of the author’s PhD thesis, DAI 1984.
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.