Skip to main content


eCommons@Cornell

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: Oct-1994
Publisher: Cornell University
Citation: http://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cs/TR94-1460
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 co-inductive 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 depth-first-search 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 proof-theoretic 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

Files in This Item:

File Description SizeFormat
94-1460.pdf722.47 kBAdobe PDFView/Open
94-1460.ps607.79 kBPostscriptView/Open

Refworks Export

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

 

© 2014 Cornell University Library Contact Us