Informatics Report Series
Report
 EDI-INF-RR-0178
 Related Pages Report (by Number) Index Report (by Date) Index Author Index Institute Index Home
Title:Automating Proof in Non-standard Analysis
Authors: Ewen Maclean
Date:Aug 2001
Publication Title:ESSLLI 2001 student session
Abstract:
Non-standard analysis provides a framework to carry out formally calculus proofs in a much more intuitive manner than in the $\epsilon-\delta$ formulation of Weierstra{\ss}. This paper introduces the notions of proof-planning and rippling, and gives an example showing how they can be applied to non-standard analysis to produce readable proofs. We present the related work in the area and give an outline of the proposed work.