Rippling: Meta-Level Guidance for

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.

Preface

xi

Acknowledgments

xiv

An introduction to rippling

1

(23)

Overview

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)

Annotating formulas

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)

Recursive data types

17

(1)

Varieties of induction rule

18

(2)

Rippling in inductive proofs

20

(1)

The history of rippling

21

(3)

Varieties of rippling

24

(30)

Compound wave-fronts

24

(4)

An example of wave-front splitting

24

(1)

Maximally split normal form

25

(1)

A promise redeemed

26

(1)

Meta-rippling

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)

An abstract example

33

(1)

Another way to look at it

34

(1)

A concrete example

35

(1)

Rippling towards several givens

36

(5)

An example using trees

36

(2)

Shaken but not stirred

38

(1)

Weakening wave-fronts

39

(2)

Conditional wave-rules

41

(3)

Rippling wave-fronts from given to goal

44

(1)

Higher-order rippling

45

(3)

Rippling to prove equations

48

(2)

Relational rippling

50

(3)

Summary

53

(1)

Productive use of failure

54

(28)

Eureka steps

54

(2)

Precondition analysis and proof patching

56

(2)

Revising inductions

58

(3)

Failure analysis

59

(1)

Patch: wave-front speculation

60

(1)

Lemma discovery

61

(6)

Failure analysis

61

(1)

Patch: lemma speculation

62

(2)

Alternative lemmas

64

(2)

Patch: lemma calculation

66

(1)

Generalizing conjectures

67

(6)

Failure analysis

67

(1)

Patch: sink speculation

68

(2)

Alternative generalizations

70

(3)

Case analysis

73

(1)

Failure analysis

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)

Summary

81

(1)

A formal account of rippling

82

(36)

General preliminaries

82

(4)

Terms and positions

83

(1)

Substitution and rewriting

84

(1)

Notation

85

(1)

Properties of rippling

86

(2)

Preliminaries

86

(1)

Properties of rippling

87

(1)

Implementing rippling: generate-and-test

88

(4)

Embeddings

89

(1)

Annotated terms and rippling

90

(1)

Implementation

91

(1)

Term annotation

92

(4)

The role of annotation

92

(1)

Formal definitions

93

(3)

Structure-preserving rules

96

(1)

Rippling using wave-rules

96

(9)

Why ordinary rewriting is not enough

97

(1)

Ground rippling

98

(2)

Annotated matching

100

(3)

(Non-ground) rippling

103

(1)

Termination

104

(1)

Orders on annotated terms

105

(8)

Simple annotation

105

(3)

Multi-hole annotation

108

(2)

Termination under *

110

(3)

Implementing rippling

113

(5)

Dynamic wave-rule parsing

114

(2)

Sinks and colors

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)

Hit: lim+ theorem

121

(1)

Hit: summing the binomial series

122

(1)

Hit: meta-logical reasoning

123

(1)

Hit: SAM's lemma

123

(1)

What counts as a failure?

124

(1)

Miss: mutual recursion

125

(1)

Miss: commuted skeletons

126

(1)

Miss: holeless wave-fronts

127

(2)

Miss: inverting a tower

129

(2)

Miss: difference removal

131

(1)

Best-first rippling

132

(1)

Rippling implementations and practical experience

133

(1)

Summary

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)

Summary

159

(1)

Using annotations to implement abstractions

160

(12)

Limitations of abstractions

160

(2)

Abstractions on annotated terms

162

(3)

Examples revisited

165

(7)

Implementation

172

(1)

Summary

173

(2)

Conclusions

175

(2)

Appendix 1 An annotated calculus and a unification algorithm

177

(13)

An annotation calculus

177

(6)

Unification algorithm

183

(5)

Soundness and completeness

188

(2)

Appendix 2 Definitions of functions used in this book

190

(3)

References

193

(7)

Index

200

What is included with this book?

The New copy of this book will include any supplemental materials advertised. Please check the title of the book to determine if it should include any access cards, study guides, lab manuals, CDs, etc.

The Used, Rental and eBook copies of this book are not guaranteed to include any supplemental materials. Typically, only the book itself is included. This is true even if the title states it includes any access cards, study guides, lab manuals, CDs, etc.

FREE SHIPPING

Amazon no longer offers textbook rentals. We do!

Rippling: Meta-Level Guidance for Mathematical Reasoning

Summary

Table of Contents

Supplemental Materials