Real Analysis with ACL2(r)
ACL2(r) is a variant of the theorem prover ACL2 with support for irrational real and complex numbers. ACL2 is an inductive theorem prover, with the syntax of the applicative subset of Common Lisp. The objects in ACL2 mirror the data structures in Common Lisp: numbers, strings, atoms, and cons pairs. As a result, ACL2 lacks sets or other infinite objects that could be used to introduce or reason about the real numbers, e.g., the Least Upper Bound theorem. To get around this fact, ACL2(r) uses non-standard analysis as a foundation to reason about the real and complex numbers. Non-standard analysis, pioneered by Robinson and later axiomatized by Nelson, is well-suited for this purpose, since many arguments in non-standard analysis use induction (a forte of ACL2) in place of the ε-δ arguments common in elementary analysis.
My most recent research in ACL2(r) has been joint work with John Cowles on the logical foundations of ACL2(r). These foundations are based on Nelson's Internal Set Theory, his axiomatization of non-standard analysis. Our recent work focuses on the interaction between Internal Set Theorem and the theory extension mechanisms in ACL2. This has allowed us to enhance ACL2(r) with some important features, such as the introduction of non-classical functions that use recursion or a weak version of choice. We are currently writing those enhancements, which will be released with the next version of ACL2.
ACL2(r) is included in the normal ACL2 distribution. To install it, follow the instructions posted there.