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.