Trudy Matematicheskogo Instituta imeni V.A. Steklova
General information
Latest issue
Forthcoming papers
Impact factor
Guidelines for authors
License agreement

Search papers
Search references

Latest issue
Current issues
Archive issues
What is RSS

Trudy Mat. Inst. Steklova:

Personal entry:
Save password
Forgotten password?

Trudy Mat. Inst. Steklova, 2003, Volume 242, Pages 147–175 (Mi tm413)  

This article is cited in 37 scientific papers (total in 37 papers)

Proof Mining: A Systematic Way of Analyzing Proofs in Mathematics

U. Kohlenbach, P. Oliva

University of Aarhus

Abstract: 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.

Full text: PDF file (367 kB)
References: PDF file   HTML file

English version:
Proceedings of the Steklov Institute of Mathematics, 2003, 242, 136–164

Bibliographic databases:
UDC: 510.6
Received in June 2002

Citation: U. Kohlenbach, P. Oliva, “Proof Mining: A Systematic Way of Analyzing Proofs in Mathematics”, Mathematical logic and algebra, Collected papers. Dedicated to the 100th birthday of academician Petr Sergeevich Novikov, Trudy Mat. Inst. Steklova, 242, Nauka, MAIK Nauka/Inteperiodika, M., 2003, 147–175; Proc. Steklov Inst. Math., 242 (2003), 136–164

Citation in format AMSBIB
\by U.~Kohlenbach, P.~Oliva
\paper Proof Mining: A~Systematic Way of Analyzing Proofs in Mathematics
\inbook Mathematical logic and algebra
\bookinfo Collected papers. Dedicated to the 100th birthday of academician Petr Sergeevich Novikov
\serial Trudy Mat. Inst. Steklova
\yr 2003
\vol 242
\pages 147--175
\publ Nauka, MAIK Nauka/Inteperiodika
\publaddr M.
\jour Proc. Steklov Inst. Math.
\yr 2003
\vol 242
\pages 136--164

