Non-Standard
Analysis in ACL2, Ruben A. Gamboa and Matt Kaufmann, Journal of Automated
Reasoning 27(4), 323-351, 2001.
This paper describes
ACL2(r), a version of ACL2 with support for the real and complex numbers. The
modifications are based on non-standard analysis, which interacts better with
the discrete flavor of ACL2 than does traditional analysis. See
below (discussion of a variant of ACL2 called “ACL2(r)”) or see real
for more about ACL2(r).
Modular Proof: The Fundamental Theorem of Calculus, Matt Kaufmann,
Chapter 6 of Computer-Aided Reasoning:
ACL2 Case Studies (Kaufmann, Manolios, Moore, eds.) Kluwer, 2000.
(ACL2 scripts are available from
directory 1999/calculus/ in the community-books.)
The article presents a modular top-down proof methodology and
uses it to formalize and prove the Fundamental Theorem of Calculus. The
modular strategy works for both ACL2 and “ACL2(r)” (see above); the
Fundamental Theorem is proved with ACL2(r). The ACL2 scripts referenced here
provide the full details of the results described in the article along with
solutions to all the exercises in the article.
Continuity and Differentiability, Ruben Gamboa, Chapter 18 of Computer-Aided Reasoning: ACL2 Case
Studies (Kaufmann, Manolios, Moore, eds.) Kluwer, 2000.
(ACL2 scripts are available from
directory 1999/analysis/ in the community-books.)
This article shows how an extended version of ACL2 (named
“ACL2(r)” and described below) can be used to reason about the real and
complex numbers, using non-standard analysis. It describes some
modifications to ACL2 that introduce the irrational real and complex numbers
into ACL2's number system. It then shows how the modified ACL2 can prove
classic theorems of analysis, such as the intermediate-value and mean-value
theorems. The ACL2(r) scripts referenced here provide the full details of
the results described in the article along with solutions to all the
exercises in the article.
ACL2 supports the rational numbers but not the reals. Starting with
Version 2.5, however, a variant of ACL2 called “ACL2(r)” supports the real
numbers by way of non-standard analysis. ACL2(r) was produced by Ruben
Gamboa from ACL2. ACL2(r) can be built from the ACL2 sources (Versions 2.5
and higher). See the makefile for instructions for building ACL2(r). For
further acknowledgements and some technical details see the documentation
topic real in the online documentation for ACL2. ACL2 authors
Kaufmann and Moore consider ACL2(r) Version 2.5 to be in “beta release.”
They have tried to ensure that when ACL2 is built from the integrated source
files, the result is a sound ACL2. They are confident that ACL2(r) will
eventually be sound and behave much as it does in the Version 2.5 release,
but have not yet checked every detail of the integration. For the
foundations of ACL2(r), see Gamboa's Ph.D. dissertation Mechanically Verifying
Real-Valued Algorithms in ACL2 (UT, May, 1999). The dissertation
includes ACL2(r)-checked proofs of many fundamental properties of the real
numbers, including such results as the continuity of e^x,
Euler's identity, the basic identities of trigonometry, the intermediate
value theorem, and others.
Square
Roots in ACL2: A Study in Sonata Form, Ruben Gamboa, UTCS Tech Report
TR96-34, November, 1996. This paper describes a proof in ACL2 that (*
x x) is never 2. This was the beginning of Gamboa's journey into
the ACL2 mechanization of non-standard analysis.
