Trudy Matematicheskogo Instituta imeni V.A. Steklova
 RUS  ENG JOURNALS   PEOPLE   ORGANISATIONS   CONFERENCES   SEMINARS   VIDEO LIBRARY   PACKAGE AMSBIB
 General information Latest issue Forthcoming papers Archive Impact factor Guidelines for authors License agreement Search papers Search references RSS Latest issue Current issues Archive issues What is RSS

 Trudy Mat. Inst. Steklova: Year: Volume: Issue: Page: Find

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

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
Language:

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
\Bibitem{KohOli03}
\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»
\mathnet{http://mi.mathnet.ru/tm413}
\mathscinet{http://www.ams.org/mathscinet-getitem?mr=2054493}
\zmath{https://zbmath.org/?q=an:1079.03045}
\transl
\jour Proc. Steklov Inst. Math.
\yr 2003
\vol 242
\pages 136--164

• http://mi.mathnet.ru/eng/tm413
• http://mi.mathnet.ru/eng/tm/v242/p147

 SHARE:

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
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
3. Hernest M.D., “Light functional interpretation: an optimization of Gö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
4. Ferreira F., Oliva P., “Bounded functional interpretation”, Ann. Pure Appl. Logic, 135:1-3 (2005), 73–112
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
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
7. Hernest M.-D., Kohlenbach U., “A complexity analysis of functional interpretations”, Theoret. Comput. Sci., 338:1-3 (2005), 200–246
8. Schuster P., “Unique solutions”, MLQ Math. Log. Q., 52:6 (2006), 534–539
9. Gerhardy Ph., Kohlenbach U., “Strongly uniform bounds from semi-constructive proofs”, Ann. Pure Appl. Logic, 141:1-2 (2006), 89–107
10. Ferreira F., Nunes A., “Bounded modified realizability”, J. Symbolic Logic, 71:1 (2006), 329–346
11. Gerhardy Ph., “A quantitative version of Kirk's fixed point theorem for asymptotic contractions”, J. Math. Anal. Appl., 316:1 (2006), 339–345
12. Briseid E.M., “Some results on Kirk's asymptotic contractions”, Fixed Point Theory, 8:1 (2007), 17–27
13. Hayashi S., “Can proofs be animated by games?”, Fund. Inform., 77:4 (2007), 331–343
14. Briseid E.M., “A rate of convergence for asymptotic contractions”, J. Math. Anal. Appl., 330:1 (2007), 364–376
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
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
17. Schuster P., “Problems as solutions”, Computation and Logic in the Real World, Proceedings, Lecture Notes in Computer Science, 4497, 2007, 676–684
18. Briseid E.M., “Fixed points of generalized contractive mappings”, J. Nonlinear Convex Anal., 9:2 (2008), 181–204
19. Seisenberger M., “Programs from proofs using classical dependent choice”, Ann. Pure Appl. Logic, 153:1-3 (2008), 97–110
20. Gerhardy Ph., Kohlenbach U., “General logical metatheorems for functional analysis”, Trans. Amer. Math. Soc., 360:5 (2008), 2615–2660
21. Cantini A., “On formal proofs”, Deduction, Computation, Experiment: Exploring the Effectiveness of Proof, 2008, 29–48
22. Ferreira F., “A most artistic package of a jumble of ideas (Kurt Gödel)”, Dialectica, 62:2 (2008), 205–222
23. Kohlenbach U., “Gö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
24. Oliva P., “An analysis of Gödel's 'Dialectica' interpretation via linear logic”, Dialectica, 62:2 (2008), 269–290
25. Hernest M.-D., Oliva P., “Hybrid functional interpretations”, Logic and Theory of Algorithms, Lecture Notes in Computer Science, 5028, 2008, 251–260
26. Briseid E.M., “Logical aspects of rates of convergence in metric spaces”, J. Symbolic Logic, 74:4 (2009), 1401–1428
27. Hernest M.-D., “Light monotone Dialectica methods for proof mining”, MLQ Math. Log. Q., 55:5 (2009), 551–561
28. Schuster P., “Problems, solutions, and completions”, J. Log. Algebr. Program., 79:1 (2010), 84–91
29. Avigad J., Towsner H., “Metastability in the Furstenberg-Zimmer tower”, Fund Math, 210:3 (2010), 243–268
30. Safarik P., Kohlenbach U., “On the computational content of the Bolzano-WeierstraB Principle”, MLQ Math Log Q, 56:5 (2010), 508–532
31. Singh Sh.L., Mishra S.N., Pant R., “Fixed Points of Generalized Asymptotic Contractions”, Fixed Point Theory, 12:2 (2011), 475–484
32. Oliva P., “Hybrid Functional Interpretations of Linear and Intuitionistic Logic”, J. Logic Comput., 22:2, SI (2012), 305–328
33. Hadzihasanovic A., van den Berg B., “Nonstandard Functional Interpretations and Categorical Models”, Notre Dame J. Form. Log., 58:3 (2017), 343–380
34. Rinaldi D., Schuster P., Wessel D., “Eliminating Disjunctions By Disjunction Elimination”, Indag. Math.-New Ser., 29:1, SI (2018), 226–259
35. Leustean L., Nicolae A., Sipos A., “An Abstract Proximal Point Algorithm”, J. Glob. Optim., 72:3 (2018), 553–577
36. Miller D., “Mechanized Metatheory Revisited”, J. Autom. Reasoning, 63:3 (2019), 625–665
37. Dinis B., Pinto P., “Metastability of the Proximal Point Algorithm With Multi-Parameters”, Port Math., 77:3-4 (2020), 345–381
•  Number of views: This page: 593 Full text: 193 References: 43