Division of Informatics
Forrest Hill & 80 South Bridge
Research Paper #559 | |
|---|---|
| Title: | Well-Founded Induction and Program Synthesis Using Proof Plans |
| Authors: | Phillips,C |
| Date: | 1991 |
| Presented: | To appear in the Proceedings of 2nd Workshop on Logical Frameworks, Edinburgh, 1991 |
| Keywords: | |
| Abstract: | The Mathematical Reasoning Group (MRG) in the Department of Artificial Intelligence at Edinburgh University has developed an approach to the verification and synthesis of programs using proof plans - high level descriptions of proofs, which control the automatic search for a proof. Constructive mathematics is employed, enabling programs to be derived using the proofs as programs technique. The proofs in question employ various forms of induction and techniques have been developed for automating the search for the form of induction appropriate to a given proof. In this paper I will discuss a modification of this methodology which involves using well-founded introduction and the automated search for the appropriate well-founded relation. This is being implemented in a version of Martin-Loef's type theory extended by Nordstroem's Acc Type. i shall be comparing this approach with that previously employed in the Mathematical Reasoning Group. |
| Download: | POSTSCRIPT 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}