Geodesic
Proof Mining: A~Systematic Way of Analyzing Proofs in Mathematics
Informatics and Automation, 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{TRSPY_2003_242_a12,
     author = {U. Kohlenbach and P. Oliva},
     title = {Proof {Mining:} {A~Systematic} {Way} of {Analyzing} {Proofs} in {Mathematics}},
     journal = {Informatics and Automation},
     pages = {147--175},
     publisher = {mathdoc},
     volume = {242},
     year = {2003},
     language = {en},
     url = {http://geodesic.mathdoc.fr/item/TRSPY_2003_242_a12/}
}
TY  - JOUR
AU  - U. Kohlenbach
AU  - P. Oliva
TI  - Proof Mining: A~Systematic Way of Analyzing Proofs in Mathematics
JO  - Informatics and Automation
PY  - 2003
SP  - 147
EP  - 175
VL  - 242
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/TRSPY_2003_242_a12/
LA  - en
ID  - TRSPY_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 Informatics and Automation
%D 2003
%P 147-175
%V 242
%I mathdoc
%U http://geodesic.mathdoc.fr/item/TRSPY_2003_242_a12/
%G en
%F TRSPY_2003_242_a12
U. Kohlenbach; P. Oliva. Proof Mining: A~Systematic Way of Analyzing Proofs in Mathematics. Informatics and Automation, Mathematical logic and algebra, Tome 242 (2003), pp. 147-175. http://geodesic.mathdoc.fr/item/TRSPY_2003_242_a12/