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/6069
Title:  Aspects of the Computational Content of Proofs 
Authors:  Underwood, Judith 
Keywords:  computer science technical report 
Issue Date:  Oct1994 
Publisher:  Cornell University 
Citation:  http://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cs/TR941460 
Abstract:  In this thesis, we explore three aspects of the computational content of proofs. These are: a computational interpretation of the metatheory of intuitionistic propositional logic, an extension of this approach to intuitionistic predicate logic, and a computational interpretation of classical sequent proofs. We begin with a study of the computational aspects of validity, provability, and completeness for intuitionistic propositional logic. We give a constructive proof of completeness of Kripke models for intuitionistic propositional calculus, such that the computational content of the proof is a form of the tableau algorithm. Since the evidence for provability we construct is actually a term in typed $\lambda$calculus, we can interpret this result as a formal relationship between Kripke semantics and realizability semantics. We also show how a formal proof of the completeness theorem in Nuprl could be used to add the tableau decision procedure for provability to Nuprl's collection of proof techniques via reflection. We then explore how these results could be generalized to the metatheory of intuitionistic predicate logic. To do this, we develop some machinery for representing infinite Kripke models in type theory using coinductive types. Although provability in intuitionistic predicate logic is undecidable, we can still prove a constructive theorem in the metatheory which has computational content. We also show that using classical logic in part of the proof does not destroy the computational content of the proof. Finally, we examine the computational aspects of classical sequent proofs. We show how the interpretation of nonlocal control operators as the computational content of classical axioms allows us to prove a completeness result for intuitionistic predicate logic with a depthfirstsearch tableau procedure as the computational content of the proof. Using the nonlocal control operator \cc\ as the the computational interpretation of the classical axiom we define a method for extracting programs from classical sequent proofs in propositional logic. We give a prooftheoretic account of continuations and their behaviour in this context, and prove a number of properties of the extraction. 
URI:  http://hdl.handle.net/1813/6069 
Appears in Collections:  Computer Science Technical Reports

Items in eCommons are protected by copyright, with all rights reserved, unless otherwise indicated.
