ACL2 Version 2.5
|Two short tours of ACL2||FAQ|
|Books and Papers about ACL2 and Its Applications||The User's Manual and Hyper-Card|
|Mathematical Tools (Lemma Libraries and Utilities)||Useful Addresses|
|Recent changes to this page||Obtaining and Installing Version 2.5|
|Differences with Version 2.4||Home Page for Version 2.4|
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.
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: 3.7
megabytes of Postscript (which prints as a book almost 900 pages long), HTML,
EMAC's Texinfo, and ACL2's own :DOC commands (only if you build the ``large''
version of the system). 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 MB).