Division of Informatics
Forrest Hill & 80 South Bridge
Research Paper #564 | |
|---|---|
| Title: | On Exploiting the Structure of Martin-Loef'S Theory of Types |
| Authors: | Ireland,A |
| Date: | 1991 |
| Presented: | In Proceedings of 7th Austrial Conference on Artificial Intelligence, Tagung, 91. (Ed. Hermann Kaindl) pp. 126-136. Springer-Verlag, Informatik-Fachberichte, 28 |
| Keywords: | |
| Abstract: | Program synthesis in Martin-Loef's Theory of Types is a theorem proving activity. We demonstrate how the rich structure of the theory may be exploited in the automation of this activity. Basic properties of data type constructors are shown to exhibit a general structure in the way in which they are expressed and derived. A proof procedure for negation is developed based upon these properties. As a consequence our proof procedure may be extended uniformly to incorporate new data types. |
| 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}