Linking options:

    SHARE: FaceBook Twitter Livejournal

    Citing articles on Google Scholar: Russian citations, English citations
    Related articles on Google Scholar: Russian articles, English articles

    This publication is cited in the following articles:
    1. Kohlenbach U., “Some logical metatheorems with applications in functional analysis”, Trans. Amer. Math. Soc., 357:1 (2005), 89–128  crossref  mathscinet  zmath  isi  scopus
    2. Macintyre A., “The mathematical significance of proof theory”, Philos. Trans. R. Soc. Lond. Ser. A Math. Phys. Eng. Sci., 363:1835 (2005), 2419–2435  crossref  mathscinet  zmath  adsnasa  isi  scopus
    3. Hernest M.D., “Light functional interpretation: an optimization of Gödel's technique towards the extraction of (more) efficient programs from (classical) proofs”, Computer science logic, Lecture Notes in Comput. Sci., 3634, Springer, Berlin, 2005, 477–492  crossref  mathscinet  zmath  isi
    4. Ferreira F., Oliva P., “Bounded functional interpretation”, Ann. Pure Appl. Logic, 135:1-3 (2005), 73–112  crossref  mathscinet  zmath  isi  scopus
    5. Kohlenbach U., “Proof mining in functional analysis”, New computational paradigms, First conference on computability in Europe, CiE 2005 (Amsterdam, The Netherlands, June 8–12, 2005), Proceedings, Lecture Notes in Comput. Sci., 3526, Springer, Berlin, 2005, 233–234  crossref  zmath  isi
    6. Hayashi S., “Can proofs be animated by games?”, Typed lambda calculi and applications, Lecture Notes in Comput. Sci., 3461, Springer, Berlin, 2005, 11–22  crossref  mathscinet  zmath  isi
    7. Hernest M.-D., Kohlenbach U., “A complexity analysis of functional interpretations”, Theoret. Comput. Sci., 338:1-3 (2005), 200–246  crossref  mathscinet  zmath  isi  scopus
    8. Schuster P., “Unique solutions”, MLQ Math. Log. Q., 52:6 (2006), 534–539  crossref  mathscinet  zmath  isi  scopus
    9. Gerhardy Ph., Kohlenbach U., “Strongly uniform bounds from semi-constructive proofs”, Ann. Pure Appl. Logic, 141:1-2 (2006), 89–107  crossref  mathscinet  zmath  isi  scopus
    10. Ferreira F., Nunes A., “Bounded modified realizability”, J. Symbolic Logic, 71:1 (2006), 329–346  crossref  mathscinet  zmath  isi  scopus
    11. Gerhardy Ph., “A quantitative version of Kirk's fixed point theorem for asymptotic contractions”, J. Math. Anal. Appl., 316:1 (2006), 339–345  crossref  mathscinet  zmath  adsnasa  isi  scopus
    12. Briseid E.M., “Some results on Kirk's asymptotic contractions”, Fixed Point Theory, 8:1 (2007), 17–27  mathscinet  zmath  isi
    13. Hayashi S., “Can proofs be animated by games?”, Fund. Inform., 77:4 (2007), 331–343  mathscinet  zmath  isi
    14. Briseid E.M., “A rate of convergence for asymptotic contractions”, J. Math. Anal. Appl., 330:1 (2007), 364–376  crossref  mathscinet  zmath  adsnasa  isi  scopus
    15. Schuster P., “Corrigendum to: “Unique solutions” [MLQ Math. Log. Q. 52 (2006), no. 6, 534–539]”, MLQ Math. Log. Q., 53:2 (2007), 214  crossref  mathscinet  zmath  adsnasa  isi  scopus
    16. Ishihara H., “Unique existence and computability in constructive reverse mathematics”, Computation and Logic in the Real World, Proceedings, Lecture Notes in Computer Science, 4497, 2007, 368–377  crossref  mathscinet  zmath  isi  scopus
    17. Schuster P., “Problems as solutions”, Computation and Logic in the Real World, Proceedings, Lecture Notes in Computer Science, 4497, 2007, 676–684  crossref  mathscinet  zmath  isi  scopus
    18. Briseid E.M., “Fixed points of generalized contractive mappings”, J. Nonlinear Convex Anal., 9:2 (2008), 181–204  mathscinet  zmath  isi
    19. Seisenberger M., “Programs from proofs using classical dependent choice”, Ann. Pure Appl. Logic, 153:1-3 (2008), 97–110  crossref  mathscinet  zmath  isi  scopus
    20. Gerhardy Ph., Kohlenbach U., “General logical metatheorems for functional analysis”, Trans. Amer. Math. Soc., 360:5 (2008), 2615–2660  crossref  mathscinet  zmath  isi  scopus
    21. Cantini A., “On formal proofs”, Deduction, Computation, Experiment: Exploring the Effectiveness of Proof, 2008, 29–48  crossref  mathscinet  zmath  isi
    22. Ferreira F., “A most artistic package of a jumble of ideas (Kurt Gödel)”, Dialectica, 62:2 (2008), 205–222  crossref  mathscinet  zmath  isi  scopus
    23. Kohlenbach U., “Gödel's functional interpretation and its use in current mathematics (Reprinted from 'Horizons of Truth - Logics, Foundations of Mathematics, and the Quest for Understanding the Nature of Knowledge', 2008)”, Dialectica, 62:2 (2008), 223–267  crossref  mathscinet  isi  elib  scopus
    24. Oliva P., “An analysis of Gödel's 'Dialectica' interpretation via linear logic”, Dialectica, 62:2 (2008), 269–290  crossref  mathscinet  isi  scopus
    25. Hernest M.-D., Oliva P., “Hybrid functional interpretations”, Logic and Theory of Algorithms, Lecture Notes in Computer Science, 5028, 2008, 251–260  crossref  mathscinet  zmath  isi  scopus
    26. Briseid E.M., “Logical aspects of rates of convergence in metric spaces”, J. Symbolic Logic, 74:4 (2009), 1401–1428  crossref  mathscinet  zmath  isi  scopus
    27. Hernest M.-D., “Light monotone Dialectica methods for proof mining”, MLQ Math. Log. Q., 55:5 (2009), 551–561  crossref  mathscinet  zmath  isi  scopus
    28. Schuster P., “Problems, solutions, and completions”, J. Log. Algebr. Program., 79:1 (2010), 84–91  crossref  mathscinet  zmath  isi  scopus
    29. Avigad J., Towsner H., “Metastability in the Furstenberg-Zimmer tower”, Fund Math, 210:3 (2010), 243–268  crossref  mathscinet  zmath  isi  scopus
    30. Safarik P., Kohlenbach U., “On the computational content of the Bolzano-WeierstraB Principle”, MLQ Math Log Q, 56:5 (2010), 508–532  crossref  mathscinet  zmath  isi
    31. Singh Sh.L., Mishra S.N., Pant R., “Fixed Points of Generalized Asymptotic Contractions”, Fixed Point Theory, 12:2 (2011), 475–484  mathscinet  zmath  isi
    32. Oliva P., “Hybrid Functional Interpretations of Linear and Intuitionistic Logic”, J. Logic Comput., 22:2, SI (2012), 305–328  crossref  mathscinet  zmath  isi  scopus
    33. Hadzihasanovic A., van den Berg B., “Nonstandard Functional Interpretations and Categorical Models”, Notre Dame J. Form. Log., 58:3 (2017), 343–380  crossref  mathscinet  zmath  isi  scopus
    34. Rinaldi D., Schuster P., Wessel D., “Eliminating Disjunctions By Disjunction Elimination”, Indag. Math.-New Ser., 29:1, SI (2018), 226–259  crossref  mathscinet  zmath  isi  scopus
    35. Leustean L., Nicolae A., Sipos A., “An Abstract Proximal Point Algorithm”, J. Glob. Optim., 72:3 (2018), 553–577  crossref  mathscinet  isi  scopus
    36. Miller D., “Mechanized Metatheory Revisited”, J. Autom. Reasoning, 63:3 (2019), 625–665  crossref  mathscinet  isi
    37. Dinis B., Pinto P., “Metastability of the Proximal Point Algorithm With Multi-Parameters”, Port Math., 77:3-4 (2020), 345–381  crossref  mathscinet  isi
  •    . . .  Proceedings of the Steklov Institute of Mathematics
    Number of views:
    This page:593
    Full text:193

    Contact us:
     Terms of Use  Registration to the website  Logotypes © Steklov Mathematical Institute RAS, 2021