Extensions to the rippling-out tactic for guiding inductive proofs

Abstract

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.