Informatics Report Series



Related Pages

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

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

Home : Publications : Report 

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