ACL2 Version 3.1 ACL2 is both a programming language in which you can model computer systems and a tool to help you prove properties of those models. ACL2 is part of the Boyer-Moore family of provers, for which its authors have received the 2005 ACM Software System Award. SEARCH

	Tours and demos		ACL2 Workshops, UT ACL2 Seminar, and Upcoming Conferences
	Books and Papers about ACL2 and Its Applications		The User's Manual and Hyper-Card
	Mathematical Tools (Lemma Libraries and Utilities); and, How to Contribute		Mailing Lists
	Recent changes to this page		Obtaining and Installing Version 3.1
	Differences with Version 3.0		Other Releases
	Matt Kaufmann and J Strother Moore University of Texas at Austin November 28, 2006		We gratefully acknowledge substantial support from the following. (These are included in a much more complete acknowledgments page.) DARPA National Science Foundation (Any opinions, findings and conclusions or recomendations expressed in this material are those of the author(s) and do not necessarily reflect the views of the National Science Foundation (NSF).) Advanced Micro Devices, Inc. Rockwell Collins, Inc. Sun Microsystems, Inc.

The User's Manual

Here are the two common entries to the documentation graph:

	Major Topics (Table of Contents)
	Index of all documented topics

The tiny warning signs, , indicate that the links lead out of introductory level material and into user-level material. It is easy for the newcomer to get lost.

Here is how we recommend you use this documentation.

If you are a newcomer to ACL2, we do not recommend that you wander off into the full documentation. Instead start with the tours and perhaps the demos.

If you are still interested in ACL2, we recommend that you get a copy of Computer-Aided Reasoning: An Approach and read it carefully. Work the exercises with ACL2. Learn ``The Method.''

Less effective than reading the book and doing the exercises, but still useful, is to read selected papers from Books and Papers about ACL2 and Its Applications, read the documentation topic the-method, and the Hyper-Card and then work your way through the tutorials.

Then, we recommend you read selected topics from ``Major Topics'':

• EVENTS -- the top-level commands like DEFUN and DEFTHM
• PROGRAMMING -- all the Common Lisp functions ACL2 supports
• RULE-CLASSES -- how you can influence ACL2's behavior with rules,
• BOOKS -- how to create re-usable databases of rules.

Finally, experienced users tend mostly to use the ``Index'' to lookup concepts mentioned in error messages or vaguely remembered from their past experiences with ACL2.

Note: If ACL2 has been installed on your local system, the HTML documentation should also be available locally. You can minimize network traffic by browsing your local copy. Suppose ACL2 was installed on /usr/jones/acl2/vi-j. Then the local URL for this page is
file:/usr/jones/acl2/vi-j/acl2-sources/doc/HTML/acl2-doc.html.
Many ACL2 users set a browser bookmark to this file and use their browser to access the documentation during everyday use of ACL2. If you obtain ACL2, please encourage users to use the local copy of the documentation rather than access it across the Web.

Note: The documentation is available in four forms: Postscript (which prints as a book over 1200 pages long), HTML, EMACS Texinfo, and ACL2's own :DOC commands. The documentation, in all but the Postscript form, is distributed with the source code for the system. So if you have already obtained ACL2, you should look in the doc/ subdirectory of the directory upon which ACL2 is installed. You may obtain the gzipped Postscript form of the documentation by clicking here (1.4 MB).

Mathematical Tools

We strongly encourage users to submit additional books by following the instructions for contributing books to ACL2.

We also distribute a few interface tools, such as support for infix printing. For these, see the Utilities section of Books and Papers about ACL2 and Its Applications. Some of the papers mentioned in that collection contain utilities, scripts, or ACL2 books the problem domains in question.