Refined program extraction from classical proofs

Annals of Pure and Applied Logic 114 (1-3):3-25 (2002)
  Copy   BIBTEX

Abstract

The paper presents a refined method of extracting reasonable and sometimes unexpected programs from classical proofs of formulas of the form ∀x∃yB . We also generalize previously known results, since B no longer needs to be quantifier-free, but only has to belong to a strictly larger class of so-called “goal formulas”. Furthermore we allow unproven lemmas D in the proof of ∀x∃yB , where D is a so-called “definite” formula

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 90,616

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

Similar books and articles

Program extraction for 2-random reals.Alexander P. Kreuzer - 2013 - Archive for Mathematical Logic 52 (5-6):659-666.
Light monotone Dialectica methods for proof mining.Mircea-Dan Hernest - 2009 - Mathematical Logic Quarterly 55 (5):551-561.
Dialectica interpretation of well-founded induction.Helmut Schwichtenberg - 2008 - Mathematical Logic Quarterly 54 (3):229-239.
Minimal from classical proofs.Helmut Schwichtenberg & Christoph Senjak - 2013 - Annals of Pure and Applied Logic 164 (6):740-748.
The three dimensions of proofs.Yves Guiraud - 2006 - Annals of Pure and Applied Logic 141 (1):266-295.
Electronic Media Review.Michael B. Burke - 2006 - Teaching Philosophy 29 (3):255-260.
System ST toward a type system for extraction and proofs of programs.Christophe Raffalli - 2003 - Annals of Pure and Applied Logic 122 (1-3):107-130.

Analytics

Added to PP
2014-01-16

Downloads
17 (#742,076)

6 months
1 (#1,040,386)

Historical graph of downloads
How can I increase my downloads?

Author's Profile

Citations of this work

Minimal from classical proofs.Helmut Schwichtenberg & Christoph Senjak - 2013 - Annals of Pure and Applied Logic 164 (6):740-748.
Uniform heyting arithmetic.Ulrich Berger - 2005 - Annals of Pure and Applied Logic 133 (1):125-148.
Programs from proofs using classical dependent choice.Monika Seisenberger - 2008 - Annals of Pure and Applied Logic 153 (1-3):97-110.
Dialectica interpretation of well-founded induction.Helmut Schwichtenberg - 2008 - Mathematical Logic Quarterly 54 (3):229-239.

View all 9 citations / Add more citations

References found in this work

Syntactic translations and provably recursive functions.Daniel Leivant - 1985 - Journal of Symbolic Logic 50 (3):682-688.

Add more references