Geodesic
Proof Mining: A~Systematic Way of Analyzing Proofs in Mathematics
Trudy Matematicheskogo Instituta imeni V.A. Steklova, Mathematical logic and algebra, Tome 242 (2003), pp. 147-175

Voir la notice de l'article provenant de la source Math-Net.Ru

Proof mining is the process of logically analyzing proofs in mathematics with the aim of obtaining new information. In this survey paper, we discuss, by means of examples from mathematics, some of the main techniques used in proof mining. We show that these techniques apply not only to proofs based on classical logic but also to proofs that involve noneffective principles such as the attainment of the infimum of $f\in C[0,1]$ and the convergence for bounded monotone sequences of reals. We also report on recent case studies in approximation theory and fixed point theory where new results were obtained. 
@article{TM_2003_242_a12,
     author = {U. Kohlenbach and P. Oliva},
     title = {Proof {Mining:} {A~Systematic} {Way} of {Analyzing} {Proofs} in {Mathematics}},
     journal = {Trudy Matematicheskogo Instituta imeni V.A. Steklova},
     pages = {147--175},
     publisher = {mathdoc},
     volume = {242},
     year = {2003},
     language = {en},
     url = {http://geodesic.mathdoc.fr/item/TM_2003_242_a12/}
}
TY  - JOUR
AU  - U. Kohlenbach
AU  - P. Oliva
TI  - Proof Mining: A~Systematic Way of Analyzing Proofs in Mathematics
JO  - Trudy Matematicheskogo Instituta imeni V.A. Steklova
PY  - 2003
SP  - 147
EP  - 175
VL  - 242
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/TM_2003_242_a12/
LA  - en
ID  - TM_2003_242_a12
ER  - 
%0 Journal Article
%A U. Kohlenbach
%A P. Oliva
%T Proof Mining: A~Systematic Way of Analyzing Proofs in Mathematics
%J Trudy Matematicheskogo Instituta imeni V.A. Steklova
%D 2003
%P 147-175
%V 242
%I mathdoc
%U http://geodesic.mathdoc.fr/item/TM_2003_242_a12/
%G en
%F TM_2003_242_a12
U. Kohlenbach; P. Oliva. Proof Mining: A~Systematic Way of Analyzing Proofs in Mathematics. Trudy Matematicheskogo Instituta imeni V.A. Steklova, Mathematical logic and algebra, Tome 242 (2003), pp. 147-175. http://geodesic.mathdoc.fr/item/TM_2003_242_a12/