To obtain ACL2 by ftp, first connect to ftp.cli.com by anonymous login. Then
`cd' to ~acl2/v1-8, `get' the file `README' and follow the directions therein.
To obtain ACL2 by magnetic tape (for which service a fee shall be charged)
write to Software-Request, Computational Logic Inc., 1717 West Sixth, Suite
290, Austin, TX 78703-4776, USA; email: Software-Request@cli.com. FAX: +1
512 322 0656.
If you would like to join the unmoderated ACL2 mailing list, acl2@cli.com, send
to acl2-request@cli.com a message containing as its body (NOT its Subject) the
the single word `subscribe'. To get general information about the mailing
list, send the word `info' (this will not subscribe you to the mailing list).
To send a message to all who receive ACL2 mail, send the message to
acl2@cli.com. Finally, please report bugs in ACL2 to acl2-bugs@cli.com.
The ACL2 logic is a first-order logic of recursive functions providing
mathematical induction on the ordinals up to epsilon-0 and two extension
principles: one for recursive definition and one for constrained introduction
of new function symbols. First-order quantification is supported in a weak
sense using a ``choice'' operator.
The syntax of ACL2 is that of Common Lisp. Constants and macros may be defined
and used to extend the syntax.
The following primitive data types are axiomatized: rational numbers
(including, of course, integers and naturals), complex rationals, characters,
character strings, symbols (including packages), and conses. All primitive
Common Lisp functions on the above data types are (meant to be) defined in
ACL2. By ``Common Lisp function'' we mean any function described in ``Common
Lisp The Language,'' by Guy Steele (Digital Press, 30 North Avenue, Burlington,
MA 01803, 1984 and 1990), that is applicative, is not dependent on state,
implicit parameters or data types other than those listed above, and is
completely and unambiguously specified in a host-independent manner.
Approximately 170 such symbols are axiomatized.
To applicative Common Lisp ACL2 adds a single-threaded notion of ``state''
allowing the efficient provision of one and two dimensional arrays, property
lists, and file directed input and output within the applicative setting. In
addition, ACL2 adds notions of multi-valued function call and return and a
number of other useful primitives.
The ACL2 system allows the definition of new function symbols and the proofs of
theorems about those symbols. Like Nqthm, the behavior of the theorem proving
engine is determined by rules derived from previously introduced functions and
theorems. ACL2 provides many ``rule classes'' by which the user can specify
how a theorem is to affect the behavior of the theorem prover. ACL2 also
provides
* an interactive capability like that of Pc-Nqthm;
* more user control of proofs than Nqthm, via hints and scoping mechanisms;
* improved handling of propositional logic (including use of BDDs);
* a specification capability (``guards'') akin to types, but more flexible;
* proof techniques in addition to those of Nqthm, including forward chaining,
congruence-based rewriting, forced case-splits, and built-in clauses for
termination proofs;
* extensive hyper-linked on-line documentation available via ACL2 documentation
commands, HTML browsers and Emacs Info; and
* a ``proof-tree'' facility that makes it easy to explore failed proof
attempts.
ACL2 has seen heavy in-house use at Computational Logic, Inc., for
approximately 2 years. Several major projects have been carried out with it.
However, it has not received the extensive scrutiny that Nqthm has and bugs --
possibly even soundness bugs -- may crop up. Please report them to
acl2-bugs@cli.com, so that we can fix them and notify other users.
ACL2, including the source code, is available electronically without fee.
However, use of ACL2 signifies the user's agreement to abide by the terms of a
license agreement distributed as part of the system.
ACL2 currently works on the Unix (and some variants, including Linux) and
Macintosh operating systems. It is built on top of any of the following Common
Lisps: Allegro, GCL (Gnu Common Lisp) [or, AKCL], Lispworks, Lucid, and MCL
(Macintosh Common Lisp). We recommend running ACL2 with at least 16MB of
memory.