ACL2 Version 1.9

ACL2 is both a programming language in which you can model computer systems and a tool to help you prove properties of those models.

Two short tours of ACL2
A Paper about Some Industrial Applications of ACL2.
Tutorials (for those who have taken the tours)
Scientific Papers about ACL2 and Its Applications
The User's Manual
Mathematical Tools (Lemmas Libraries and Utilities)
Downloading ACL2
Matt Kaufmann and J Strother Moore
Computational Logic, Inc. (CLI)
June 16, 1997

Scientific Papers about ACL2 and Its Applications

We recommend you read the first two papers listed below, and then whatever others seem interesting to you.

The User's Manual

ACL2's user manual is a vast hypertext document. You can wander through it here, in its HTML format.

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 the tours.

If you are a serious ACL2 student and have taken the tours and done the tutorials, 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/. 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.5 megabytes of postscript (which prints as an 800 page book), HTML, EMAC's Texinfo, and ACL2's own :DOC commands. The documentation, in all four forms, is distributed with the source code for the system. See the doc/ subdirectory of the directory upon which ACL2 is installed.

Mathematical Tools

The distribution of ACL2 includes several additional tools. These tools are part of what you get when you obtain ACL2; there is no need to download anything because if you have ACL2 Version 1.9, you have these tools. You just may not know it! The pathnames below are relative to the directory on which ACL2 was installed.

License, Runtime Images and Sources

ACL2 Version 1.9 -- A Computational Logic for Applicative Common Lisp
Copyright (C) 1997 Computational Logic, Inc.

This program is free software; you can redistribute it and/or modify it under the terms of version 2 (or, at your option, any later version) of the GNU General Public License.

This program is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License for more details.

Computational Logic, Inc..