Department of Computer Sciences 1999 ACL2 Workshop March 29 - March 31, 1999

The Application of a Modular Proof Methodology for ACL2 to Proving the Fundamental Theorem of Calculus

I will describe a simple methodology for developing proofs in a modular style using ACL2. I will illustrate the methodology by describing some highlights of a proof I carried out of the Fundamental Theorem of Calculus, using a modification of ACL2 developed by Ruben Gamboa that supports the real numbers using non-standard analysis. But the main emphasis of the talk will be on the simple proof methodology and a tool that supports it.

Slides (use "Swap Landscape" when in ghostview)

• One slide per page
• Four slides per page

Matt Kaufmann