Daniel P. Friedman - The Little Prover

It automatically uses structural induction when necessary, and automatically generates its own induction formulas. It will occasionally generalize the theorem to be proved, and in so doing, often discovers interesting lemmas. Finally, it is capable of writing new, recursive LISP functions to help properly generalize a theorem. How is mathematical logic used to describe the behavior of functions or programs? What is a theorem? How do you prove theorems? What is an automatic theorem prover? What do all these mathematical termsinduction, generalization, lemmahave to do with programs being correct? How can programmers intuition guide a foray into mathematics? How do you think about programs that call themselves without just going in circles? These are some of the questions Bob and I had to answer when we began writing the program described above. Our answers are still evolving 40 years later and are currently manifested in ACL2, the living descendant of the prover above. But while our code is well documented and available for study, the answers to the above questions are not always explicit in it.

Sometimes, the best way to learn how to do something is just to sit down and try to do it. There are two problems with that advice and the problems are especially acute when mathematical logic is involved. First, you have to understand the rules of the game. Those rulesif followed exactlywill ensure that what you prove is really true. Second, it is hard to keep in mind the precise statement of every ruleand if you make a mistake you might end up believing something is true when it is not. This little book and the accompanying little assistant addresses both of these problems.

The book itself provides you with a gentle introduction to the mathematics behind all of this. It presents the rules in a way geared toward the programmer. Indeed the rules themselves are largely intuitive to the programmer. Second, the assistant enforces the rules for you. But unlike the automatic theorem provers that I create, their assistant is designed to enforce the rules while allowing you to learn by doing. The offer here is: the prover will make sure the formulas are formulas and the proofs are proofs.

But youre the intelligent actor: so what do you do now? J Strother Moore Austin, Texas

When we evaluate (reverse (reverse '(1 2))) , we reach the result '(1 2) , exactly as we expect. Furthermore, evaluating a recursive function follows a predictableand fortunately, often simpleset of rules. We can therefore answer more general questions. For instance, does (reverse (reverse x)) always produce x for any list? We can determine the answer without ever evaluating the expression or even knowing the specific value of x . Our goal is to teach the reader how to determine facts about recursive functions using induction. Our approach is to start with programming concepts such as recursive functions and lists, and to lead the reader along the shortest path to inductive proofs.

We aim to teach enough to verify simple properties such as whether (reverse (reverse x)) always produces x for any list, although we leave that particular example as an exercise for the reader. Understanding how to read, write, and evaluate recursive functions over lists is adequate preparation. We assume knowledge of neither logic nor mathematics beyond arithmetic. We express as much as we can using simple programming concepts. Acknowledgements We have many people to thank for their contributions to this book. Thanks, as always, to Dorai Sitaram for the typesetting program.

Thanks to Jared Davis, whose dissertation on the theorem prover Milawa has been a useful reference for the core of ACL2s logic. For help with ACL2 and the implementation of dethm , we thank Pete Manolios and Matt Kaufmann. We are also grateful to J Moore and Bob Boyer for their contributions to theorem proving research and for allowing us to name our little proof assistant, J-Bob, after them. We thank our mentors and inspirations for teaching and guiding us: Will Byrd, Matthias Felleisen, Bob Filman, George Springer, and Mitch Wand. We especially want to thank Matthias for forging our partnership. Thanks to our early supporters: Adam Foltzer, Ron Garcia, Amr Sabry, Christian Urban, and Yin Wang, and everyone else who has been kind and helpful.

Thanks to Jason Hemann, who has given us endless help, support, and feedback on drafts of the book and the implementation of J-Bob. For their feedback on drafts, thanks to Conrad Barski, Daniel Brady, Will Byrd, Kyle Carter, Josh Cox, Jim Duey, Matthias Felleisen, Bob Filman, Adam Foltzer, Ron Garcia, Jaime Guerrero, Jason Hemann, Joe Hendrix, Andrew Kent, J Moore, Joe Near, Rex Page, Paul Snively, Vincent St-Amour, Dylan Thurston, Christian Urban, Dale Vaillaincourt, Michael Vanier, and Dave Yrueta. Thanks to our illustrator, Duane Bibby, for illustrations, for inspiration, and for coming through with our last-minute requests. Special thanks to our editor, Marie Lufkin Lee, for helping us throughout the process of bringing this book to its final form. We also thank our hosts for the many visits to Bloomington, where most of our work took place. Thanks to our friends Katie Edmonds and Sam Tobin-Hochstadt for hosting one such visit, and our eternal gratitude to Mary Friedman for hosting all of the others, for graciously tolerating our constant postponements and demands on her time, and for supporting this book every step of the way.