@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@
Name: ACL2
Keywords: applicative Common Lisp, recursion, induction, arithmetic, lists,
fast prototyping, executable, bdd, floating point, microprocessor
Description:
Semantics: applicative subset of Common Lisp, including macros;
extended with a single-threaded state, fast applicative arrays, and
property lists, and with constrained introduction of undefined functions
for specification purposes.
Deductive machinery: automatic theorem prover driven by an incrementally
constructed data base of previously proved theorems; decision procedures
for propositional calculus, equality, and linear arithmetic; integrated
heuristics for congruence-based rewriting, backwards and forward chaining,
destructor elimination, generalization, and induction; user supplied
meta-theoretic simplifiers; elaborate hint mechanism including use of BDDs;
interactive ``proof checker'' built-in;
Dynamics: packages, encapsulation, books, and theories provide name and
rule scoping; use is made of the fact that ACL2 is a safe programming
language in which hints and prover advice can be expressed and codified
Persistence: books are incrementally loadable source files containing events
such as defuns, theorems and theory definitions
Contact persons:
moore@cs.utexas.edu
kaufmann@aus.edsr.eds.com
User group:
user mailing list: acl2@cs.utexas.edu
to subscribe: acl2-request@cs.utexas.edu. We handle the mailing list
manually.
bugs reports: acl2-bugs@cs.utexas.edu.
Pragmatics:
Strengths: ACL2 is an ``industrial strength'' version of Boyer and Moore's
Nqthm, supporting as a logic (and programmed in) a large applicative subset
of Common Lisp. Chances are if Nqthm can do it, ACL2 can do it and it will
be somewhat easier. However, Nqthm event scripts are not ACL2 compatible
(see weaknesses below).
Unlike Nqthm, ACL2 supports the rational numbers, complex rationals,
character objects, character strings, and symbol packages. However,
ACL2 does not support user defined ``shells.''
Formal models written in ACL2 are usually executable (the exception being
those that use undefined functions) and can execute much faster than Nqthm
models.
While ACL2's language is untyped Common Lisp, ACL2 provides a powerful type-
like mechanism called ``guards'' which can be used to assure that functions
are ``well-typed.'' Guards are arbitrary ACL2 formulas and guard checking is
undecidable (i.e., requires general purpose theorem proving in the hard
cases) but optional. When guards are verified, ACL2 functions can be
reliably executed by any compliant Common Lisp.
ACL2 is programmed in the same logic it supports. This has insured that the
logic is a practical means of building large formal systems. Interesting
metatheoretical explorations are also possible in this setting.
Weaknesses: While ACL2 feels like Nqthm its logic is not the same as Nqthm's
and so ACL2 does not inherit Nqthm's vast collection of proved results.
However, with the exception of those results depending on Nqthm's V&C$
construct, ACL2 could be led to those results with essentially the same
amount of work (!). A book which embeds a large fragment of the Nqthm logic
in ACL2 and makes ACL2 nearly mimic Nqthm is available but we do not
encourage its use in ``real'' modeling projects because ``native'' ACL2
results in better proofs and faster models.
Like Nqthm, ACL2 is best used to work on conjectures about recursive
functions over the integers and other finitely generated structures, e.g.,
conses. ACL2 does not support, especially well, attacks on theorems in set
theory or about such nonconstructive entities as the real numbers. (Its BDD
package gives it the capability, however, to do propositional reasoning, for
example about low-level hardware, with considerable efficiency.)
As with any contemporary general-purpose automated reasoning tool, successful
checking of interesting theorems with ACL2 requires a considerable amount of
mathematical talent, experience, and persistence. As with most uses of most
such tools, ACL2 should be regarded by the serious user as a proof checker
rather than a proof discoverer. That is, the user had better have in mind a
proof of any non-trivial theorem to be checked, and be prepared to guide ACL2
to checking that proof by giving hints, such as formulating lemmas.
Documentation:
See http://www.cs.utexas.edu/users/moore/acl2/acl2-doc.html#User's-Manual
for approximately 2 megabytes of hyper-linked online documentation.
The ACL2 documentation is distributed as part of the sources and includes
html, Emacs Info, and postcript formats.
The paper ``An Industrial Strength Theorem Prover for a Logic Based
on Common Lisp,'' by M. Kaufmann and J S. Moore, IEEE Transactions on
Software Engineering, 23(4), April, 1997, pp. 203-213, gives an
overview of the system.
The paper ``ACL2 Theorems about Commercial Microprocessors,'' by
B. Brock, M. Kaufmann and J S. Moore, in M. Srivas and A. Camilleri (eds.)
Proceedings of Formal Methods in Computer-Aided Design (FMCAD'96),
Springer-Verlag, pp. 275--293, 1996 gives an some details of two
industrial applications.
``A Mechanically Checked Proof of the Correctness of the Kernel of
the AMD5K86 Floating-Point Division Algorithm,'' by J S. Moore,
T. Lynch and M. Kaufmann, IEEE Trans. Comp., 47(9) September, 1998,
describes one application in detail.
Applications:
See the papers section of the ACL2 home page:
http://www.cs.utexas.edu/users/moore/acl2.
The most significant work with ACL2 to date (Summer, 1998) has been
David Russinoff's proofs of the correctness of the floating-point
hardware for the add, subtract, multiply, divide, and square root
functions of the AMD K7. See
http://www.onr.com/user/russ/david/k7-div-sqrt.html
Extensions/enhancements:
None at the moment.
Resource requirements: 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 (less however for MCL).
Where-to-get-it:
To obtain ACL2 via the World Wide Web, see the home page:
http://www.cs.utexas.edu/users/moore/acl2.
[Matt Kaufmann & J Strother Moore, Summer, 1998]
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%