Planning and Patching Proof - Artificial Intelligence and Symbolic Computation - page 33

Rippling can also be extended to support reasoning about logic programs
- and other situations where values are passed between conjoined relations
via shared existential variables, as opposed to being passed between nested
functions.

Relational rippling adapts rippling to this environment

[Bundy & Lombart, 1995].

3.3 Wave Annotations

Is the Concept of Wave-Rule a Formal or Informal One? 'Wave-rule'
can be defined formally. It is a rewrite rule containing wave annotation in which
the skeletons are preserved and the wave-front measure of the right-hand side
is less than that of the left-hand side. Informally, the skeleton consists of those
bits of the expression outside of wave-fronts or inside the wave-holes. The mea-
sure records the position of the wave-fronts in the skeleton. It decreases when
outwards directed wave-fronts move out or downwards wave-fronts move in. A
formal definition of skeleton and of the wave-front measure can be found in
[Basin & Walsh, 1996] and in chapter 4 of [Bundy et al , 2005].

Where Do the Wave Annotations in Wave-Rules and in Induction
Rules Come from? Wave annotation can be inserted in expressions by a
family of difference unification algorithms invented by Basin and Walsh (see
[Basin & Walsh, 1993]). These algorithms are like unification but with the addi-
tional ability to hide non-matching structure in wave-fronts. Ground difference
matching can be used to insert wave annotation into induction rules and ground
difference unification for wave-rules. 'Ground' means that no instantiation of
variables occurs. 'Matching' means that wave-fronts are inserted only into the
induction conclusion and not the induction hypothesis. 'Unification' means that
wave-fronts are inserted into both sides of wave-rules. Note that the process of
inserting wave annotations can be entirely automated.

3.4 Performance

Has Rippling Been Used to Prove Any Hard Theorems? Yes. Rippling
has been used successfully in the verification of the Gordon microprocessor and
the synthesis of a decision procedure and of the rippling tactic itself. It has also
been used outwith inductive proofs for the summing of series and the Lim+
theorem. A survey of some of these successes can be found in chapter 5 of
[Bundy et al , 2005].

Can Rippling Fail? Yes, if there is no wave-rule available to move a wave-front.
In this case we apply critics to try to patch the partial proof. For inductive proofs,
for instance, these may: generalize the induction formula; revise the induction
rule; introduce a case split; or introduce and prove an intermediate lemma, ac-
cording to the precise circumstances of the breakdown. The fact that a failed
ripple provides so much information to focus the attempt to patch the proof is