You are cordially invited to join us for the
 
School of Mathematical Sciences
Colloquium
 
 
 
 
Wednesday, September 13, 2006
3:35 – 4:25 p.m.
Ross 2238 (Conference Room)
 
 
Speaker:
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.