Edinburgh Research Archive >
Informatics, School of >
Informatics thesis and dissertation collection >
Please use this identifier to cite or link to this item:
|Title: ||Using Proof-Planning to Investigate the Structure of Proof in Non-Standard Analysis|
|Authors: ||Maclean, Ewen|
|Supervisor(s): ||Fleuriot, Jacques|
|Issue Date: ||2004|
|Abstract: ||This thesis presents an investigation into the structure of proof in non-standard analysis using
proof-planning. The theory of non-standard analysis, developed by Robinson in the 1960s,
offers a more algebraic way of looking at proof in analysis. Proof-planning is a technique for
reasoning about proof at the meta-level. In this thesis, we use it to encapsulate the patterns of
reasoning that occur in non-standard analysis proofs.
We first introduce in detail the mathematical theory and the proof-planning architecture.
We then present our research methodology, describe the formal framework, which includes an
axiomatisation, and develop suitable evaluation criteria. We then present our development of
proof-plans for theorems involving limits, continuity and differentiation. We then explain how
proof-planning applies to theorems which combine induction and non-standard analysis.
Finally we give a detailed evaluation of the results obtained by combining the two attractive
approaches of proof-planning and non-standard analysis, and draw conclusions from the work.|
|Description: ||Centre for Intelligent Systems and their Applications|
award number 99303126
|Sponsor(s): ||Engineering and Physical Sciences Research Council (EPSRC)|
|Appears in Collections:||Informatics thesis and dissertation collection|
Items in ERA are protected by copyright, with all rights reserved, unless otherwise indicated.