Now showing items 1-3 of 3

    • Formalized Metareasoning in Type Theory 

      Knoblock, Todd B.; Constable, Robert L. (Cornell University, 1986-03)
      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 ...
    • Metamathematical Extensibility in Type Theory 

      Knoblock, Todd B. (Cornell University, 1987-12)
      An automated theorem prover is said to be metamathematically extensible if a metalanguage can be employed by the user to soundly extend the reasoning capabilities of the system. In this thesis, we present a framework for ...
    • Writing Programs that Construct Proofs 

      Constable, Robert L.; Knoblock, Todd B.; Bates, Joseph L. (Cornell University, 1984-10)
      When we learn mathematics, we learn more than definitions and theorems. We learn techniques of proof. In this paper, we describe a particular way to express these techniques and incorporate them into formal theories and ...