ACL2-tutorial
Tutorial introduction to ACL2
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.
Alternatively, or in addition, there are talks that you can peruse,
many of them introductory in nature.
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 Try ACL2 web site provides
interactive lessons to get you started using ACL2.
- See introduction-to-the-theorem-prover (10-40 hours) for
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 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.
- An Alternative
Introduction document, while largely subsumed by the 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.
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.
Subtopics
- Introduction-to-the-theorem-prover
- How the theorem prover works — level 0
- Pages Written Especially for the Tours
- Pages Written Especially for the Tours
- The-method
- How to find proofs
- Advanced-features
- Some advanced features of ACL2
- Interesting-applications
- Some industrial examples of ACL2 use
- Tips
- Some hints for using the ACL2 prover
- Alternative-introduction
- Introduction to ACL2
- Tidbits
- Some basic hints for using ACL2
- Annotated-ACL2-scripts
- Examples of ACL2 scripts
- Startup
- How to start using ACL2; the ACL2 command loop
- ACL2-as-standalone-program
- Calling ACL2 from another program
- ACL2-sedan
- ACL2 Sedan interface
- Talks
- Some talks about ACL2
- Nqthm-to-ACL2
- ACL2 analogues of Nqthm functions and commands
- Emacs
- Emacs support for ACL2
