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.
| Identifer | oai:union.ndltd.org:bl.uk/oai:ethos.bl.uk:561878 |
| Date | January 2004 |
| Creators | Maclean, Ewen |
| Contributors | Fleuriot, Jacques. ; Smaill, Alan |
| Publisher | University of Edinburgh |
| Source Sets | Ethos UK |
| Detected Language | English |
| Type | Electronic Thesis or Dissertation |
| Source | http://hdl.handle.net/1842/2250 |
Page generated in 0.0024 seconds