## Department of Computer Sciences## 1999 ACL2 WorkshopMarch 29 - March 31, 1999 |

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.

Matt Kaufmann

Last updated March 1999 pete@cs.utexas.edu |
Computer Sciences
Department University of Texas at Austin |