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

criteria for assessing proof plans. These include generality and parsimony, which
discourage the creation of ad hoc methods designed to guide particular theorems.
Rather, they encourage the design of a few, general-purpose methods which guide
a wide range of theorems. The expectancy criterion promotes the association of
a method with an explanation of why it works. This discourages the design of
methods which often succeed empirically, but for poorly understood reasons. Of
course, these criteria are a matter of degree, so poor judgement may produce
methods which other researchers regard as ad hoc. The criteria of proof planning
then provide a basis for other researchers to criticize such poor judgement.

2.4 Is All This of Relevance to Me?

Would a Proof Planning Approach Be Appropriate for My Applica-
tion? The properties of a problem that indicate that proof planning might be a
good solution are: 1. A search space which causes a combinatorial explosion when
searched without heuristic guidance; 2. The existence of heuristic tactics which
enable expert problem solvers to search a much smaller search space defined by
these tactics; 3. The existence of specifications for each tactic to determine when
it is appropriate to apply it and what effect it will have if it succeeds.

How Would I Go About Developing Proof Plans for My Domain? The
key problem is to identify the tactics and their specifications. This is usually
done by studying successful human problem solving and extracting the tactics.
Sometimes there are texts describing the tactics, e.g. in bridge and similar games.
Sometimes knowledge acquisition techniques, like those used in expert systems,
are needed, e.g. analysis of problem solving protocols, exploratory interviews
with human experts.

3 Rippling

3.1 Introduction

What Is Rippling? A technique for controlling term rewriting using anno-
tations to restrict application and to ensure termination, see Fig. 1. A goal
expression is rippled with respect to one or more given expressions. Each given
expression embeds in the goal expression. Annotations in the goal mark those
subexpressions which correspond to bits of the given (the skeleton) and those
which do not (the wave-fronts). The goal is rewritten so that the embeddings are
preserved, i.e. rewriting can only move the wave-fronts around within the skele-
ton - wave-fronts can change but the skeleton cannot. Furthermore, wave-fronts
are given a direction (outwards or inwards) and movement can only be in that
direction. Outward wave-fronts can mutate to inward, but not vice versa. This
ensures termination. Rippling can be implemented by putting wave annotation
into the rewrite rules to turn them into wave-rules, see Fig. 2. The successful ap-
plication of wave-rule requires that any wave-front in the wave-rule must match