Rippling: A heuristic for guiding inductive proofs (Q685548)

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 \textit{A. Bundy, F. van Harmelen, J. Hesketh} and \textit{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.