Informatics Report Series



Related Pages

Report (by Number) Index
Report (by Date) Index
Author Index
Institute Index

Title:Proof-planning Non-standard Analysis
Authors: Ewen Maclean ; Jacques Fleuriot ; Alan Smaill
Date:Jan 2002
Publication Title:Procs of AIMATH 2002
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.
2003 by The University of Edinburgh. All Rights Reserved
Links To Paper
No links available
Bibtex format
author = { Ewen Maclean and Jacques Fleuriot and Alan Smaill },
title = {Proof-planning Non-standard Analysis},
year = 2002,
month = {Jan},

Home : Publications : Report 

Please mail <> with any changes or corrections.
Unless explicitly stated otherwise, all material is copyright The University of Edinburgh