Informatics Report Series


Report   

EDI-INF-RR-0175


Related Pages

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

Home
Title:Proof-planning Non-standard Analysis (ii)
Authors: Ewen Maclean ; Jacques Fleuriot ; Alan Smaill
Date:Mar 2002
Publication Title:Annals of AI+MATH 2002
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},
}


Home : Publications : Report 

Please mail <reports@inf.ed.ac.uk> with any changes or corrections.
Unless explicitly stated otherwise, all material is copyright The University of Edinburgh