Rippling: A heuristic for guiding inductive proofs
type: Item
instance of: scholarly article
title: Rippling: A heuristic for guiding inductive proofs
zbMATH Open document ID: 0789.68121
DOI: 10.1016/0004-3702(93)90079-Q
author: Alan Bundy
author: Andrew Stevens
author: Frank van Harmelen
author: Andrew Ireland
author: Alan Smaill
published in: Artificial Intelligence
publication date: 1994-05-09T00:00:00Z
review text: 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 …
reviewed by: Alexander Leitsch
Mathematics Subject Classification ID: 68T15
Mathematics Subject Classification ID: 03B35
zbMATH DE Number: 417435
zbMATH Keywords: inductive proofs
zbMATH Keywords: rippling
Wikidata QID: Q56840271
describes a project that uses: Nuprl
describes a project that uses: CLAM
describes a project that uses: Oyster
MaRDI profile type: Publication
cites work: Q4264732
cites work: Q3490989
cites work: Q3804239
cites work: Experiments with proof plans for induction
cites work: Q3490990
cites work: A Transformation System for Developing Recursive Programs
cites work: Proving termination with multiset orderings
cites work: Q3783512
cites work: Automated deduction -- CADE-11. Proceedings of the 11th international conference held in Saratoga Springs, NY, USA, June 15--18, 1992
cites work: Q5581665
cites work: Q4264708
cites work: The OYSTER-CLAM system
cites work: Extensions to the rippling-out tactic for guiding inductive proofs
cites work: Guiding induction proofs
full work available at URL: 0004-3702(93)90079-q
OpenAlex ID: W2087028873
DBLP publication ID: journals/ai/BundySHIS93
description: scientific article; zbMATH DE number 417435