The University of Edinburgh -
Division of Informatics
Forrest Hill & 80 South Bridge

Research Paper #564

Title:On Exploiting the Structure of Martin-Loef'S Theory of Types
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
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.

[Search These Pages] [DAI Home Page] [Comment]