Abstract
Proof by mathematical induction gives rise to various kinds of eureka steps, e.g., missing lemmata and generalization. Most inductive theorem provers rely upon user intervention in supplying the required eureka steps. In contrast, we present a novel theorem-proving architecture for supporting the automatic discovery of eureka steps. We build upon rippling, a search control heuristic designed for inductive reasoning. We show how the failure if rippling can be used in bridging gaps in the search for inductive proofs.
The research reported in this paper was supported by EPSRC grant GR/J/80702 and ARC grant 438.
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
Aubin, R.: Some generalization heuristics in proofs by induction, in G. Huet and G. Kahn (eds), Actes du Colloque Construction: Amélioration et vérification de Programmes, Institut de recherche d’informatique et d’automatique, 1975.
Boyer, R. S. and Moore, J. S.: A Computational Logic, Academic Press, New York, 1979. ACM monograph series.
Bouboula. A. and Rusinowitch, M.: Automatic case analysis in proof by induction, in Proc. 13th IJCAJ, Int. Joint Conf. Artificial Intelligence, 1993.
Bundy, A., Stevens, A., van Harmelen, E, Ireland, A., and Smaill, A.: Rippling: A heuristic for guiding inductive proofs, Artificial Intelligence 62 (1993), 185–253. Also available from Edinburgh as DAI Research Paper No. 567.
Bundy, A.: The use of explicit plans to guide inductive proofs, in R. Lusk and R. Overbeek (eds), 9th Conf. Automated Deduction,Springer-Verlag, 1988, pp. 111–120. Longer version avilable from Edinburgh as DAI Research Paper No. 349.
Bundy, A., van Harmelen, F., Horn, C., and Smaill, A.: The Oyster-Clam system, in M. E. Stickel (ed.), 10th Int. Conf. Automated Deduction,Lecture Notes in Artificial Intelligence 449, Springer-Verlag, 1990, pp. 647–648. Also available from Edinburgh as DAI Research Paper No. 507.
Bundy, A., van Harmelen, F., Smaill, A., and Ireland, A.: Extensions to the rippling-out tactic for guiding inductive proofs, in M. E. Stickel (ed.), 10th Int. Conf. Automated Deduction,Lecture Notes in Artificial Intelligence 449, Springer-Verlag, 1990, pp. 132–146. Also available from Edinburgh as DAI Research Paper No. 459.
Bundy, A. and Welham, B.: Using meta-level inference for selective application of multiple rewrite rules in algebraic manipulation, Artificial Intelligence 16(2) (1981), 189–212. Also available from Edinburgh as DAI Research Paper No. 121.
Basin, D. and Walsh, T.: Difference matching, in Deepak Kapur (ed.), 11th Conf. Automated Deduction, Saratoga Springs, NY, USA, June 1992. Published as Springer Lecture Notes in Artificial Intelligence 607, pp. 295–309.
Gentzen, G.: The Collected Papers of Gerhard Gentzen, edited by M. E. Szabo, North-Holland, Amsterdam, 1969.
Gordon, M. J., Milner, A. J., and Wadsworth, C. P.: Edinburgh LCF-A Mechanised Logic of Computation, Lecture Notes in Computer Science 78, Springer-Verlag, 1979.
Hardy, G. H.: Mathematical proof, MIND: A Quarterly Review of Psychology and Philosophy, 38 (149) (January 1929), 1–25.
Hesketh, J. T.: Using middle-out reasoning to guide inductive theorem proving, PhD thesis, University of Edinburgh, 1991.
Hutter, D. and Kohlhase, M.: A Colored Version of the A-Calculus, Seki-report sr-95–05, University of Saarland, 1995.
Hutter, D.: Guiding inductive proofs, in M. E. Stickel (ed.), 10th Int. Con’ Automated Deduction, Lecture Notes in Artificial Intelligence 449, Springer-Verlag, 1990, pp. 147–161.
Ireland, A.: The use of planning critics in mechanizing inductive proofs, in A. Voronkov (ed.), Im’. Conf. Logic Programming and Automated Reasoning, LPAR 92, Si. Petersburg,Lecture Notes in Artificial Intelligence 624, Springer-Verlag, 1992, pp. 178–189. Also available from Edinburgh as DAI Research Paper No. 592.
Monroy, R., Bundy, A., and Ireland, A.: Proof plans for the correction of false conjectures, in F. Pfenning (ed.), 5th Int. Conf. Logic Programming and Automated Reasoning, LPAR 94, Lecture Notes in Artificial Intelligence 822, Springer-Verlag, 1994, pp. 54–68. Also available from Edinburgh as Research Paper No. 681.
Miller, D. and Nadathur, G.: An overview of AProlog, in R. Bowen and K. Kowalski (eds), Proc. 5th Int. Logic Programming Conf./5th Symp. on Logic Programming, MIT Press, 1988.
Manna, Z. and Waldinger, R.: The Logical Basis for Computer Programming, Vol. 1. Deductive Reasoning, Addison/Wesley, Reading, MA, 1985.
Thomas, M. and Jantke, K. P.: Inductive inference for solving divergance in Knuth—Bendix, in K. P. Jantke (ed.), Analogical and Inductive Inference, Proc. AII’89, Springer-Verlag, 1989, pp. 288–303.
Walsh, T.: A divergence critic, in Alan Bundy (ed.), 12th Conf. Automated Deduction, Lecture Notes in Artificial Intelligence 814, Springer-Verlag, Nancy, France, 1994.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1996 Kluwer Academic Publishers
About this chapter
Cite this chapter
Ireland, A., Bundy, A. (1996). Productive Use of Failure in Inductive Proof. In: Zhang, H. (eds) Automated Mathematical Induction. Springer, Dordrecht. https://doi.org/10.1007/978-94-009-1675-3_3
Download citation
DOI: https://doi.org/10.1007/978-94-009-1675-3_3
Publisher Name: Springer, Dordrecht
Print ISBN: 978-94-010-7250-2
Online ISBN: 978-94-009-1675-3
eBook Packages: Springer Book Archive