Posted by N. Pischke - 11.02.25
The list given here is an attempt to collect some of the many relevant references for works from and around the area of proof mining. For simplicity, the focus is (initially) on applications in analysis and on applications using functional interpretations. Through the breadth of this goal, the list nevertheless will presumably always be incomplete.
Suggestions for additions can be send to pischke@mathematik.tu-darmstadt.de.
The references are ordered alphabetically via the authors. Click here for a PDF version.
[1] | D. Ariza-Ruiz, E.M. Briseid, A. Jiménez-Melado, and G. López-Acedo. Rate of convergence under weak contractiveness conditions. Fixed Point Theory, 14(1):11--28, 2013. |
[2] | D. Ariza-Ruiz, L. Leuştean, and G. Lopez-Acedo. Firmly nonexpansive mappings in classes of geodesic spaces. Transactions of the American Mathematical Society, 366:4299--4322, 2014. DOI. |
[3] | R. Arthan and P. Oliva. On the Borel-Cantelli Lemmas, the Erdós-Rényi Theorem, and the Kochen-Stone Theorem. Journal of Logic and Analysis, 13(6):1--23, 2021. DOI. |
[4] | J. Avigad. The metamathematics of ergodic theory. Annals of Pure and Applied Logic, 157(2--3):64--76, 2009. DOI. |
[5] | J. Avigad, E.T. Dean, and J. Rute. A metastable dominated convergence theorem. Journal of Logic and Analysis, 4(3):1--19, 2012. DOI. |
[6] | J. Avigad, P. Gerhardy, and H. Towsner. Local stability of ergodic averages. Transactions of the American Mathematical Society, 362:261--288, 2010. DOI. |
[7] | J. Avigad and J. Rute. Oscillation and the mean ergodic theorem for uniformly convex Banach spaces. Ergodic Theory and Dynamical Systems, 35:1009--1027, 2015. DOI. |
[8] | J. Avigad and H. Towsner. Metastability in the Furstenberg-Zimmer tower. Fundamenta Mathematicae, 210(3):243--268, 2010. DOI. |
[9] | M. Baaz. Note on the generalization of calculations. Theoretical Computer Science, 224(1--2):3--11, 1999. DOI. |
[10] | M. Bacak and U. Kohlenbach. On proximal mappings with Young functions in uniformly convex Banach spaces. Journal of Convex Analysis, 25:1291--1318, 2018. |
[11] | M.J. Beeson. Principles of continuous choice and continuity of functions in formal systems for constructive mathematics. Annals of Mathematical Logic, 12:249--322, 1977. DOI. |
[12] | M.J. Beeson. Foundations of Constructive Mathematics. Ergebnisse der Mathematik und ihrer Grenzgebiete. Springer Berlin, Heidelberg, 1985. DOI. |
[13] | G. Bellin. Ramsey interpreted: a parametric version of Ramsey's theorem. In Logic and computation (Pittsburgh, PA, 1987), volume 106 of Contemporary Mathematics, pages 17--37. American Mathematical Society, Providence, RI,, 1990. |
[14] | E. Bishop. Mathematics as a Numerical Language. In A. Kino, J. Myhill, and R.E. Vesley, editors, Intuitionism and Proof Theory: Proceedings of the Summer Conference at Buffalo N.Y., pages 53--71. North-Holland, Amsterdam, 1968. DOI. |
[15] | E.M. Briseid. A rate of convergence for asymptotic contractions. Journal of Mathematical Analysis and Applications, 330(1):364--376, 2007. DOI. |
[16] | E.M. Briseid. Some results on Kirk's asymptotic contractions. Fixed Point Theory, 8(1):17--27, 2007. |
[17] | E.M. Briseid. Fixed points of generalized contractive mappings. Journal of Nonlinear and Convex Analysis, 9(2):181--204, 2008. |
[18] | E.M. Briseid. Logical aspects of rates of convergence in metric spaces. The Journal of Symbolic Logic, 74:1401--1428, 2009. DOI. |
[19] | E.M. Briseid. On Rates of Convergence in Metric Fixed Point Theory. PhD thesis, TU Darmstadt, 2009. |
[20] | E.M. Briseid. A new uniformity for asymptotic contractions in the sense of Kirk. International Journal of Mathematics and Statistics, 6:2--13, 2010. |
[21] | H. Cheval. Rates of asymptotic regularity of the Tikhonov-Mann iteration for families of mappings. Revue Roumaine de Mathématiques Pures et Appliquées, 2023. To appear. |
[22] | H. Cheval, U. Kohlenbach, and L. Leustean. On modified Halpern and Tikhonov-Mann iterations. Journal of Optimization Theory and Applications, 197:233--251, 2023. DOI. |
[23] | H. Cheval and L. Leuştean. Quadratic rates of asymptotic regularity for the Tikhonov-Mann iteration. Optimization Methods and Software, 37:2225--2240, 2022. DOI. |
[24] | H. Cheval and L. Leuştean. Linear rates of asymptotic regularity for Halpern-type iterations. Mathematics of Computation, 2024. To appear. DOI. |
[25] | V. Colao, L. Leuştean, G. Lopez-Acedo, and V. Martin-Marquez. Alternative iterative methods for nonexpansive mappings, rates of convergence and application. Journal of Convex Analysis, 18:465--487, 2011. |
[26] | C.N. Delzell. Kreisel's Unwinding of Artin's Proof. In P. Odifreddi, editor, Kreiseliana: about and around Georg Kreisel, pages 113--246. A.K. Peters, Wellesley Massachusetts, 1996. |
[27] | L.M. Després and U. Kohlenbach. Herbrand analyses in geometry: a case study. 2024. Manuscript available at https://www2.mathematik.tu-darmstadt.de/~kohlenbach/. |
[28] | B. Dinis and J. Gaspar. Intuitionistic nonstandard bounded modified realisability and functional interpretation. Annals of Pure and Applied Logic, 169(5):392--412, 2018. DOI. |
[29] | B. Dinis and P. Pinto. Metastability of the multi-parameters proximal point algorithm. Portugaliae Mathematica, 77(3/4):345--381, 2020. DOI. |
[30] | B. Dinis and P. Pinto. On the convergence of algorithms with Tikhonov regularization terms. Optimization Letters, 15(4):1263--1276, 2021. DOI. |
[31] | B. Dinis and P. Pinto. Quantitative Results on the Multi-Parameters Proximal Point Algorithm. Journal of Convex Analysis, 28(3):729--750, 2021. |
[32] | B. Dinis and P. Pinto. Strong convergence for the alternating Halpern-Mann iteration in CAT(0) spaces. SIAM Journal on Optimization, 33(2):785--815, 2023. DOI. |
[33] | B. Dinis and P. Pinto. Effective metastability for a method of alternating resolvents. Fixed Point Theory, 25(1):61--98, 2024. DOI. |
[34] | P. Engrácia. Proof-theoretic studies on the bounded functional interpretation. PhD thesis, Universidade de Lisboa, 2009. |
[35] | P. Engrácia and F. Ferreira. The bounded functional interpretation of the double negation shift. The Journal of Symbolic Logic, 75(2):759--773, 2010. DOI. |
[36] | P. Engrácia and F. Ferreira. Bounded functional interpretation with an abstract type. In A. Rezuş, editor, Contemporary Logic and Computing, volume 1 of Landscapes in Logic, pages 87--112. College Publications, 2020. |
[37] | S. Feferman. Kreisel's `Unwinding Program'. In P. Odifreddi, editor, Kreiseliana: about and around Georg Kreisel, pages 247--273. A.K. Peters, Wellesley Massachusetts, 1996. |
[38] | F. Ferreira. Injecting uniformities into Peano arithmetic. Annals of Pure and Applied Logic, 157(2--3):122--129, 2009. DOI. |
[39] | F. Ferreira. Bounds for indexes of nilpotency in commutative ring theory: A proof mining approach. Bulletin of Symbolic Logic, 26(3--4):257--267, 2020. DOI. |
[40] | F. Ferreira. The abstract type of the real number. Archive for Mathematical Logic, 60(7--8):1005--1017, 2021. DOI. |
[41] | F. Ferreira and J. Gaspar. Nonstandardness and the bounded functional interpretation. Annals of Pure and Applied Logic, 166(6):701--712, 2015. DOI. |
[42] | F. Ferreira, L. Leuştean, and P. Pinto. On the removal of weak compactness arguments in proof mining. Advances in Mathematics, 354:106728, 55pp., 2019. DOI. |
[43] | F. Ferreira and P. Oliva. Bounded functional interpretation. Annals of Pure and Applied Logic, 135(1--3):73--112, 2005. DOI. |
[44] | F. Ferreira and P. Oliva. Bounded functional interpretation and feasible analysis. Annals of Pure and Applied Logic, 145(2):115--129, 2007. DOI. |
[45] | G. Ferreira and P. Oliva. On bounded functional interpretations. Annals of Pure and Applied Logic, 163(8):1030--1049, 2012. DOI. |
[46] | R. Findling and U. Kohlenbach. Rates of convergence and metastability for Chidume's algorithm for the approximation of zeros of accretive operators in Banach spaces. Numerical Functional Analysis and Optimization, 45(3):216--233, 2024. DOI. |
[47] | P. Firmino and L. Leuştean. Quantitative asymptotic regularity of the VAM iteration with error terms for m-accretive operators in Banach spaces. Zeitschrift für Analysis und ihre Anwendungen, 2024. To appear. DOI. |
[48] | P. Firmino and P. Pinto. The alternating Halpern-Mann iteration for families of maps. 2024. Manuscript available at https://www2.mathematik.tu-darmstadt.de/~pinto/. |
[49] | A. Freund and U. Kohlenbach. R.E. Bruck, proof mining and a rate of asymptotic regularity for ergodic averages in Banach spaces. Applied Set-Valued Analysis and Optimization, 4:323--336, 2022. DOI. |
[50] | A. Freund and U. Kohlenbach. Bounds for a nonlinear ergodic theorem for Banach spaces. Ergodic Theory and Dynamical Systems, 43:1570--1593, 2023. DOI. |
[51] | J. Gaspar. Factorization of the Shoenfield-like bounded functional interpretation. Notre Dame Journal of Formal Logic, 50(1):53--60, 2009. DOI. |
[52] | J. Gaspar. Proof interpretations: theoretical and practical aspects. PhD thesis, TU Darmstadt, 2011. |
[53] | J. Gaspar and U. Kohlenbach. On Tao's "finitary" infinite pigeonhole principle. The Journal of Symbolic Logic, 75:355--371, 2010. DOI. |
[54] | J. Gaspar and P. Oliva. Proof interpretations with truth. Mathematical Logic Quarterly, 56(6):591--610, 2010. DOI. |
[55] | P. Gerhardy. A quantitative version of Kirk's fixed point theorem for asymptotic contractions. Journal of Mathematical Analysis and Applications, 316(1):339--345, 2006. DOI. |
[56] | P. Gerhardy. Applications of Proof Interpretations. PhD thesis, University of Aarhus, 2006. |
[57] | P. Gerhardy. Proof mining in topological dynamics. Notre Dame Journal of Formal Logic, 49:431--446, 2008. DOI. |
[58] | P. Gerhardy and U. Kohlenbach. Strongly uniform bounds from semi-constructive proofs. Annals of Pure and Applied Logic, 141:89--107, 2006. DOI. |
[59] | P. Gerhardy and U. Kohlenbach. General logical metatheorems for functional analysis. Transactions of the American Mathematical Society, 360:2615--2660, 2008. DOI. |
[60] | J.-Y. Girard. The ordinal ε0 and arithmetic. In Proof Theory and Logical Complexity, volume 1 of Studies in Proof Theory, pages 411--496. Bibliopolis, 1977. |
[61] | I. Goldbring, B. Hart, and H. Towsner. Explicit sentences distinguishing McDuff's II1 factors. arXiv preprint, arXiv:1701.07928, 2017. |
[62] | D. Günzel and U. Kohlenbach. Logical metatheorems for abstract spaces axiomatized in positive bounded logic. Advances in Mathematics, 290:503--551, 2016. DOI. |
[63] | D. Ivan and L. Leuştean. A rate of asymptotic regularity for the Mann iteration of k-strict pseudo-contractions. Numerical Functional Analysis and Optimization, 36:792--798, 2015. DOI. |
[64] | M.A.A. Khan and U. Kohlenbach. Bounds on Kuhfittig's iteration schema in uniformly convex hyperbolic spaces. Journal of Mathematical Analysis and Applications, 403:633--642, 2013. DOI. |
[65] | M.A.A. Khan and U. Kohlenbach. Quantitative image recovery theorems. Nonlinear Analysis: Theory, Methods & Applications, 106:138--150, 2014. DOI. |
[66] | U. Kohlenbach. Theorie der majorisierbaren und stetigen Funktionale und ihre Anwendung bei der Extraktion von Schranken aus inkonstruktiven Beweisen: Effektive Eindeutigkeitsmodule bei besten Approximationen aus ineffektiven Eindeutigkeitsbeweisen. PhD thesis, Johann Wolfgang Goethe-Universität Frankfurt am Main, 1990. |
[67] | U. Kohlenbach. Effective bounds from ineffective proofs in analysis: an application of functional interpretation and majorization. The Journal of Symbolic Logic, 57:1239--1273, 1992. DOI. |
[68] | U. Kohlenbach. Effective moduli from ineffective uniqueness proofs. An unwinding of de La Vallée Poussin’s proof for Chebycheff approximation. Annals of Pure and Applied Logic, 64:27--94, 1993. DOI. |
[69] | U. Kohlenbach. New effective moduli of uniqueness and uniform a-priori estimates for constants of strong unicity by logical analysis of known proofs in best approximation theory. Numerical Functional Analysis and Optimization, 14:581--606, 1993. DOI. |
[70] | U. Kohlenbach. Analysing proofs in analysis. In W. Hodges, M. Hyland, C. Steinhorn, and J. Truss, editors, Logic: from Foundations to Applications. European Logic Colloquium (Keele, 1993), pages 225--260. Oxford University Press, 1996. |
[71] | U. Kohlenbach. Mathematically strong subystems of analysis with low rate of growth of provably recursive functionals. Archive for Mathematical Logic, 36:31--71, 1996. DOI. |
[72] | U. Kohlenbach. Arithmetizing proofs in analysis. In J.M. Larrazabal, D. Lascar, and G. Mints, editors, Logic Colloquium '96, volume 12 of Springer Lecture Notes in Logic, pages 115--158. Springer Berlin Heidelberg, 1998. |
[73] | U. Kohlenbach. Elimination of Skolem functions for monotone formulas in analysis. Archive for Mathematical Logic, 37:363--390, 1998. DOI. |
[74] | U. Kohlenbach. On the arithmetical content of restricted forms of comprehension, choice and general uniform boundedness. Annals of Pure and Applied Logic, 95:257--285, 1998. DOI. |
[75] | U. Kohlenbach. Proof theory and computational analysis. Electronic Notes in Theoretical Computer Science, 13:124--157, 1998. DOI. |
[76] | U. Kohlenbach. Relative constructivity. The Journal of Symbolic Logic, 63:1218--1238, 1998. DOI. |
[77] | U. Kohlenbach. The use of a logical principle of uniform boundedness in analysis. In A. Cantini, E. Casari, and P. Minari, editors, Logic and Foundations of Mathematics, volume 280 of Synthese Library, pages 93--106. Kluwer Academic Publishers, 1999. DOI. |
[78] | U. Kohlenbach. Things that can and things that can't be done in PRA. Annals of Pure and Applied Logic, 102:223--245, 2000. DOI. |
[79] | U. Kohlenbach. A quantitative version of a theorem due to Borwein-Reich-Shafrir. Numerical Functional Analysis and Optimization, 22:641--656, 2001. DOI. |
[80] | U. Kohlenbach. On the computational content of the Krasnoselski and Ishikawa fixed point theorems. In J. Blanck, V. Brattka, P. Hertling, and K. Weihrauch, editors, Proceedings of the Fourth Workshop on Computability and Complexity in Analysis, volume 2064 of Lecture Notes in Computer Science, pages 119--145. Springer Berlin Heidelberg, 2001. DOI. |
[81] | U. Kohlenbach. Applied foundations: proof mining in analysis. Newsletter of the Danish Mathematical Society (`Matilde'), 13:7--9, 2002. |
[82] | U. Kohlenbach. Foundational and mathematical uses of higher types. In W. Sieg, R. Sommer, and C. Talcott, editors, Reflections on the Foundations of Mathematics: Essays in Honor of Solomon Feferman, volume 15 of Lecture Notes in Logic, pages 92--116. A.K. Peters, 2002. |
[83] | U. Kohlenbach. Uniform asymptotic regularity for Mann iterates. Journal of Mathematical Analysis and Applications, 279:531--544, 2003. DOI. |
[84] | U. Kohlenbach. Some computational aspects of metric fixed point theory. Nonlinear Analysis: Theory, Methods & Applications, 61:823--837, 2005. DOI. |
[85] | U. Kohlenbach. Some logical metatheorems with applications in functional analysis. Transactions of the American Mathematical Society, 357(1):89--128, 2005. DOI. |
[86] | U. Kohlenbach. A logical uniform boundedness principle for abstract metric and hyperbolic spaces. Electronic Notes in Theoretical Computer Science, 165:81--93, 2006. DOI. |
[87] | U. Kohlenbach. Proof interpretations and the computational content of proofs in mathematics. Bulletin EATCS, 93:143--173, 2007. |
[88] | U. Kohlenbach. Applied Proof Theory: Proof Interpretations and their Use in Mathematics. Springer Monographs in Mathematics. Springer Heidelberg-Berlin, 2008. DOI. |
[89] | U. Kohlenbach. Effective uniform bounds from proofs in abstract functional analysis. In B. Cooper, B. Loewe, and A. Sorbi, editors, New Computational Paradigms: Changing Conceptions of What is Computable, pages 223--258. Springer Publisher, 2008. DOI. |
[90] | U. Kohlenbach. Herbrand's theorem and extractive proof theory. SMF - Gazette des Mathematiciens, 118:29--41, 2008. |
[91] | U. Kohlenbach. On the logical analysis of proofs based on nonseparable Hilbert space theory. In S. Feferman and W. Sieg, editors, Proofs, Categories and Computations. Essays in Honor of Grigori Mints, pages 131--143. College Publications, 2010. |
[92] | U. Kohlenbach. A note on the monotone functional interpretation. Mathematical Logic Quarterly, 57:611--614, 2011. DOI. |
[93] | U. Kohlenbach. Gödel's functional interpretation and its use in current mathematics. In M. Baaz, C.H. Papadimitriou, H.W. Putnam, D.S. Scott, and C.L. Harper Jr., editors, Kurt Gödel and the Foundations of Mathematics. Horizons of Truth, pages 361--398. Cambridge University Press, New York, 2011. DOI. |
[94] | U. Kohlenbach. On quantitative versions of theorems due to F.E. Browder and R. Wittmann. Advances in Mathematics, 226:2764--2795, 2011. DOI. |
[95] | U. Kohlenbach. On the asymptotic behavior of odd operators. Journal of Mathematical Analysis and Applications, 382:615--620, 2011. DOI. |
[96] | U. Kohlenbach. A uniform quantitative form of sequential weak compactness and Baillon's nonlinear ergodic theorem. Communications in Contemporary Mathematics, 14:20pp., 2012. DOI. |
[97] | U. Kohlenbach. Gödel functional interpretation and weak compactness. Annals of Pure and Applied Logic, 163:1560--1579, 2012. DOI. |
[98] | U. Kohlenbach. On the quantitative asymptotic behavior of strongly nonexpansive mappings in Banach and geodesic spaces. Israel Journal of Mathematics, 216:215--246, 2016. DOI. |
[99] | U. Kohlenbach. Recent progress in proof mining in nonlinear analysis. IFCoLog Journal of Logics and their Applications, 10(4):3361--3410, 2017. |
[100] | U. Kohlenbach. A polynomial rate of asymptotic regularity for compositions of projections in Hilbert space. Foundations of Computational Mathematics, 19:83--99, 2019. DOI. |
[101] | U. Kohlenbach. Proof-theoretic Methods in Nonlinear Analysis. In B. Sirakov, P. Ney de Souza, and M. Viana, editors, Proceedings ICM 2018, volume 2, pages 61--82. World Scientific, 2019. DOI. |
[102] | U. Kohlenbach. Local formalizations in nonlinear analysis and related areas and proof-theoretic tameness. In P. Weingartner and H.-P. Leeb, editors, Kreisel's Interests. On the Foundations of Logic and Mathematics, volume 41 of Tributes, pages 45--61. College Publications, 2020. |
[103] | U. Kohlenbach. Quantitative analysis of a Halpern-type Proximal Point Algorithm for accretive operators in Banach spaces. Journal of Nonlinear and Convex Analysis, 21(9):2125--2138, 2020. LINK. |
[104] | U. Kohlenbach. Proof-theoretic uniform boundedness and bounded collection principles and Heine-Borel compactness. Archive for Mathematical Logic, 60:995--1003, 2021. DOI. |
[105] | U. Kohlenbach. Quantitative results on the Proximal Point Algorithm in uniformly convex Banach spaces. Journal of Convex Analysis, 28(1):11--18, 2021. |
[106] | U. Kohlenbach. On the Proximal Point Algorithm and its Halpern-type variant for generalized monotone operators in Hilbert space. Optimization Letters, 16:611--621, 2022. DOI. |
[107] | U. Kohlenbach. Kreisel's `shift of emphasis' and contemporary proof mining. Studies in Logic, 16(3):1--35, 2023. |
[108] | U. Kohlenbach and D. Körnlein. Rate of metastability for Bruck's iteration of pseudocontractive mappings in Hilbert space. Numerical Functional Analysis and Optimization, 35:20--31, 2014. DOI. |
[109] | U. Kohlenbach and A. Koutsoukou-Argyraki. Rates of convergence and metastability for abstract Cauchy problems generated by accretive operators. Journal of Mathematical Analysis and Applications, 423:1089--1112, 2015. DOI. |
[110] | U. Kohlenbach and A. Koutsoukou-Argyraki. Effective asymptotic regularity for one-parameter nonexpansive semigroups. Journal of Mathematical Analysis and Applications, 433:1883--1903, 2016. DOI. |
[111] | U. Kohlenbach and A. Kreuzer. Ramsey's theorem for pairs and provably recursive functions. Notre Dame Journal of Formal Logic, 50:427--444, 2009. DOI. |
[112] | U. Kohlenbach and A.P. Kreuzer. Term extraction and Ramsey's theorem for pairs. The Journal of Symbolic Logic, 77:853--895, 2012. DOI. |
[113] | U. Kohlenbach and B. Lambov. Bounds on iterations of asymptotically quasi-nonexpansive mappings. In G.J. Falset, E.L. Fuster, and B. Sims, editors, Proceedings of the International Conference on Fixed Point Theory, Valencia 2003, pages 143--172. Yokohama Press, 2004. LINK. |
[114] | U. Kohlenbach and L. Leuştean. Mann iterates of directionally nonexpansive mappings in hyperbolic spaces. Abstract and Applied Analysis, 2003(8):449--477, 2003. DOI. |
[115] | U. Kohlenbach and L. Leuştean. The approximate fixed point property in product spaces. Nonlinear Analysis: Theory, Methods & Applications, 66:806--818, 2007. DOI. |
[116] | U. Kohlenbach and L. Leuştean. A quantitative mean ergodic theorem for uniformly convex Banach spaces. Ergodic Theory and Dynamical Systems, 29:1907--1915, 2009. DOI. |
[117] | U. Kohlenbach and L. Leuştean. Asymptotically nonexpansive mappings in uniformly convex hyperbolic spaces. Journal of the European Mathematical Society, 12:71--92, 2010. DOI. |
[118] | U. Kohlenbach and L. Leuştean. Effective metastability of Halpern iterates in CAT(0) spaces. Advances in Mathematics, 231:2526--2556, 2012. DOI. |
[119] | U. Kohlenbach and L. Leuştean. On the computational content of convergence proofs via Banach limits. Philosophical Transactions of the Royal Society A, 370(1971):3449--3463, 2012. DOI. |
[120] | U. Kohlenbach, L. Leuştean, and A. Nicolae. Quantitative results on Fejér monotone sequences. Communications in Contemporary Mathematics, 20:42pp., 2018. DOI. |
[121] | U. Kohlenbach, G. López-Acedo, and A. Nicolae. Quantitative asymptotic regularity results for the composition of two mappings. Optimization, 66:1291--1299, 2017. DOI. |
[122] | U. Kohlenbach, G. Lopez-Acedo, and A. Nicolae. Moduli of regularity and rates of convergence for Fejér monotone sequences. Israel Journal of Mathematics, 232:261--297, 2019. DOI. |
[123] | U. Kohlenbach, G. Lopez-Acedo, and A. Nicolae. A uniform betweenness property in metric spaces and its role in the quantitative analysis of the `Lion-Man' game. Pacific Journal of Mathematics, 310:181--212, 2021. DOI. |
[124] | U. Kohlenbach and A. Nicolae. A proof-theoretic bound extraction theorem for CAT(κ)-spaces. Studia Logica, 105:611--624, 2017. DOI. |
[125] | U. Kohlenbach and P. Oliva. Proof mining: a systematic way of analysing proofs in mathematics. Proceedings of the Steklov Institute of Mathematics, 242:136--164, 2003. |
[126] | U. Kohlenbach and P. Oliva. Proof mining in L1-approximation. Annals of Pure and Applied Logic, 121:1--38, 2003. DOI. |
[127] | U. Kohlenbach and P. Pinto. Quantitative translations for viscosity approximation methods in hyperbolic spaces. Journal of Mathematical Analysis and Applications, 507:125823, 33pp., 2022. DOI. |
[128] | U. Kohlenbach and P. Pinto. Fejér monotone sequences revisited. Journal of Convex Analysis, 2024. To appear. |
[129] | U. Kohlenbach and N. Pischke. Proof theory and nonsmooth analysis. Philosophical Transactions of the Royal Society A, 381(2248):21pp., 2023. DOI. |
[130] | U. Kohlenbach and N. Pischke. Quantitative results for a Tseng-type primal-dual method for composite monotone inclusions. 2024. Manuscript available at https://nicholaspischke.github.io/. |
[131] | U. Kohlenbach and T. Powell. Rates of convergence for iterative solutions of equations involving set-valued accretive operators. Computers & Mathematics with Applications, 80:490--503, 2020. DOI. |
[132] | U. Kohlenbach and P. Safarik. On the computational content of the Bolzano-Weierstrass principle. Mathematical Logic Quaterly, 56:508--532, 2010. DOI. |
[133] | U. Kohlenbach and P. Safarik. Fluctuations, effective learnability and metastability in analysis. Annals of Pure and Applied Logic, 165:266--304, 2014. DOI. |
[134] | U. Kohlenbach and A. Sipoş. The finitary content of sunny nonexpansive retractions. Communications in Contemporary Mathematics, 23(1):1950093, 63pp., 2021. DOI. |
[135] | D. Körnlein. Quantitative results for Halpern iterations of nonexpansive mappings. Journal of Mathematical Analysis and Applications, 428(2):1161--1172, 2015. DOI. |
[136] | D. Körnlein. Quantitative Analysis of Iterative Algorithms in Fixed Point Theory and Convex Optimization. PhD thesis, TU Darmstadt, 2016. |
[137] | D. Körnlein. Quantitative results for Bruck iterations of demicontinuous pseudocontractions. arXiv preprint, arXiv:1610.00515, 2016. |
[138] | D. Körnlein. Quantitative strong convergence for the hybrid steepest descent method. arXiv preprint, arXiv:1610.00517, 2016. |
[139] | D. Körnlein and U. Kohlenbach. Effective rates of convergence for Lipschitzian pseudocontractive mappings in general Banach spaces. Nonlinear Analysis: Theory, Methods & Applications, 74:5253--5267, 2011. DOI. |
[140] | A. Koutsoukou-Argyraki. Proof Mining for Nonlinear Operator Theory: Four Case Studies on Accretive Operators, the Cauchy Problem and Nonexpansive Semigroups. PhD thesis, TU Darmstadt, 2016. |
[141] | A. Koutsoukou-Argyraki. Effective rates of convergence for the resolvents of accretive operators. Numerical Functional Analysis and Optimization, 38(12):1601--1613, 2017. DOI. |
[142] | A. Koutsoukou-Argyraki. New effective bounds for the approximate common fixed points and asymptotic regularity of nonexpansive semigroups. Journal of Logic and Analysis, 10(7):1--30, 2018. DOI. |
[143] | A. Koutsoukou-Argyraki. On Preserving the Computational Content of Mathematical Proofs: Toy Examples for a Formalising Strategy. In Connecting with Computability. CiE 2021, volume 12813 of LNCS, pages 285--296. Springer, 2021. DOI. |
[144] | G. Kreisel. On the interpretation of non-finitist proofs, part I. The Journal of Symbolic Logic, 16:241--267, 1951. DOI. |
[145] | G. Kreisel. On the interpretation of non-finitist proofs, part II. The Journal of Symbolic Logic, 17:43--58, 1952. DOI. |
[146] | G. Kreisel. Mathematical significance of consistency proofs. The Journal of Symbolic Logic, 23:155--182, 1958. DOI. |
[147] | G. Kreisel. Interpretation of analysis by means of constructive functionals of finite types. In A. Heyting, editor, Constructivity in Mathematics, pages 101--128. North-Holland, Amsterdam, 1959. |
[148] | G. Kreisel. Hilbert's programme and the search for automatic proof procedures. In M. Laudet, D. Lacombe, L. Nolin, and M. Schützenberger, editors, Symposium on Automatic Deduction, volume 125 of Lecture Notes in Mathematics, pages 128--146. Springer, 1970. DOI. |
[149] | G. Kreisel. Der unheilvolle Einbruch der Logik in die Mathematik. Acta Philosophica Fennica, 28:166--187, 1976. |
[150] | G. Kreisel. What have we learnt from Hilbert's second problem? In F.E. Browder, editor, Mathematical developments arising from Hilbert problems, volume 28 of Proceedings of Symposia in Pure Mathematics, pages 93--130. AMS, 1976. |
[151] | G. Kreisel. On the kind of data needed for a theory of proofs. In R. Gandy and M. Hyland, editors, Logic Colloquium 76, pages 111--128. North-Holland Publishing Company, 1977. DOI. |
[152] | G. Kreisel. Finiteness theorems in arithmetic: an application of Herbrand’s theorem for Σ2-formulas. In Proceedings of the Herbrand symposium (Marseille, 1981), pages 39--55. North-Holland, Amsterdam, 1982. DOI. |
[153] | G. Kreisel. Proof Theory and Synthesis of Programs: Potentials and Limitations. In B. Buchberger, editor, Eurocal ’85 (Linz 1985), volume 203 of Lecture Notes in Computer Science, pages 136--150. Springer, 1986. DOI. |
[154] | G. Kreisel. Logical aspects of computation: contributions and distractions. In P. Odifreddi, editor, Logic and Computer Science, pages 205--278. Academic Press, London, 1990. |
[155] | G. Kreisel. Logical Hygiene, Foundations, and Abstractions: Diversity among Aspects and Options. In M. Baaz, C.H. Papadimitriou, H.W. Putnam, D.S. Scott, and C.L. Harper Jr., editors, Kurt Gödel and the Foundations of Mathematics. Horizons of Truth, pages 27--53. Cambridge University Press, New York, 2011. DOI. |
[156] | G. Kreisel and A. Macintyre. Constructive logic versus algebraization I. In A.S. Troelstra and D. van Dalen, editors, Proceedings L.E.J. Brouwer Centenary Symposium (Noordwijkerhout 1981), pages 217--260. North-Holland, Amsterdam, 1982. DOI. |
[157] | A. Kreuzer. A logical analysis of the generalized Banach contractions principle. Journal of Logic and Analysis, 4(17):1--16, 2012. DOI. |
[158] | A. Kreuzer. Non-principal ultrafilters, program extraction and higher order reverse mathematics. Journal of Mathematical Logic, 12(1):1250002, 16pp., 2012. DOI. |
[159] | A. Kreuzer. Program extraction for 2-random reals. Archive for Mathematical Logic, 52(5--6):659--666, 2013. DOI. |
[160] | A. Kreuzer. Measure theory and higher order arithmetic. Proceedings of the American Mathematical Society, 143:5411--5425, 2015. DOI. |
[161] | A.P. Kreuzer. Proof mining and combinatorics: Program extraction for Ramsey's theorem for pairs. PhD thesis, TU Darmstadt, 2012. |
[162] | B. Lambov. Rates of convergence of recursively defined sequences. Electronic Notes in Theoretical Computer Science, 120:125--133, 2005. DOI. |
[163] | B. Lambov. Topics in the Theory and Practice of Computable Analysis. PhD thesis, University of Aarhus, 2006. DOI. |
[164] | L. Leuştean. Proof mining in R-trees and hyperbolic spaces. Electronic Notes in Theoretical Computer Science, 165:95--106, 2006. DOI. |
[165] | L. Leuştean. A quadratic rate of asymptotic regularity for CAT(0)-spaces. Journal of Mathematical Analysis and Applications, 325:386--399, 2007. DOI. |
[166] | L. Leuştean. Rates of asymptotic regularity for Halpern iterations of nonexpansive mappings. Journal of Universal Computer Science, 13:1680--1691, 2007. |
[167] | L. Leuştean. Nonexpansive iterations in uniformly convex W-hyperbolic spaces. In A. Leizarowitz, B.S. Mordukhovich, I. Shafrir, and A. Zaslavski, editors, Nonlinear Analysis and Optimization I: Nonlinear Analysis, volume 513 of Contemporary Mathematics, pages 193--209. American Mathematical Society, 2010. |
[168] | L. Leuştean. An application of proof mining to nonlinear iterations. Annals of Pure and Applied Logic, 165:1484--1500, 2014. DOI. |
[169] | L. Leuştean and A. Nicolae. Effective results on compositions of nonexpansive mappings. Journal of Mathematical Analysis and Applications, 410:902--907, 2014. DOI. |
[170] | L. Leuştean and A. Nicolae. A note on an ergodic theorem in weakly uniformly convex geodesic spaces. Archiv der Mathematik, 105:467--477, 2015. DOI. |
[171] | L. Leuştean and A. Nicolae. Effective results on nonlinear ergodic averages in CAT(k) spaces. Ergodic Theory and Dynamical Systems, 36:2580--2601, 2016. DOI. |
[172] | L. Leuştean and A. Nicolae. A note on an alternative iterative method for nonexpansive mappings. Journal of Convex Analysis, 24:501--503, 2017. |
[173] | L. Leuştean, A. Nicolae, and A. Sipoş. An abstract proximal point algorithm. Journal of Global Optimization, 72(3):553--577, 2018. DOI. |
[174] | L. Leuştean and P. Pinto. Quantitative results on a Halpern-type proximal point algorithm. Computational Optimization and Applications, 79(1):101--125, 2021. DOI. |
[175] | L. Leuştean and P. Pinto. Rates of asymptotic regularity for the alternating Halpern-Mann iteration. Optimization Letters, 18:529--543, 2024. DOI. |
[176] | L. Leuştean, V. Radu, and A. Sipoş. Quantitative results on the Ishikawa iteration of Lipschitz pseudo-contractions. Journal of Nonlinear and Convex Analysis, 17(11):2277--2292, 2016. LINK. |
[177] | L. Leuştean and A. Sipoş. An application of proof mining to the proximal point algorithm in CAT(0) spaces. In A. Bellow, C. Calude, and T. Zamfirescu, editors, Mathematics Almost Everywhere. In Memory of Solomon Marcus, pages 153--168. World Scientific, 2018. DOI. |
[178] | L. Leuştean and A. Sipoş. Effective strong convergence of the proximal point algorithm in CAT(0) spaces. Journal of Nonlinear and Variational Analysis, 2(2):219--228, 2018. LINK. |
[179] | H. Luckhardt. Herbrand-Analysen zweier Beweise des Satzes von Roth: Polynomiale Anzahlschranken. The Journal of Symbolic Logic, 54:234--263, 1989. DOI. |
[180] | H. Luckhardt. Bounds Extracted by Kreisel from Ineffective Proofs. In P. Odifreddi, editor, Kreiseliana: about and around Georg Kreisel, pages 289--300. A.K. Peters, Wellesley Massachusetts, 1996. |
[181] | A. Macintyre. The mathematical significance of proof theory. Philosophical Transactions of the Royal Society A, 363(1835):2419--2435, 2005. DOI. |
[182] | G. Moser and T. Powell. On the computational content of termination proofs. In Proceedings of CiE '15, pages 276--285, 2015. DOI. |
[183] | M. Neri. A finitary Kronecker's lemma and large deviations in the Strong Law of Large numbers on Banach spaces. arXiv preprint, arXiv:2411.08620, 2024. |
[184] | M. Neri. Quantitative Strong Laws of Large Numbers. Electronic Journal of Probability, 30, 2025. 20, 22pp., DOI. |
[185] | M. Neri and N. Pischke. Proof mining and probability theory. arXiv preprint, arXiv:2403.00659, 2024. |
[186] | M. Neri, N. Pischke, and T. Powell. Generalized learnability of stochastic principles. 2025. Manuscript available at https://nicholaspischke.github.io/. |
[187] | M. Neri and T. Powell. A computational study of a class of recursive inequalities. Journal of Logic and Analysis, 15(3):1--48, 2023. DOI. |
[188] | M. Neri and T. Powell. A quantitative Robbins-Siegmund theorem. arXiv preprint, arXiv:2410.15986, 2024. |
[189] | M. Neri and T. Powell. On quantitative convergence for stochastic processes: Crossings, fluctuations and martingales. arXiv preprint, arXiv:2406.19979, 2024. |
[190] | A. Nicolae. Asymptotic behavior of averaged and firmly nonexpansive mappings in geodesic spaces. Nonlinear Analysis: Theory, Methods & Applications, 87:102--115, 2013. DOI. |
[191] | P. Oliva. On the computational complexity of L1-approximation. Mathematical Logic Quarterly, 48(66--77):1, 2002. DOI. |
[192] | P. Oliva. Polynomial-time algorithms from ineffective proofs. In 18th Annual IEEE Symposium of Logic in Computer Science, 2003. Proceedings., pages 128--137, 2003. DOI. |
[193] | P. Oliva. Proof Mining in Subsystems of Analysis. PhD thesis, University of Aarhus, 2003. |
[194] | P. Oliva and T. Powell. A constructive interpretation of Ramsey's theorem via the product of selection functions. Mathematical Structure in Computer Science, 25(8):1755--1778, 2015. DOI. |
[195] | P. Oliva and T. Powell. A game-theoretic computational interpretation of proofs in classical analysis. In R. Kahle and M. Rathjen, editors, Gentzen's Centenary: The Quest for Consistency, pages 501--531. Springer, 2015. DOI. |
[196] | P. Pinto. Proof mining with the bounded functional interpretation. PhD thesis, Universidade de Lisboa, 2019. |
[197] | P. Pinto. A Rate of Metastability for the Halpern Type Proximal Point Algorithm. Numerical Functional Analysis and Optimization, 42(3):320--343, 2021. DOI. |
[198] | P. Pinto. Nonexpansive maps in nonlinear smooth spaces. Transactions of the American Mathematical Society, 377(9):6379--6426, 2024. DOI. |
[199] | P. Pinto. On the finitary content of Dykstra's cyclic projections algorithm. Zeitschrift für Analysis und ihre Anwendungen, 2024. To appear. DOI. |
[200] | P. Pinto. Proof mining and the convex feasibility problem: the curious case of Dykstra's algorithm. 2024. Manuscript available at https://www2.mathematik.tu-darmstadt.de/~pinto/. |
[201] | P. Pinto and N. Pischke. On computational properties of Cauchy problems generated by accretive operators. Documenta Mathematica, 28(5):1235--1274, 2023. DOI. |
[202] | P. Pinto and N. Pischke. On Dykstra's algorithm with Bregman projections. Oberwolfach Preprint 2024-04, 2024. DOI. |
[203] | P. Pinto and N. Pischke. On the Halpern method with adaptive anchoring parameters. 2024. DOI. |
[204] | P. Pinto and A. Sipoş. Products of hyperbolic spaces. arXiv preprint, arXiv:2408.14093, 2024. |
[205] | N. Pischke. A Proof-Theoretic Metatheorem for Nonlinear Semigroups generated by an Accretive Operator and Applications. arXiv preprint, arXiv:2304.01723, 2023. |
[206] | N. Pischke. On Korpelevich's Extragradient Algorithm. Zeitschrift für Analysis und ihre Anwendungen, 42(1/2):117--129, 2023. DOI. |
[207] | N. Pischke. Quantitative Results on Algorithms for Zeros of Differences of Monotone Operators in Hilbert Space. Journal of Convex Analysis, 30(1):295--315, 2023. |
[208] | N. Pischke. A proof-theoretic bound extraction theorem for monotone operators in Banach spaces. 2024. Manuscript available at https://nicholaspischke.github.io/. |
[209] | N. Pischke. Duality, Fréchet differentiability and Bregman distances in hyperbolic spaces. Israel Journal of Mathematics, 2024. To appear. |
[210] | N. Pischke. Generalized Fejér monotone sequences and their finitary content. Optimization, 2024. To appear. DOI. |
[211] | N. Pischke. Logical Metatheorems for Accretive and (Generalized) Monotone Set-Valued Operators. Journal of Mathematical Logic, 24(2), 2024. 2350008, 59pp., DOI. |
[212] | N. Pischke. On logical aspects of extensionality and continuity for set-valued operators with applications to nonlinear analysis. 2024. Manuscript available at https://nicholaspischke.github.io/. |
[213] | N. Pischke. On the proximal point algorithm for strongly quasiconvex functions in Hadamard spaces. arXiv preprint, arXiv:2411.06910, 2024. |
[214] | N. Pischke. Proof mining for the dual of a Banach space with extensions for uniformly Fréchet differentiable functions. Transactions of the American Mathematical Society, 377(10):7475--7517, 2024. DOI. |
[215] | N. Pischke. Rates of convergence for the asymptotic behavior of second-order Cauchy problems. Journal of Mathematical Analysis and Applications, 533(2), 2024. 128078, 15pp., DOI. |
[216] | N. Pischke and U. Kohlenbach. Quantitative analysis of a subgradient-type method for equilibrium problems. Numerical Algorithms, 90:197--219, 2022. DOI. |
[217] | N. Pischke and U. Kohlenbach. Effective rates for iterations involving Bregman strongly nonexpansive operators. Set-Valued and Variational Analysis, 32(4), 2024. 33, 58pp., DOI. |
[218] | N. Pischke and T. Powell. Asymptotic regularity of a generalised stochastic Halpern scheme with applications. arXiv preprint, arXiv:2411.04845, 2024. |
[219] | T. Powell. Applying Gödel's Dialectica interpretation to obtain a constructive proof of Higman's Lemma. In Proceedings of CL&C '12, pages 49--62, 2012. DOI. |
[220] | T. Powell. On Bar Recursive Interpretations of Analysis. PhD thesis, Queen Mary University of London, 2013. |
[221] | T. Powell. A new metastable convergence criterion and an application in the theory of uniformly convex Banach spaces. Journal of Mathematical Analysis and Applications, 478(2):790--805, 2019. DOI. |
[222] | T. Powell. A proof theoretic study of abstract termination principles. Journal of Logic and Computation, 29(8):1345--1366, 2019. DOI. |
[223] | T. Powell. A note on the finitization of Abelian and Tauberian theorems. Mathematical Logic Quarterly, 66(3):300--310, 2020. DOI. |
[224] | T. Powell. On the computational content of Zorn's lemma. In Proceedings of LICS '20, pages 768--781. ACM, 2020. DOI. |
[225] | T. Powell. A finitization of Littlewood's Tauberian theorem and an application in Tauberian remainder theory. Annals of Pure and Applied Logic, 174(4):103231, 2023. DOI. |
[226] | T. Powell. Proof mining and informal proof theoretic reasoning: A case study on greedy approximation schemes. 2024. Manuscript available at https://t-powell.github.io/publications.html. |
[227] | T. Powell and F. Wiesnet. Rates of convergence for asymptotically weakly contractive mappings in normed spaces. Numerical Functional Analysis and Optimization, 42(15):1802--1838, 2021. DOI. |
[228] | L. Pǎunescu and A. Sipoş. A proof-theoretic metatheorem for tracial von Neumann algebras. Mathematical Logic Quarterly, 69(1):63--76, 2023. DOI. |
[229] | P. Safarik. A quantitative nonlinear strong ergodic theorem for Hilbert spaces. Journal of Mathematical Analysis and Applications, 391:26--37, 2012. DOI. |
[230] | P. Safarik. On the extraction of computational content from noneffective convergence proofs in analysis. PhD thesis, TU Darmstadt, 2013. |
[231] | L. Sauras-Altuzarra. Some applications of Baaz's generalization method to the study of the factors of Fermat numbers. Journal of Logic and Computation, 34(6):1199--1209, 2024. DOI. |
[232] | K. Schade and U. Kohlenbach. Effective metastability for modified Halpern iterations in CAT(0) spaces. Fixed Point Theory and Applications, 191:19pp., 2012. DOI. |
[233] | W. Simmons and H. Towsner. Proof mining and effective bounds in differential polynomial rings. Advances in Mathematics, 343:567--623, 2019. DOI. |
[234] | W. Simmons and H. Towsner. Explicit polynomial bounds on prime ideals in polynomial rings over fields. Pacific Journal of Mathematics, 306(2):721--754, 2020. DOI. |
[235] | A. Sipoş. A note on the Mann iteration for k-strict pseudocontractions in Banach spaces. Numerical Functional Analysis and Optimization, 38(1):80--90, 2017. DOI. |
[236] | A. Sipoş. Contributions to proof mining. PhD thesis, Universitatea din Bucureşti, 2017. |
[237] | A. Sipoş. Effective results on a fixed point algorithm for families of nonlinear mappings. Annals of Pure and Applied Logic, 168(1):112--128, 2017. DOI. |
[238] | A. Sipoş. Proof mining in Lp-spaces. The Journal of Symbolic Logic, 84(4):1612--1629, 2019. DOI. |
[239] | A. Sipoş. The asymptotic behaviour of convex combinations of firmly nonexpansive mappings. Journal of Convex Analysis, 26(3):911--924, 2019. |
[240] | A. Sipoş. A quantitative multiparameter mean ergodic theorem. Pacific Journal of Mathematics, 314(1):209--218, 2021. DOI. |
[241] | A. Sipoş. Bounds on strong unicity for Chebyshev approximation with bounded coefficients. Mathematische Nachrichten, 294(12):2425--2440, 2021. DOI. |
[242] | A. Sipoş. Construction of fixed points of asymptotically nonexpansive mappings in uniformly convex hyperbolic spaces. Numerical Functional Analysis and Optimization, 42(6):696--711, 2021. DOI. |
[243] | A. Sipoş. Rates of metastability for iterations on the unit interval. Journal of Mathematical Analysis and Applications, 502(1):125235, 11pp., 2021. DOI. |
[244] | A. Sipoş. Abstract strongly convergent variants of the proximal point algorithm. Computational Optimization and Applications, 83(1):349--380, 2022. DOI. |
[245] | A. Sipoş. On extracting variable Herbrand disjunctions. Studia Logica, 110(4):1115--1134, 2022. DOI. |
[246] | A. Sipoş. Quantitative inconsistent feasibility for averaged mappings. Optimization Letters, 16(6):1915--1925, 2022. DOI. |
[247] | A. Sipoş. Revisiting jointly firmly nonexpansive families of mappings. Optimization, 71(13):3819--3834, 2022. DOI. |
[248] | A. Sipoş. The computational content of super strongly nonexpansive mappings and uniformly monotone operators. Israel Journal of Mathematics, 2023. To appear. |
[249] | A. Sipoş. On quantitative metastability for accretive operators. Zeitschrift für Analysis und ihre Anwendungen, 43(3/4):417--433, 2024. DOI. |
[250] | T. Tao. Soft analysis, hard analysis, and the finite convergence principle. In Structure and Randomness: Pages from Year One of a Mathematical Blog. AMS, 2008. |
[251] | H. Towsner. Metastability and the Furstenberg-Zimmer Tower II: Polynomial and Multidimensional Szemeredi's Theorem. arXiv preprint, arXiv:0909.5668, 2009. |
[252] | H. Towsner. Partial impredicativity in reverse mathematics. The Journal of Symbolic Logic, 78(2):459--488, 2013. DOI. |
[253] | H. Towsner. An Inverse Ackermannian Lower Bound on the Local Unconditionality Constant of the James Space. arXiv preprint, arXiv:1503.04745, 2015. |
[254] | H. Towsner. Towards an effective theory of absolutely continuous measures. In P. Cégielski, A. Enayat, and R. Kossak, editors, Studies in Weak Arithmetics. Vol. 3, volume 217 of CSLI Lecture Notes, pages 171--229. CSLI Publications, Stanford, CA, 2016. |
[255] | H. Towsner. From Saturated Embedding Tests to Explicit Algorithms. arXiv preprint, arXiv:2306.12239, 2023. |
[256] | H. Towsner. What do ultraproducts remember about the original structures? Journal of Logic and Computation, 34(1):125--160, 2024. DOI. |
[257] | J. Treusch and U. Kohlenbach. Rates of convergence for splitting algorithms. Israel Journal of Mathematics, 2024. To appear. |
[258] | A.S. Troelstra. Aspects of constructive mathematics. In J. Barwise, editor, Handbook of Mathematical Logic, pages 973--1052. North-Holland, Amsterdam, 1977. DOI. |
This file was generated by bibtex2html 1.99.