97:
At the start of rippling the differences between the two expressions, known as wave-fronts in rippling parlance, are identified. Typically these differences prevent the completion of the proof and need to be "moved away". The target expression is annotated to distinguish the wavefronts (differences)
121:
Typically, the base case of any inductive proof is solved by methods other than rippling. For this reason, we will concentrate on the step case. Our step case takes the following form, where we have chosen to use x as the induction variable:
56:
Raymond Aubin was the first person to use the term "rippling out" whilst working on his 1976 PhD thesis at the
University of Edinburgh. He recognised a common pattern of movement during the rewriting stage of inductive proofs.
94:, and the target expression the inductive conclusion. Usually, the differences between the hypothesis and conclusion are only minor, perhaps the inclusion of a successor function (e.g., +1) around the induction variable.
48:, where special object level annotations are used to ensure fertilization upon the completion of rewriting, with a measure decreasing requirement ensuring termination for any set of rewrite rules and expression.
64:
Since then, "rippling sideways", "rippling in" and "rippling past" were coined, so the term was generalised to rippling. Rippling continues to be developed at
Edinburgh, and elsewhere, as of 2007.
157:
132:
We may also possess several rewrite rules, drawn from lemmas, inductive definitions or elsewhere, that can be used to form wave-rules. Suppose we have the following three rewrite rules:
137:
147:
83:
Very often, when attempting to prove a proposition, we are given a source expression and a target expression, which differ only by the inclusion of a few extra syntactic elements.
127:
167:
152:
Note that all these annotated rules preserve the skeleton (x + y = y + x, in the first case and x + y in the second/third). Now, annotating the inductive step case, gives us:
172:
Note that the final rewrite causes all wave-fronts to disappear, and we may now apply fertilization, the application of the inductive hypotheses, to complete the proof.
118:. This is an elementary property, and the proof is by routine induction. Nevertheless, the search space for finding such a proof may become quite large.
67:
Rippling has been applied to many problems traditionally viewed as being hard in the inductive theorem proving community, including
304:
61:
later turned this concept on its head by defining rippling to be this pattern of movement, rather than a side effect.
210:
98:
and skeleton (common structure) between the two expressions. Special rules, called wave rules, can then be used in a
261:
102:
fashion to manipulate the target expression until the source expression can be used to complete the proof.
194:
21:
41:
33:
37:
71:'s limit theorems and a proof of the Gordon microprocessor, a miniature computer developed by
32:, developed primarily in the Mathematical Reasoning Group in the School of Informatics at the
91:
72:
8:
299:
278:
87:
206:
99:
282:
270:
231:
198:
17:
111:
188:
156:
45:
293:
202:
115:
68:
253:
136:
274:
58:
29:
146:
235:
126:
166:
193:. Cambridge Tracts in Theoretical Computer Science. Cambridge:
189:
Alan Bundy; David Basin; Dieter Hutter; Andrew
Ireland (2005).
251:
230:, EDI-INF-PHD, vol. 76–002, University of Edinburgh,
191:
Rippling: Meta-Level
Guidance for Mathematical Reasoning
44:. Rippling may be viewed as a restricted form of
291:
90:, where the given expression is taken to be the
254:"A Calculus for and Termination of Rippling"
162:And we are all set to perform rippling:
292:
252:David A. Basin and Toby Walsh (1996).
142:then these can be annotated, to form:
225:
86:This is especially true in inductive
110:We aim to show that the addition of
13:
245:
36:, and most commonly used to guide
14:
316:
42:automated theorem proving systems
228:Mechanizing Structural Induction
165:
155:
145:
135:
125:
28:refers to a group of meta-level
262:Journal of Automated Reasoning
219:
182:
1:
175:
7:
78:
75:and his team at Cambridge.
10:
321:
195:Cambridge University Press
105:
51:
305:Automated theorem proving
22:automated theorem proving
203:10.1017/CBO9780511543326
226:Aubin, Raymond (1976),
34:University of Edinburgh
20:, more particularly in
92:inductive hypothesis
73:Michael J. C. Gordon
275:10.1007/BF00244462
312:
286:
269:(1–2): 147–180.
258:
239:
238:
223:
217:
216:
186:
169:
159:
149:
139:
129:
38:inductive proofs
18:computer science
320:
319:
315:
314:
313:
311:
310:
309:
290:
289:
256:
248:
246:Further reading
243:
242:
224:
220:
213:
187:
183:
178:
112:natural numbers
108:
81:
54:
12:
11:
5:
318:
308:
307:
302:
288:
287:
247:
244:
241:
240:
218:
211:
180:
179:
177:
174:
107:
104:
80:
77:
53:
50:
46:rewrite system
9:
6:
4:
3:
2:
317:
306:
303:
301:
298:
297:
295:
284:
280:
276:
272:
268:
264:
263:
255:
250:
249:
237:
233:
229:
222:
214:
212:0-521-83449-X
208:
204:
200:
196:
192:
185:
181:
173:
170:
168:
163:
160:
158:
153:
150:
148:
143:
140:
138:
133:
130:
128:
123:
119:
117:
113:
103:
101:
95:
93:
89:
84:
76:
74:
70:
65:
62:
60:
49:
47:
43:
39:
35:
31:
27:
23:
19:
266:
260:
227:
221:
190:
184:
171:
164:
161:
154:
151:
144:
141:
134:
131:
124:
120:
109:
96:
85:
82:
66:
63:
55:
25:
15:
116:commutative
100:terminating
300:Heuristics
294:Categories
176:References
59:Alan Bundy
30:heuristics
236:1842/6649
283:14427821
79:Overview
26:rippling
106:Example
69:Bledsoe
52:History
281:
209:
88:proofs
279:S2CID
257:(PDF)
207:ISBN
271:doi
232:hdl
199:doi
114:is
40:in
16:In
296::
277:.
267:16
265:.
259:.
205:.
197:.
24:,
285:.
273::
234::
215:.
201::
Text is available under the Creative Commons Attribution-ShareAlike License. Additional terms may apply.
