By Alan Bundy
By David Basin
By Dieter Hutter
By Andrew Ireland
Publisher: Cambridge University Press
Print Publication Year: 2005
Online Publication Date:August 2009
Online ISBN:9780511543326
Hardback ISBN:9780521834490
Chapter DOI: http://dx.doi.org/10.1017/CBO9780511543326.002
Subjects: Algorithmics, Complexity, Computer Algebra, Computational Geometry, Logic, categories and Sets
Image View Extract Fullview: Text View | Enlarge Image ‹ Previous Chapter ›Next Chapter
Overview
This book describes rippling, a new technique for automating mathematical reasoning. Rippling captures a common pattern of reasoning in mathematics: the manipulation of one formula to make it resemble another. Rippling was originally developed for proofs by mathematical induction; it was used to make the induction conclusion more closely resemble the induction hypotheses. It was later found to have wider applicability, for instance to problems in summing series and proving equations.
The problem of automating reasoning
The automation of mathematical reasoning has been a long-standing dream of many logicians, including Leibniz, Hilbert, and Turing. The advent of electronic computers provided the tools to make this dream a reality, and it was one of the first tasks to be tackled. For instance, the Logic Theory Machine and the Geometry Theorem-Proving Machine were both built in the 1950s and reported in Computers and Thought (Feigenbaum & Feldman, 1963), the earliest textbook on artificial intelligence. Newell, Shaw and Simon's Logic Theory Machine (Newell et al., 1957), proved theorems in propositional logic, and Gelernter's Geometry Theorem-Proving Machine (Gelernter, 1963), proved theorems in Euclidean geometry.
This early work on automating mathematical reasoning showed how the rules of a mathematical theory could be encoded within a computer and how a computer program could apply them to construct proofs. But they also revealed a major problem: combinatorial explosion. Rules could be applied in too many ways.
pp. i-vi
pp. vii-x
pp. xi-xiii
pp. xiv-xiv
1 - An introduction to rippling : Read PDF
pp. 1-23
2 - Varieties of rippling : Read PDF
pp. 24-53
3 - Productive use of failure : Read PDF
pp. 54-81
4 - A formal account of rippling : Read PDF
pp. 82-117
5 - The scope and limitations of rippling : Read PDF
pp. 118-143
6 - From rippling to a general methodology : Read PDF
pp. 144-174
pp. 175-176
Appendix 1 - An annotated calculus and a unification algorithm : Read PDF
pp. 177-189
Appendix 2 - Definitions of functions used in this book : Read PDF
pp. 190-192
pp. 193-199
pp. 200-202