You are cordially invited to join us for the
School of Mathematical Sciences
Wednesday, September 13, 2006
3:35 – 4:25 p.m.
Ross 2238 (Conference Room)
Ruben Gamboa, University of Wyoming
Mechanical Verification of Elementary Calculus Theorems in ACL2(r)
ACL2 is both a first-order logic with equality and induction and a theorem prover over this logic.  In this talk we describe ACL2(r), a modified version of ACL2 with support for reasoning about the real and complex numbers.  ACL2(r) is based on non-standard analysis, which uses induction instead of the more familiar epsilon-delta arguments used in traditional analysis.  In this talk we will give a brief introduction to theorem proving with ACL2 and non-standard analysis, and we will illustrate these ideas with a mechanical proof in ACL2(r) of the Intermediate Value Theorem.