Major Section: ACL2 Documentation

To learn about ACL2, read at least the first two links below. If you want to learn
*how to use* ACL2, we recommend you read the first four links below, in the order
listed.

* 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

* A Walking Tour (1 hour) to get an overview of the theorem prover

* Introduction to the Theorem Prover (10-40 hours)
for instruction on how to interact with the system; this is the first of
these documents in which you are expected 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.

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!

While learning and using ACL2 you might keep in mind the following resources:

* 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).

* Some Annotated ACL2 Scripts and Demos contain relatively elementary proof scripts that have been annotated to help train the newcomer.

* Many books in the `books/`

directory are distributed with ACL2; many 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 is largely subsumed by the Introduction to the Theorem Prover above, but it might help just because it covers much of the tutorial material in a different way.

The topics listed below are a hodge podge, developed over time. Although some of these are not mentioned above, you might find some of those to be useful as well.

### ACL2-AS-STANDALONE-PROGRAM -- Calling ACL2 from another program

### ACL2-SEDAN -- ACL2 Sedan interface

### ALTERNATIVE-INTRODUCTION -- introduction to ACL2

### ANNOTATED-ACL2-SCRIPTS -- examples of ACL2 scripts

### EMACS -- emacs support for ACL2

### INTERESTING-APPLICATIONS -- some industrial examples of ACL2 use

### INTRODUCTION-TO-THE-THEOREM-PROVER -- how the theorem prover works -- level 0

### STARTUP -- How to start using ACL2; the ACL2 command loop

### TIDBITS -- some basic hints for using ACL2

### TIPS -- some hints for using the ACL2 prover