Edinburgh Research Explorer

Extensions to the Rippling-Out Tactic for Guiding Inductive Proofs

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Related Edinburgh Organisations

Open Access permissions


Original languageEnglish
Title of host publication10th International Conference on Automated Deduction
Subtitle of host publicationKaiserslautern, FRG, July 24–27, 1990 Proceedings
PublisherSpringer-Verlag GmbH
VolumeLecture Notes in Artificial Intelligence No. 449
ISBN (Print)3-540-52885-7
Publication statusPublished - 1990

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Verlag
ISSN (Print)0302-9743


In earlier papers we described a technique for automatically constructing inductive proofs, using a heuristic search control tactic called rippling-out. Further testing on harder examples has shown that the rippling-out tactic significantly reduces the search for a proof of a wide variety of theorems, with relatively few cases in which all proofs were pruned. However, it also proved necessary to generalise and extend rippling-out in various ways. Each of the various extensions are described with examples to illustrate why they are needed, but it is shown that the spirit of the original rippling-out tactic has been retained. The research reported in this paper was supported by SERC grant GR/E/44598, and an SERC Senior Fellowship to the first author. We wish to thank our colleagues in the Edinburgh Mathematical Reasoning Group and three anonymous referees for feedback on this paper.

Download statistics

No data available

ID: 403792