
ACL2 Version 2.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.

Matt Kaufmann and J Strother Moore
University of Texas at Austin
December 8, 1997
We recommend you read the first two papers listed below, and then whatever
others seem interesting to you.
 ACL2 Theorems about Commercial
Microprocessors (with Bishop Brock)  sketches the system and two
industrial appliations: the AMD5K86 floatingpoint division proof and the
Motorola CAP DSP model.
 An Industrial Strength Theorem Prover for
a Logic Based on Common Lisp  discusses how we scaled up the Nqthm
(``BoyerMoore'') logic to Common Lisp, preserving the use of total functions
within the logic but achieving Common Lisp execution speeds, via the
introduction of ``guards.''
 A Precise Description of the ACL2
Logic  a working draft of a precise description of the base logic.
The draft does not describe the theorem prover or the system; it is a
dry mathematical document describing the logic from first principles. At
the moment the description omits multiple values, property lists, arrays,
state, and macros.
 A
Mechanically Checked Proof of the Correctness of the Kernel of the AMD5K86
FloatingPoint Division Algorithm (with Tom Lynch)  the mathematical
details of the floatingpoint division proof.
 Interactive Consistency in ACL2
(by Bill Young)  an ACL2 translation of Rushby's PVS improvement to
Bevier and Young's Nqthm formalization of the Pease, Shostak and Lamport Oral
Messages (``Byzantine Generals'') problem.
 The Specification of a Simple Autopilot
in ACL2 (by Bill Young)  an ACL2 translation of Butler's PVS
formalization of a simple autopilot.
 Mechanized Formal Reasoning about
Programs and Computing Machines (by Boyer and Moore)  explains a
formalization style which has been extremely successful in enabling mechanized
reasoning about programs and machines, illustrated in ACL2.
 Defstructure for ACL2 (by Bishop
Brock)  documentation for the ACL2
defstructure
book,
which provides a ``record facility'' similar to Common Lisp's
defstruct
and Nqthm's addshell
.
 Design Goals for ACL2  an early
report identifying aspects of Nqthm of special concern during the design of
ACL2.
 ACL2
Documentation  the complete ACL2 documentation tree in the form of a
compressed (gzip'd) postscript file. When uncompressed the documentation is
approximately 3.5 megabytes of postscript and prints as an 800 page book. The
documentation is most useful in its HTML or Texinfo forms, where the links in
it can be browsed interactively. The complete HTML documentation tree is
available below.
Recommended Web sites on formal methods and automated reasoning systems:
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:
The tiny warning signs, , indicate that the links lead out of
introductory level material and into userlevel 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'':
 EVENTS
 the toplevel commands like
DEFUN
and DEFTHM
 PROGRAMMING
 all the Common Lisp functions ACL2 supports
 RULECLASSES
 how you can influence ACL2's behavior with rules,
 BOOKS
 how to create reusable 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/v20
. Then the local URL for this page is
file:/usr/jones/acl2/v20/acl2sources/doc/HTML/acl2doc.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: 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.
The distribution of ACL2 includes several additional tools.
 Books Built by Experts
In its native state, ACL2 ``knows'' very little about arithmetic and other
commonly used mathematical theories. Such knowledge is imparted to ACL2 in the
form of ``books'' written by users; books contain definitions and theorems that
ACL2 interprets as rules to guide its search for a proof. Users have
written some books that may help you. We list a few of them here. The pathnames
below are relative to the books/
subdirectory of the ACL2 directory.
arithmetic/topwithmeta
 elementary arithmetic
datastructures/listdefuns
 definitions of list functions
datastructures/listdefthms
 theorems about list functions
datastructures/deflist
 a tool for defining typed lists
datastructures/listtheory
 brings in all three of the above books
datastructures/setdefuns
 definitions of set functions
datastructures/setdefthms
 theorems about set functions
datastructures/settheory
 brings in both the definitions and theorems
datastructures/alistdefuns
 definitions of alist functions
datastructures/alistdefthms
 theorems about alist functions
datastructures/defalist
 a tool for defining typed alists
datastructures/alisttheory
 brings in all three of the above books
datastructures/numberlistdefuns
 definitions about lists of numbers
datastructures/numberlistdefthms
 theorems about number list functions
datastructures/numberlisttheory
 brings in both the definitions and theorems
datastructures/structures
 a tool for definining typed record structures
You may include these books into an ACL2 session by executing the event
(includebook name)
, where name
is the full pathname of the
book.
 Infix Printing
An infix syntax for ACL2 has been implemented by Michael Smith. Two
capabilities are supported.
 IACL2 is an infix version of the ACL2
theorem proving system that performs I/O in infix
format. It is intended to make initial
experiments with ACL2 somewhat simpler for those unfamiliar with or
opposed to Lisp prefix syntax. (It is not an interface for experts, as
some of the more advanced aspects of ACL2 are not supported by the
infix parser.) Some examples of the syntax:
Function idiv (m : integer, n : integer  n ~= 0)
{ ifix ( m/n ) };
/* Idiv takes two integer arguments, the second of which cannot = zero */
Theorem distributivityofminusoverplus
{(x + y) = x + y};
Theorem carnth0 { consp(x) > x.car = x[0] };
 We provide formatting support to help the user publish ACL2 event
files. The syntax produced is either standard ACL2 or ``conventional''
infix mathematical notation with formatted comments and
docstrings. For example, in LaTeX mode comments are formatted as
running text, events are indexed and substitutions are made of LaTeX
mathematical symbols for various functions. In HTML mode, cross
references are created from function usage to definition. Other ouput
modes include Scribe and ASCII text. The formatting conventions are
user extensible.
For more information, see the
README overview.
University of Texas at Austin.