- Abstract:
-
This paper presents work done on automating the construction of proofs in mathematical analysis. We present a proof of the Intermediate Value Theorem, using both induction and non-standard analysis within the framework of proof-planning.
We first give an overview of proof-planning and rippling, a heuristic guidance for rewriting. We explain in general terms some of the important concepts used in non-standard analysis, and the motivation behind our approach. The proofs themselves all use a combination of induction and non-standard analysis, which we show are techniques well suited to proof-planning.
The central idea of the work is to use proof-planning to automate the construction of plans for the proofs of the non-trivial theorems we present. The specific mathematical technique that we employ is one of infinite approximation.
- Copyright:
- 2003 by The University of Edinburgh. All Rights Reserved
- Links To Paper
- No links available
- Bibtex format
- @Misc{EDI-INF-RR-0175,
- author = {
Ewen Maclean
and Jacques Fleuriot
and Alan Smaill
},
- title = {Proof-planning Non-standard Analysis (ii)},
- year = 2002,
- month = {Mar},
- }
|
