2024-03-07
I’m trying to figure out what computational logic (theorem proving, formal methods, automated reasoning, etc.) is all about. Below are some of my notes, along with interesting resources I’ve found. I’ll keep adding to it as I go.
Feel free to email me if you have any suggestions, comments, criticisms, or questions. I don’t get much email, so I will most likely respond to you. You can find my email address here.
Disclaimer: This is my informal survey of the field; I make no guarantees on correctness.
https://www.cs.utexas.edu/users/moore/acl2/
https://en.wikipedia.org/wiki/ACL2
ACL2 is a system for proving theorems about programs written in a special subset of Common Lisp. For many theorems, the system can automatically generate a proof without any help.
Interestingly, ACL2 is able to avoid the use of quantifiers (like “for all”) by using recursive functions instead.
It should be noted that ACL2 is only a first-order logic, which means you can’t pass functions as inputs to other functions (here’s an example). For someone used to programming in a language like Scheme, this is a big restriction. However, I believe the restriction is here because it makes it much easier to prove that a function always terminates and returns a value, which is a requirement for proving any theorems about the function.
https://mitpress.mit.edu/9780262527958/the-little-prover/
If you know Scheme and want to learn how theorem proving works, this is the book for you.
It shows how to manually prove theorems about programs written in a subset of Scheme. It is heavily inspired by ACL2.
The book also comes with a proof checker called J-Bob. J-Bob has no automated theorem proving capabilities; each step of the proof (taking the form of a rewrite rule) must be manually specified by the user. J-Bob can check that a proof was done correctly and can also show the state of a proof still in-progress (for interactive use). J-Bob is written entirely in the subset of Scheme on which it operates. The source code for it is printed in the book.
At first glance The Little Prover looks like a children’s book, but I promise it’s not. It’s part of a series of books that use an unusual question-and-answer dialog style to intuitively explain traditionally difficult-to-understand computer science concepts. It’s worth taking a look.
https://www.cs.utexas.edu/users/boyer/acl.pdf
This book presents the precursor to ACL2: Nqthm. It explains the need for automated theorem provers, shows how functions and theorems are defined, gives examples of program correctness proofs and mathematical proofs, and discusses in-depth the strategies used to generate proofs.
This book is interesting from a historical perspective and from the perspective of someone trying to figure out how theorem provers work internally. If your only goal is to learn how to use a theorem prover, this is not the best resource.
https://en.wikipedia.org/wiki/Principia_Mathematica
This is a famous three-volume work written as an attempt to formally define the foundations of mathematics.
It’s relevant here because of the approach Whitehead and Russell took: the first thing they did was formally define a notation for mathematical statements and a set of rules for deducing new statements from existing statements. The rest of it is spent defining and proving various mathematical concepts using their notation. It reads like a programming textbook, which is remarkable because it was published way back in 1910!
I only read the introduction and most of part 1 of volume 1 (around 300 pages). Nobody reads the whole thing (around 2,000 pages) because most of it is long proofs written in their formal notation; it’s like reading source code.
Their formal notation is a bit unusual (instead of using parentheses to group expressions, they use groups of dots as an infix notation for linking operators to expressions), but it’s not too bad once you figure it out.
The writing itself is very clear and readable, which I did not expect for a book written over a hundred years ago. It avoids the overly-academic english that so much technical writing tends to suffer from. In fact, it was easier to read than many research papers I’ve read that were written less than ten years ago.