7 - Conclusions

Summary

We have come a long way in our investigation of rippling: from the observation of a common pattern in structural induction proofs, to a new paradigm in proof search. Firstly, we noted that this common pattern could be enforced, rather than merely observed, by inserting meta-level annotations into object-level formulas. These annotations – wave-holes and wave-fronts – marked those parts of formulas that were to be preserved and moved, respectively. Ensuring that rewriting respected these annotations enforced additional constraints during proof search: restricting that search to those parts of the search space that made progress towards using the induction hypothesis to prove the induction conclusion.

Secondly, experimental exploration with these annotations suggested a wealth of ways to extend and generalize the original idea beyond simple structural inductions to more complex forms of induction and to many other kinds of proof. Indeed, whenever proving a goal using one or more structurally similar “givens”, rippling could help guide the proof through a potential combinatorial explosion towards a successful conclusion with little or no search.

Thirdly, since rippling imposes such strong expectations on the structure of a proof, any failure of rippling can be analyzed to suggest how to patch an initially failed proof attempt. This productive use of failure often suggests proof patches that had previously been thought beyond the ability of automated reasoners: so-called, “eureka” steps. These may include, for instance, the suggestion of a novel induction rule, a new lemma, a generalization of the original conjecture, or a case split.