Rippling: Meta-Level Guidance for Mathematical Reasoning

by Alan Bundy , David Basin , Dieter Hutter , Andrew Ireland

• ISBN13: 9780521834490
• ISBN10: 052183449X
• Format: Hardcover
• Copyright: 2005-08-08
• Publisher: Cambridge University Press

Summary

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.

Table of Contents

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