|
eCommons@Cornell >
College of Engineering >
Computer Science >
Computer Science Technical Reports >
Please use this identifier to cite or link to this item:
http://hdl.handle.net/1813/6582
| Title: | Formalized Metareasoning in Type Theory |
| Authors: | Knoblock, Todd B.
Constable, Robert L. |
| Keywords: | computer science
technical report |
| Issue Date: | Mar-1986 |
| Publisher: | Cornell University |
| Citation: | http://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cs/TR86-742 |
| 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. |
| URI: | http://hdl.handle.net/1813/6582 |
| Appears in Collections: | Computer Science Technical Reports
|
Items in eCommons are protected by copyright, with all rights reserved, unless otherwise indicated.
|
