		Search-engine friendly clone of the ACL2 documentation.

About-ACL2

Soundness

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.

The built-in axioms describe properties of the ACL2 data types, such as the following.

ACL2 !>:pe car-cons
       -8139  (DEFAXIOM CAR-CONS
                (EQUAL (CAR (CONS X Y)) X))
ACL2 !>

A key extension principle is the Principle of Definition, which, for a definition (defun <fn> <args> <body>), introduces an axiom equating <body> with application of <fn> to <args>. This principle permits recursion, and even mutual-recursion, provided a suitable measure conjecture is provable.
Other events come with extension principles too, including encapsulate, defchoose, defpkg, and include-book. Note that from a logical perspective, defstobj and defabsstobj just provide definitional extensions.
Each ACL2 theory is closed under induction: that is, every instance of induction (in the language of the theory) below the ordinal epsilon-0 (see ordinals) is also in the theory. In practical terms, this is what allows ACL2 to prove theorems by induction.

For more about the ACL2 logic see the following publications by Matt Kaufmann and J Moore.

“A Precise Description of the ACL2 Logic” (April, 1998).
“Structured Theory Development for a Mechanized Logic”, Journal of Automated Reasoning 26, no. 2 (2001) 161-203.

The following soundness property is key for a given ACL2 session.

The theorem prover proves only formulas that are theorems in the corresponding prover's theory in that session.

Note that the theorem prover uses evaluation during proofs. The soundness property thus encompasses the following: when such evaluation of a term tm produces a value v, then (equal tm 'v) is provable from the context of that evaluation. Evaluation in the top-level loop has such a property as well, but because of attachments (see defattach) and apply$, provability is with respect to a larger “evaluation theory”; see guarantees-of-the-top-level-loop.

Here is a list of general restrictions on the soundness guarantee.

The prover's theory of a session includes all axioms introduced by hidden defpkg events. See hidden-death-package.
There is no soundness guarantee for a session in which there is raw Lisp evaluation with side effects. (ACL2 normally avoids putting the user into raw Lisp, but this can happen with an interrupt, the use of break$, or explicitly leaving the top-level loop with :q.) “Side effects” should be interpreted as generously as possible: this certainly includes redefining a function or assigning to a variable, but not merely evaluating an arithmetic expression, for example.
There is no soundness guarantee for a session in which any trust tag has been installed (see defttag). The absence of trust tags is guaranteed by the absence of “TTAG NOTE” being printed to standard output (that is, to *standard-co*).
Technically, the soundness guarantee only applies to the case that a set of books is certified from scratch, including community-books. In practice this is generally not necessary.

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).

Essay on Admitting a Model for Apply$ and the Functions that Use It
Essay on Hidden Packages
Essay on Soundness Threats
Essay on a Total Order of the ACL2 Universe
Essay on Illegal-states
Essay on Evaluation in ACL2
Essay on the Logical Basis for Linear Arithmetic
Essay on the Correctness of Abstract Stobjs
Essay on Memoization with Partial Functions (Memoize-partial)
Essay on Correctness of Evaluation with Stobjs
Essay on Correctness of Meta Reasoning

Subtopics

Guarantees-of-the-top-level-loop: Guarantees provided by top-level evaluation