@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@ 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] %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%