Correctness property claimed for ACL2
What can we conclude when we use ACL2 to prove a formula or to compute the value of an expression? This topic provides a high-level sketch of an answer.
Any notion of correctness of ACL2 necessarily depends on the logic that it is intended to implement. At its core, the ACL2 logic is just classical first-order logic. The first-order theory for a given ACL2 session, which we may call the “prover's theory”, is the result of extending its set of built-in axioms according to events that have been executed in the session.
ACL2 !>:pe car-cons -8139 (DEFAXIOM CAR-CONS (EQUAL (CAR (CONS X Y)) X)) ACL2 !>
For more about the ACL2 logic see the following publications by Matt Kaufmann and J Moore.
The following soundness property is key for a given ACL2 session.
Note that the theorem prover uses evaluation during proofs. The soundness
property thus encompasses the following: when such evaluation of a term
Here is a list of general restrictions on the soundness guarantee.
Here are examples illustrating the last point above, regarding use of a single Lisp.
; True in SBCL 2.4.2, about the character it calls #MICRO_SIGN, ; but false in LispWorks 8.0.1: (alpha-char-p (code-char 181)) ; False in SBCL 2.4.2, about the character it calls #CENT_SIGN, ; but true in Allegro CL 10.1: (alpha-char-p (code-char 162))
Here is another example illustrating the requirement on a single Lisp. In ACL2 built on most host Lisp implementations, one can admit the following event. (See df for background on floating-point computations with ACL2.)
(defthm usual-sin-2pi (equal (df-sin (df* 2 *df-pi*)) #d-2.4492935982947064E-16))
But in ACL2 built on LispWorks, one can instead admit the following.
(defthm lispworks-sin-2pi (equal (df-sin (df* 2 *df-pi*)) #d-2.4492127076447545E-16))
Clearly one could prove
This topic has discussed the soundness guarantee from the user perspective. Those interested in exploring deeper theoretical and implementation issues are welcome to read the extensive relevant comments in the ACL2 source code, including the comments labeled as follows (listed in order of appearance as of this writing, not to indicate the order in which to read them).