The automation of mathematical reasoning has been an important topic of research almost since computers were invented. The new technique of rippling, described here for the first time in book form, is designed to be an approach to mathematical reasoning that takes into account ideas of heuristics and searching. Rippling addresses the problem of combinatorial explosion which has proved a huge obstacle in the past, and the book offers a systematic and comprehensive introduction to this and to the wider subject of automated inductive theorem proving.
Author(s): Alan Bundy, David Basin, Dieter Hutter, Andrew Ireland
Series: Cambridge Tracts in Theoretical Computer Science 56
Publisher: Cambridge University Press
Year: 2005
Language: English
Pages: 218
Half-title......Page 3
Series title......Page 4
Title......Page 5
Copyright......Page 6
Dedication......Page 7
Contents......Page 9
Preface......Page 13
Acknowledgments......Page 16
1.1.1 The problem of automating reasoning......Page 17
1.1.2 Applications to formal methods......Page 18
1.1.4 Rippling: a common pattern of reasoning......Page 19
1.2 A logical calculus of rewriting......Page 21
1.3 Annotating formulas......Page 24
1.4 A simple example of rippling......Page 25
1.6 Rewriting with wave-rules......Page 28
1.7 The preconditions of rippling......Page 30
1.8 The bi-directionality of rippling......Page 31
1.9 Proofs by mathematical induction......Page 32
1.9.1 Recursive data types......Page 33
1.9.2 Varieties of induction rule......Page 34
1.9.3 Rippling in inductive proofs......Page 36
1.10 The history of rippling......Page 37
2.1.1 An example of wave-front splitting......Page 40
2.1.2 Maximally split normal form......Page 41
2.1.3 A promise redeemed......Page 42
2.1.5 Unblocking rippling with simplification......Page 43
2.2 Rippling sideways and inwards......Page 44
2.2.1 An example of sideways rippling......Page 45
2.2.2 Universal variables in inductive proofs......Page 47
2.2.4 Cancellation of inwards and outwards wave-fronts......Page 48
2.3.1 An abstract example......Page 49
2.3.2 Another way to look at it......Page 50
2.3.3 A concrete example......Page 51
2.4.1 An example using trees......Page 52
2.4.2 Shaken but not stirred......Page 54
2.4.3 Weakening wave-fronts......Page 55
2.5 Conditional wave-rules......Page 57
2.6 Rippling wave-fronts from given to goal......Page 60
2.7 Higher-order rippling......Page 61
2.8 Rippling to prove equations......Page 64
2.9 Relational rippling......Page 66
2.10 Summary......Page 69
3.1 Eureka steps......Page 70
3.2 Precondition analysis and proof patching......Page 72
3.3 Revising inductions......Page 74
3.3.1 Failure analysis......Page 75
3.3.2 Patch: wave-front speculation......Page 76
3.4.1 Failure analysis......Page 77
3.4.2 Patch: lemma speculation......Page 78
3.4.3 Alternative lemmas......Page 80
3.4.4 Patch: lemma calculation......Page 82
3.5.1 Failure analysis......Page 83
3.5.2 Patch: sink speculation......Page 84
3.5.3 Alternative generalizations......Page 86
3.6.2 Patch: casesplit calculation......Page 89
3.7.1 Rotate length: conjecture generalization......Page 90
3.7.2 Rotate length: lemma discovery......Page 92
3.7.3 An automated reasoning challenge......Page 93
3.8 Implementation and results......Page 94
3.9 Summary......Page 97
4.1 General preliminaries......Page 98
4.1.1 Terms and positions......Page 99
4.1.2 Substitution and rewriting......Page 100
4.1.3 Notation......Page 101
4.2.1 Preliminaries......Page 102
4.2.2 Properties of rippling......Page 103
4.3 Implementing rippling: generate-and-test......Page 104
4.3.1 Embeddings......Page 105
4.3.2 Annotated terms and rippling......Page 106
4.3.3 Implementation......Page 107
4.4.1 The role of annotation......Page 108
4.4.2 Formal definitions......Page 109
4.6 Rippling using wave-rules......Page 112
4.6.1 Why ordinary rewriting is not enough......Page 113
4.6.2 Ground rippling......Page 114
4.6.3 Annotated matching......Page 116
4.6.4 (Non-ground) rippling......Page 119
4.6.5 Termination......Page 120
4.7.1 Simple annotation......Page 121
4.7.2 Multi-hole annotation......Page 124
4.7.3 Termination under......Page 126
4.8 Implementing rippling......Page 129
4.8.1 Dynamic wave-rule parsing......Page 130
4.8.2 Sinks and colors......Page 132
5.1 Hit: bi-directionality in list reversal......Page 134
5.3 Hit: reasoning about imperative programs......Page 136
5.4 Hit: lim+ theorem......Page 137
5.5 Hit: summing the binomial series......Page 138
5.7 Hit: SAM's lemma......Page 139
5.8 What counts as a failure?......Page 140
5.9 Miss: mutual recursion......Page 141
5.10 Miss: commuted skeletons......Page 142
5.11 Miss: holeless wave-fronts......Page 143
5.12 Miss: inverting a tower......Page 145
5.13 Miss: difference removal......Page 147
5.14 Best-first rippling......Page 148
5.15 Rippling implementations and practical experience......Page 149
5.16 Summary......Page 150
6 From rippling to a general methodology......Page 160
6.1 A general-purpose annotation language......Page 162
6.2.1 Example 1: encoding rippling and difference reduction......Page 164
6.2.2 Example 2: encoding basic ordered paramodulation and basic superposition......Page 166
6.2.3 Example 3: Encoding window inference......Page 170
6.2.4 Example 4: Proving theorems by reuse......Page 172
6.2.5 Summary......Page 175
6.3.1 Limitations of abstractions......Page 176
6.3.2 Abstractions on annotated terms......Page 178
Rippling......Page 181
Window inference......Page 183
Reuse of proofs......Page 185
6.4 Implementation......Page 188
6.5 Summary......Page 189
7 Conclusions......Page 191
A1.1 An annotation calculus......Page 193
A1.2 Unification algorithm......Page 199
A1.2.1 Soundness and completeness......Page 204
Appendix 2 Definitions of functions used in this book......Page 206
References......Page 209
Index......Page 216
