| Preface |
|
xi | |
| Acknowledgments |
|
xiv | |
|
An introduction to rippling |
|
|
1 | (23) |
|
|
|
1 | (4) |
|
The problem of automating reasoning |
|
|
1 | (1) |
|
Applications to formal methods |
|
|
2 | (1) |
|
Proof planning and how it helps |
|
|
3 | (1) |
|
Rippling: a common pattern of reasoning |
|
|
3 | (2) |
|
A logical calculus of rewriting |
|
|
5 | (3) |
|
|
|
8 | (1) |
|
A simple example of rippling |
|
|
9 | (3) |
|
Using the given: fertilization |
|
|
12 | (1) |
|
Rewriting with wave-rules |
|
|
12 | (2) |
|
The preconditions of rippling |
|
|
14 | (1) |
|
The bi-directionality of rippling |
|
|
15 | (1) |
|
Proofs by mathematical induction |
|
|
16 | (5) |
|
|
|
17 | (1) |
|
Varieties of induction rule |
|
|
18 | (2) |
|
Rippling in inductive proofs |
|
|
20 | (1) |
|
|
|
21 | (3) |
|
|
|
24 | (30) |
|
|
|
24 | (4) |
|
An example of wave-front splitting |
|
|
24 | (1) |
|
Maximally split normal form |
|
|
25 | (1) |
|
|
|
26 | (1) |
|
|
|
27 | (1) |
|
Unblocking rippling with simplification |
|
|
27 | (1) |
|
Rippling sideways and inwards |
|
|
28 | (5) |
|
An example of sideways rippling |
|
|
29 | (2) |
|
Universal variables in inductive proofs |
|
|
31 | (1) |
|
Revised preconditions for rippling |
|
|
32 | (1) |
|
Cancellation of inwards and outwards wave-fronts |
|
|
32 | (1) |
|
Rippling-in after weak fertilization |
|
|
33 | (3) |
|
|
|
33 | (1) |
|
Another way to look at it |
|
|
34 | (1) |
|
|
|
35 | (1) |
|
Rippling towards several givens |
|
|
36 | (5) |
|
|
|
36 | (2) |
|
|
|
38 | (1) |
|
|
|
39 | (2) |
|
|
|
41 | (3) |
|
Rippling wave-fronts from given to goal |
|
|
44 | (1) |
|
|
|
45 | (3) |
|
Rippling to prove equations |
|
|
48 | (2) |
|
|
|
50 | (3) |
|
|
|
53 | (1) |
|
Productive use of failure |
|
|
54 | (28) |
|
|
|
54 | (2) |
|
Precondition analysis and proof patching |
|
|
56 | (2) |
|
|
|
58 | (3) |
|
|
|
59 | (1) |
|
Patch: wave-front speculation |
|
|
60 | (1) |
|
|
|
61 | (6) |
|
|
|
61 | (1) |
|
|
|
62 | (2) |
|
|
|
64 | (2) |
|
|
|
66 | (1) |
|
|
|
67 | (6) |
|
|
|
67 | (1) |
|
|
|
68 | (2) |
|
Alternative generalizations |
|
|
70 | (3) |
|
|
|
73 | (1) |
|
|
|
73 | (1) |
|
Patch: casesplit calculation |
|
|
73 | (1) |
|
Rotate length conjecture revisited |
|
|
74 | (4) |
|
Rotate length: conjecture generalization |
|
|
74 | (2) |
|
Rotate length: lemma discovery |
|
|
76 | (1) |
|
An automated reasoning challenge |
|
|
77 | (1) |
|
Implementation and results |
|
|
78 | (3) |
|
|
|
81 | (1) |
|
A formal account of rippling |
|
|
82 | (36) |
|
|
|
82 | (4) |
|
|
|
83 | (1) |
|
Substitution and rewriting |
|
|
84 | (1) |
|
|
|
85 | (1) |
|
|
|
86 | (2) |
|
|
|
86 | (1) |
|
|
|
87 | (1) |
|
Implementing rippling: generate-and-test |
|
|
88 | (4) |
|
|
|
89 | (1) |
|
Annotated terms and rippling |
|
|
90 | (1) |
|
|
|
91 | (1) |
|
|
|
92 | (4) |
|
|
|
92 | (1) |
|
|
|
93 | (3) |
|
Structure-preserving rules |
|
|
96 | (1) |
|
Rippling using wave-rules |
|
|
96 | (9) |
|
Why ordinary rewriting is not enough |
|
|
97 | (1) |
|
|
|
98 | (2) |
|
|
|
100 | (3) |
|
|
|
103 | (1) |
|
|
|
104 | (1) |
|
Orders on annotated terms |
|
|
105 | (8) |
|
|
|
105 | (3) |
|
|
|
108 | (2) |
|
|
|
110 | (3) |
|
|
|
113 | (5) |
|
Dynamic wave-rule parsing |
|
|
114 | (2) |
|
|
|
116 | (2) |
|
The scope and limitations of rippling |
|
|
118 | (26) |
|
Hit: bi-directionality in list reversal |
|
|
118 | (2) |
|
Hit: bi-conditional decision procedure |
|
|
120 | (1) |
|
Hit: reasoning about imperative programs |
|
|
120 | (1) |
|
|
|
121 | (1) |
|
Hit: summing the binomial series |
|
|
122 | (1) |
|
Hit: meta-logical reasoning |
|
|
123 | (1) |
|
|
|
123 | (1) |
|
What counts as a failure? |
|
|
124 | (1) |
|
|
|
125 | (1) |
|
|
|
126 | (1) |
|
Miss: holeless wave-fronts |
|
|
127 | (2) |
|
|
|
129 | (2) |
|
|
|
131 | (1) |
|
|
|
132 | (1) |
|
Rippling implementations and practical experience |
|
|
133 | (1) |
|
|
|
134 | (10) |
|
From rippling to a general methodology |
|
|
144 | (31) |
|
A general-purpose annotation language |
|
|
146 | (2) |
|
Encoding constraints in proof search: some examples |
|
|
148 | (12) |
|
Example 1: encoding rippling and difference reduction |
|
|
148 | (2) |
|
Example 2: encoding basic ordered paramodulation and basic superposition |
|
|
150 | (4) |
|
Example 3: Encoding window inference |
|
|
154 | (2) |
|
Example 4: Proving theorems by reuse |
|
|
156 | (3) |
|
|
|
159 | (1) |
|
Using annotations to implement abstractions |
|
|
160 | (12) |
|
Limitations of abstractions |
|
|
160 | (2) |
|
Abstractions on annotated terms |
|
|
162 | (3) |
|
|
|
165 | (7) |
|
|
|
172 | (1) |
|
|
|
173 | (2) |
|
|
|
175 | (2) |
|
Appendix 1 An annotated calculus and a unification algorithm |
|
|
177 | (13) |
|
|
|
177 | (6) |
|
|
|
183 | (5) |
|
Soundness and completeness |
|
|
188 | (2) |
|
Appendix 2 Definitions of functions used in this book |
|
|
190 | (3) |
| References |
|
193 | (7) |
| Index |
|
200 | |
Biežāk uzdotie jautājumi par e-grāmatām