Rippling: A heuristic for guiding inductive proofs. (English) Zbl 0789.68121
In proof search for inductive proofs typical term patterns occur in deriving the induction conclusion out of the induction hypothesis. A powerful method to control this stage of the induction proof is rippling. This paper gives a thorough analysis of the rippling technique and its various forms. Some of the rippling tactics presented here are the original rippling-out, rippling with multi wave-rules, rippling-in, rippling with conditional wave rules, rippling sideways – accross and under existential quantification. While rippling-out in successor induction consists (roughly spoken) in shifting the successor function symbol in the induction conclusion outwards (in order to obtain the form of the induction hypothesis), rippling-in is more difficult technique. It is used essentially if rippling-out is blocked and consists in shifting the successor (or, in general, a distinguished term) in words. It is practically impossible to give a detailed account of all the different techniques presented in this very rich paper. The authors do not only present several new techniques (not contained in the article by A. Bundy, F. van Harmelen, J. Hesketh and A. Smaill [J. Autom. Reasoning 7, 303-324 (1991; Zbl 0733.68069)]), but they also define a generalization which serves as uniform framework for all different kinds of rippling. Moreover the authors provide strong evidence of practical usefulness by several examples and case studies. It is shown that, in using rippling, a higher degree of mechanization is reached than in the Boyer-Moore proof procedure. It is also shown that rippling can be successfully applied to problems of symbolic computation (transformation of arithmetical expressions), not to induction proving only. While the termination of rippling-out is easy to prove, the situation becomes more difficult for the extensions defined in this paper. The authors settle this problem by giving a general termination proof of rippling based on so called sequent measures, which model inward and outward reduction. Thus, no matter which of the particular versions of rippling is applied, looping can always be excluded. The paper is a very valuable contribution to inductive theorem proving and to proof search in general.
Reviewer: A.Leitsch (Wien)
MSC:
| 68T15 | Theorem proving (deduction, resolution, etc.) (MSC2010) |
| 03B35 | Mechanization of proofs and logical operations |
Citations:
Zbl 0733.68069References:
| [1] | Aubin, R., Some generalization heuristics in proofs by induction, (Huet, G.; Kahn, G., Actes du Colloque Construction: Amélioration et vérification de Programmes (1975), Institut de Recherche d’Informatique et d’Automatique) |
| [2] | Basin, D.; Walsh, T., Difference matching, (Kapur, D., 11th Conference on Automated Deduction. 11th Conference on Automated Deduction, 1992. 11th Conference on Automated Deduction. 11th Conference on Automated Deduction, 1992, Lecture Notes in Artificial Intelligence, 607 (1992), Springer: Springer Berlin), 295-309 · Zbl 0925.68401 |
| [3] | Boyer, R. S.; Moore, J. S., A computational logic (1979), Academic Press: Academic Press New York · Zbl 0708.68060 |
| [4] | Bundy, A., The use of explicit plans to guide inductive proofs, (Lusk, R.; Overbeek, R., 9th Conference on Automated Deduction (1988), Springer: Springer New York), 111-120, also longer version: DAI Research Paper No 349, University of Edinburgh, Edinburgh, Scotland · Zbl 0656.68106 |
| [5] | Bundy, A.; Smaill, A.; Hesketh, J., Turning eureka steps into calculations in automatic program synthesis, (Clarke, S. L.H., Proceedings UK IT 90 (1990)), 221-226, also DAI Research Paper 448, University of Edinburgh, Edinburgh, Scotland |
| [6] | Bundy, A.; van Harmelen, F.; Hesketh, J.; Smaill, A., Experiments with proof plans for induction, J. Autom. Reasoning, 7, 303-324 (1991), also earlier version DAI Research Paper No 413, University of Edinburgh, Edinburgh, Scotland · Zbl 0733.68069 |
| [7] | Bundy, A.; van Harmelen, F.; Hesketh, J.; Smaill, A.; Stevens, A., A rational reconstruction and extension of recursion analysis, (Proceedings IJCAI-89. Proceedings IJCAI-89, Milan, Italy (1989)), 359-365, also DAI Research Paper 419, University of Edinburgh, Edinburgh, Scotland · Zbl 0708.68061 |
| [8] | Bundy, A.; van Harmelen, F.; Horn, C.; Smaill, A., The Oyster-Clam system, (Stickel, M. E., 10th International Conference on Automated Deduction. 10th International Conference on Automated Deduction, Lecture Notes in Artificial Intelligence, 449 (1990), Springer: Springer New York), 647-648, also DAI Research Paper 507, University of Edinburgh, Edinburgh, Scotland · Zbl 1509.68299 |
| [9] | Bundy, A.; van Harmelen, F.; Smaill, A.; Ireland, A., Extensions to the rippling-out tactic for guiding inductive proofs, (Stickel, M. E., 10th International Conference on Automated Deduction. 10th International Conference on Automated Deduction, Lecture Notes in Artificial Intelligence, 449 (1990), Springer: Springer New York), 146-312, also DAI Research Paper 459, University of Edinburgh, Edinburgh, Scotland · Zbl 1509.68300 |
| [10] | Bundy, A.; Welham, B., Using meta-level inference for selective application of multiple rewrite rule sets in algebraic manipulation, Artif. Intell., 16, 2, 189-212 (1981), also DAI Research Paper 121, University of Edinburgh, Edinburgh, Scotland |
| [11] | Burstall, R. M.; Darlington, J., A transformation system for developing recursive programs, J. ACM, 24, 1, 44-67 (1977) · Zbl 0343.68014 |
| [12] | Constable, R. L.; Allen, S. F.; Bromley, H. M., (Implementing Mathematics with the Nuprl Proof Development System (1986), Prentice Hall: Prentice Hall Englewood Cliffs, NJ) |
| [13] | Dershowitz, N.; Manna, Z., Proving termination with multiset orderings, Comm. ACM, 22, 8, 465-476 (1979) · Zbl 0431.68016 |
| [14] | Hesketh, J. T., Using middle-out reasoning to guide inductive theorem proving, (Ph.D. Thesis (1991), University of Edinburgh: University of Edinburgh Edinburgh, Scotland), Unpublished |
| [15] | Hutter, D., Guiding inductive proofs, (Stickel, M. E., 10th International Conference on Automated Deduction. 10th International Conference on Automated Deduction, Lecture Notes in Artificial Intelligence, 449 (1990), Springer: Springer New York), 147-161 · Zbl 1509.68309 |
| [16] | Kanamori, T.; Fujita, H., Formulation of induction formulas in verification of Prolog programs, (Siekmann, J., 8th Conference on Automated Deduction. 8th Conference on Automated Deduction, Lecture Notes in Computer Science, 230 (1986), Springer: Springer New York), 281-299 · Zbl 0642.68023 |
| [17] | (Kapur, D., 11th Conference on Automated Deduction. 11th Conference on Automated Deduction, 1992. 11th Conference on Automated Deduction. 11th Conference on Automated Deduction, 1992, Lecture Notes in Artificial Intelligence, 607 (1992), Springer: Springer Berlin) · Zbl 0925.00071 |
| [18] | Knuth, D. E.; Bendix, P. B., Simple word problems in universal algebra, (Leech, J., Computational Problems in Abstract Algebra (1970), Pergamon Press: Pergamon Press Oxford), 263-297 · Zbl 0188.04902 |
| [19] | Walsh, T.; Nunes, A.; Bundy, A., The use of proof plans to sum series, (Kapur, D., 11th Conference on Automated Deduction. 11th Conference on Automated Deduction, 1992. 11th Conference on Automated Deduction. 11th Conference on Automated Deduction, 1992, Lecture Notes in Artificial Intelligence, 607 (1992), Springer: Springer Berlin), 325-339 · Zbl 0925.03072 |
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. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
