Formalized Metareasoning in Type Theory

dc.contributor.authorKnoblock, Todd B.en_US
dc.contributor.authorConstable, Robert L.en_US
dc.date.accessioned2007-04-23T17:13:37Z
dc.date.available2007-04-23T17:13:37Z
dc.date.issued1986-03en_US
dc.description.abstractIn 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.en_US
dc.format.extent1635637 bytes
dc.format.extent530076 bytes
dc.format.mimetypeapplication/pdf
dc.format.mimetypeapplication/postscript
dc.identifier.citationhttp://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cs/TR86-742en_US
dc.identifier.urihttps://hdl.handle.net/1813/6582
dc.language.isoen_USen_US
dc.publisherCornell Universityen_US
dc.subjectcomputer scienceen_US
dc.subjecttechnical reporten_US
dc.titleFormalized Metareasoning in Type Theoryen_US
dc.typetechnical reporten_US
Files
Original bundle
Now showing 1 - 2 of 2
Loading...
Thumbnail Image
Name:
86-742.pdf
Size:
1.56 MB
Format:
Adobe Portable Document Format
No Thumbnail Available
Name:
86-742.ps
Size:
517.65 KB
Format:
Postscript Files