Modular Proof: The Fundamental Theorem of Calculus

  • Matt Kaufmann
Part of the Advances in Formal Methods book series (ADFM, volume 4)


This chapter presents a modular, top-down proof methodology for the effective use of ACL2. This methodology is intended both to ease the proof development process and to assist in proof presentation. An application is presented: a formalization and proof of the Fundamental Theorem of Calculus. An unusual characteristic of this application is the use of non-standard analysis, which however is not a prerequisite either for this chapter or for the utility of the proof methodology presented herein.


Fundamental Theorem Depth Limit Proof Obligation Main Lemma Outline Tool 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Copyright information

© Springer Science+Business Media New York 2000

Authors and Affiliations

  • Matt Kaufmann
    • 1
  1. 1.Advanced Micro Devices, Inc.AustinUSA

Personalised recommendations