Lics

ACM/IEEE Symposium on Logic in Computer Science

LICS Home - LICS Awards - LICS Newsletters - LICS Archive - LICS Organization - Logic-Related Conferences - Links

First Annual IEEE Symposium on

Logic in Computer Science (LICS 1986)

Paper: Formalized Metareasoning in Type Theory (at LICS 1986)

Authors: Todd B. Knoblock Robert L. Constable

Abstract

In this paper we present two practical methods of formalizing the metatheory of constructive type theory and demonstrate how they would be used to improve the reasoning capabilities of formal problem solving systems such as Nuprl. One method depends upon the design of a family of languages, and we sketch that construction. The second approach depends on a particular metatheorem that justifies partial reflection, and we outline this proof. We also illustrate the construction of simple metatheoretic functions, tactics, in Nuprl.

BibTeX

  @InProceedings{KnoblockConstable-FormalizedMetareaso,
    author = 	 {Todd B. Knoblock and Robert L. Constable},
    title = 	 {Formalized Metareasoning in Type Theory},
    booktitle =  {Proceedings of the First Annual IEEE Symposium on Logic in Computer Science (LICS 1986)},
    year =	 {1986},
    month =	 {June}, 
    pages =      {237--248},
    location =   {Cambridge, MA, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }
   

Last modified: 2022-10-3113:49
Sam Staton