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

Authors
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
Keywords No keywords specified (fix it)
Categories (categorize this paper)
DOI 10.1016/s0168-0072(01)00073-2
Options
Edit this record
Mark as duplicate
Export citation
Find it on Scholar
Request removal from index
Revision history

Download options

PhilArchive copy


Upload a copy of this paper     Check publisher's policy     Papers currently archived: 51,707
Through your library

References found in this work BETA

Syntactic Translations and Provably Recursive Functions.Daniel Leivant - 1985 - Journal of Symbolic Logic 50 (3):682-688.

Add more references

Citations of this work BETA

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.
Dialectica Interpretation of Well-Founded Induction.Helmut Schwichtenberg - 2008 - Mathematical Logic Quarterly 54 (3):229-239.
Programs From Proofs Using Classical Dependent Choice.Monika Seisenberger - 2008 - Annals of Pure and Applied Logic 153 (1-3):97-110.

View all 9 citations / Add more citations

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 index
2014-01-16

Total views
11 ( #760,717 of 2,333,192 )

Recent downloads (6 months)
1 ( #587,885 of 2,333,192 )

How can I increase my downloads?

Downloads

My notes