Major Section: ACL2 Documentation
To learn about ACL2, read at least the following two links.
* Industrial Applications of ACL2 (10 minutes) to help you understand what sophisticated users can do;
* A Flying Tour (10 minutes) to get an overview of the system and what skills the user must have.
If you want to learn how to use ACL2, we recommend that you read a selection of the materials referenced below, depending on your learning style, and do suggested exercises.
* ``A Walking Tour'' (1 hour) provides an overview of the theorem prover.
* The external site http://tryacl2.org provides interactive lessons to get you started using ACL2.
* ``Introduction to the Theorem Prover'' (10-40 hours) provides instruction on how to interact with the system. Unlike the three documents above, this document expects you to think! It cites the necessary background pages on programming in ACL2 and on the logic and then instructs you in The Method, which is how expert users use ACL2. It concludes with some challenge problems for the ACL2 beginner (including solutions) and an FAQ. Most users will spend several hours a day for several days working through this material.
* The book ''Computer-Aided Reasoning: An Approach'' (see http://www.cs.utexas.edu/users/moore/publications/acl2-books/car/index.html is worth a careful read, as you work exercises and learn ``The Method.''
* ``Annotated ACL2 Scripts and Demos'' contains relatively elementary proof scripts that have been annotated to help train the newcomer.
* Many files (``books'') in the ACL2 community books (see community-books) are extensively annotated. See the link to ``Lemma Libraries and Utilities'' on the ACL2 home page (http://www.cs.utexas.edu/users/moore/acl2).
* An ``Alternative Introduction'' document, while largely subsumed by the topic ``Introduction to the Theorem Prover'' mentioned above, still might be useful because it covers much of the tutorial material in a different way.
At this point you are probably ready to use ACL2 on your own small projects. A common mistake for beginners is to browse the documentation and then try to do something that is too big! Think of a very small project and then simplify it!
Note that ACL2 has a very supportive user network. See the link to ``Mailing Lists'' on the ACL2 home page (http://www.cs.utexas.edu/users/moore/acl2).
The topics listed below are a hodge podge, developed over time. Although some of these are not mentioned above, you might find some to be useful as well.
