ACL2 Version 4.1
ACL2 is part of the Boyer-Moore family of provers, for which its authors have received the 2005 ACM Software System Award.
|Start Here: Applications, Tours, and Tutorials/Demos||ACL2 Workshops and UT ACL2 Seminar|
|Books and Papers about ACL2 and Its Applications||The User's Manual and Hyper-Card|
|Lemma Libraries and Utilities||Mailing Lists|
|Recent changes to this page||Obtaining and Installing Version 4.1|
|Differences from Version 4.0||Other Releases|
|How to contribute libraries and documentation|
The distribution also includes libraries of books (files
containing definitions and theorems) that extend the code that we have
written. Books are contributed and maintained by the ACL2 community
and their authors are generally noted in each book or its
Another extension of ACL2 is the Eclipse-based ACL2 Sedan (ACL2s). Unlike the systems above, ACL2s is distributed and maintained by Pete Manolios and his research group. ACL2s comes with a standard executable ACL2 image for Windows, but it also comes with pre-certified books and an extension of ACL2 with additional features, including extra automation for termination proofs as well as counterexample generation.
Here are the two common entries to the documentation graph:
|Major Topics (Table of Contents)|
|Index of all documented topics|
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'':
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
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 1700 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
over 2 MB).
workshops'') and non-standard analysis (``
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
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.
Also, if you have written up (or are interested in writing) text that
may be helpful to other ACL2 users, we invite you to contribute it to
the community. Such user documentation may be in any format that is
readable by web browsers (for example html, pdf, and plain text).
User-contributed documentation can link back to the ACL2 documentation
proper, by using links such as:
(In general, substitute the upper-case of the documentation topic for "
MAKE-EVENT" in the example above.)
To contribute user documentation, send email to the ACL2 developers,
for example at