- Abstract:
-
We describe how non-standard analysis can be used to prove real analysis theorems, and how these proofs can be automated using proof-planning. In particular we borrow from the constructive analysis notions of inductive partitioning, and show how transferring to the non-standard model for the reals allows us a simple proof of the correctness of partitioning algorithms for certain real analysis theorems.
- Copyright:
- 2003 by The University of Edinburgh. All Rights Reserved
- Links To Paper
- No links available
- Bibtex format
- @Misc{EDI-INF-RR-0173,
- author = {
Ewen Maclean
and Jacques Fleuriot
and Alan Smaill
},
- title = {Proof-planning Non-standard Analysis},
- year = 2002,
- month = {Jan},
- }
|
