About ACL2

Matt Kaufmann and J Strother Moore
Department of Computer Sciences
University of Texas at Austin

Industrial Proofs with ACL2
A five page paper about ACL2, including some industrial-scale examples and information on where to learn more.
(95KB Postscript)
(130 KB PDF)
Recursion and Induction
The best way to learn how to use the ACL2 system is to learn how to do inductive proofs about recursive functions. We therefore recommend that you work your way through Recursion and Induction and solve every exercise. Our answers are also posted but we strongly recommend that you not look at them until you have worked very hard on the problem and explored every possibility you can think of!
Reading our answers doesn't help you! Nevertheless, if you've really given up, you can find the answers here (in the form of an ACL2 input file) and you can see ACL2's output in response to our answers here.
How to Prove Theorems Formally
After you have mastered the material above, quickly go through the material below. It consists of a 47 page paper about how to program in the ACL2 functional programming language, how to prove theorems in the ACL2 logic, and how to use the ACL2 theorem prover. The paper focuses on a very simple subset of the full logic, a dozen or so axioms and informal statements of the definitional and induction principles. The paper has a lot of overlaps with the Recursion and Induction material and you should be able to cover it quickly. But it is valuable because it encourages you to use the ACL2 system and it gives various rules of thumb for succeeding at constructing proofs. The paper has many exercises.
(500 KB Postscript)
(250 KB PDF)

We also include the Latex source, in order to make it easy to quote from this paper. We hereby give permission to quote freely from this paper, provided none of the quoted text is modified and full attribution is given.
main.tex (100 KB Latex source)
main.bib (6 KB bibtex bibliographic database)
llncs.cls (35 KB LNCS file defining documentclass llncs)
acl2.sty (1 KB ACL2 Latex package)

Finally, here are solutions to the exercises and the corresponding prover output. If you are learning to use ACL2, try to avoid the temptation to look at the solutions until after you have attempted the exercises yourself.
(24 KB exercise solutions)
(200 KB exercise solutions output)
Additional Tutorial Material
- An ACL2 Demo Given At TPHOLs 2008 includes a web page with helpful links, in particular to three individual demos that illustrate how to use ACL2 effectively.
- A focus on ACL2's interactive capabilities is offered by a talk given at UITP 2008. We may extend this page in the future; suggestions are welcome.
- See also the ACL2 home page for links to demos, tutorials, and documentation. In particular, you can follow links to the ACL2-TUTORIAL documentation topic.
ACL2 Home Page

About ACL2

Industrial Proofs with ACL2

Recursion and Induction

How to Prove Theorems Formally

Additional Tutorial Material

ACL2 Home Page