Division of Informatics
Forrest Hill & 80 South Bridge
MSc Thesis #93105 | |
|---|---|
| Title: | Automating Proofs in Constructive Analysis |
| Authors: | Chippendale,M |
| Date: | 1993 |
| Presented: | |
| Keywords: | |
| Abstract: | The principal aims of this project were the development of object- and meta-level tools for the Edinburgh MRG's Oyster/CLAM system to support the theory of real analysis. The integers are a primitive type of Oyster. They were used as a basis to construct a theory of the rationals, and thence a theory of the reals and real analysis. This work at the object level was supported by new meta level-tools (methods in CLAM) to prove theorems such as the intermediate value theorem. Although reasoning about continuity and differentiability has traditionally been considered qualitatively different from reasoning about discrete algebraic structures, many of the approaches used by CLAM to prove theorems in discrete domains were found to be applicable to work in real analysis. In particular CLAM's use of induction and rippling/fertilisation was generalised using a new induction scheme which mimicked the classical proof of the intermediate value theorem using bisection of intervals. The scheme used is a form of well founded induction. |
| Download: | NO ONLINE COPY |
![[Search These Pages]](http://www.dai.ed.ac.uk/icons/dai_search.gif){kind=icon}
![[DAI Home Page]](http://www.dai.ed.ac.uk/icons/dai_home.gif){kind=icon}
![[Comment]](http://www.dai.ed.ac.uk/icons/dai_comment.gif){kind=icon}