Modular Proof: The Fundamental Theorem of Calculus
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.
KeywordsFundamental Theorem Depth Limit Proof Obligation Main Lemma Outline Tool
Unable to display preview. Download preview PDF.