Sept. 25, 2012
Ruben Gamboa

Title: ACL2(r) and the Completeness of the Reals

Abstract:

ACL2(r) is a variant of ACL2 that supports reasoning about the
irrational real and complex numbers.  Its logical foundations are
based on non-standard analysis, which has a style of reasoning that
fits well with ACL2's principles of rewriting and induction.  In this
talk, we will give an overview of ACL2(r), including the essential
principles of non-standard analysis that are needed to carry out most
proofs about the real and complex numbers in ACL2(r).  To illustrate
these principles, we will also present a proof of the Nested Interval
Theorem and the Least Upper Bound Property , two of several
characterizations of the completeness of the reals.