ACL2 Version 2.3

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		Tutorials (for those who have taken the tours)
	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.3
	Differences with Version 2.2		Home Page for Version 2.2

Matt Kaufmann and J Strother Moore
University of Texas at Austin
October 18, 1998

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'':

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: 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. 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 compressed postscript form of the documentation by clicking here.

Mathematical Tools

The distribution of ACL2 includes some tools built by users, summarized below. In addition, see the previously mentioned Papers about ACL2 and Its Applications, since some ``papers'' include ACL2 books or extensions.

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/top-with-meta -- elementary arithmetic
- ihs/README -- this file is a guide to a collection of books supporting integer hardware specification, e.g., FLOOR, MOD, LOGAND, etc.
- data-structures/list-defuns -- definitions of list functions
- data-structures/list-defthms -- theorems about list functions
- data-structures/deflist -- a tool for defining typed lists
- data-structures/list-theory -- brings in all three of the above books
- data-structures/set-defuns -- definitions of set functions
- data-structures/set-defthms -- theorems about set functions
- data-structures/set-theory -- brings in both the definitions and theorems
- data-structures/alist-defuns -- definitions of alist functions
- data-structures/alist-defthms -- theorems about alist functions
- data-structures/defalist -- a tool for defining typed alists
- data-structures/alist-theory -- brings in all three of the above books
- data-structures/number-list-defuns -- definitions about lists of numbers
- data-structures/number-list-defthms -- theorems about number list functions
- data-structures/number-list-theory -- brings in both the definitions and theorems
- data-structures/structures -- a tool for definining typed record structures
You may include these books into an ACL2 session by executing the event (include-book 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 distributivity-of-minus-over-plus
     {-(x + y) = -x + -y};

    Theorem car-nth-0 { 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 doc-strings. 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.

Useful Addresses

To join the ACL2 mailing list, send a message to acl2-request@cs.utexas.edu. We handle the mailing list manually.
To send a message to all who receive ACL2 mail, send the message to acl2@cs.utexas.edu. To protect users from junk mail, messages are not broadcast to the full mailing list until they have been screened by one of the ACL2 principals.
Finally, please report bugs in ACL2 to acl2-bugs@cs.utexas.edu.

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