{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,1,30]],"date-time":"2024-01-30T21:10:32Z","timestamp":1706649032502},"reference-count":18,"publisher":"Duke University Press","issue":"3","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Notre Dame J. Formal Logic"],"published-print":{"date-parts":[[2012,1,1]]},"DOI":"10.1215\/00294527-1716811","type":"journal-article","created":{"date-parts":[[2012,9,24]],"date-time":"2012-09-24T23:30:27Z","timestamp":1348529427000},"source":"Crossref","is-referenced-by-count":2,"title":["The Computational Content of Arithmetical Proofs"],"prefix":"10.1215","volume":"53","author":[{"given":"Stefan","family":"Hetzl","sequence":"first","affiliation":[]}],"member":"73","reference":[{"key":"1","doi-asserted-by":"publisher","unstructured":"[1] Ackermann, W., \u201cZur Widerspruchsfreiheit der Zahlentheorie,\u201d <i>Mathematische Annalen<\/i>, vol. 117 (1940), pp. 162\u2013194.","DOI":"10.1007\/BF01450016"},{"key":"2","unstructured":"[2] Avigad, J., \u201cThe computational content of classical arithmetic,\u201d pp. 15\u201330 in <i>Proofs, Categories, and Computations: Essays in Honor of Grigori Mints<\/i>, edited by F. Solomon and S. Wilfried, vol. 13 of <i>Tributes<\/i>, College Publications, London, 2010."},{"key":"3","doi-asserted-by":"publisher","unstructured":"[3] Baaz, M., and S. Hetzl, \u201cOn the non-confluence of cut-elimination,\u201d <i>Journal of Symbolic Logic<\/i>, vol. 76 (2011), pp. 313\u2013340.","DOI":"10.2178\/jsl\/1294171002"},{"key":"4","doi-asserted-by":"publisher","unstructured":"[4] Baaz, M., S. Hetzl, A. Leitsch, C. Richter, and H. Spohr, \u201cCut-elimination: Experiments with CERES,\u201d pp. 481\u2013495 in <i>Logic for Programming, Artificial Intelligence, and Reasoning<\/i>, edited by F. Baader and A. Voronkov, vol. 3452 of <i>Lecture Notes in Computer Science<\/i>, Springer, Berlin, 2005.","DOI":"10.1007\/978-3-540-32275-7_32"},{"key":"5","doi-asserted-by":"crossref","unstructured":"[5] Friedman, H., \u201cClassically and intuitionistically provable recursive functions,\u201d pp. 21\u201327 in <i>Higher Set Theory (Oberwolfach, 1977)<\/i>, edited by G. H. M\u00fcller and D. S. Scott, vol. 669 of <i>Lecture Notes in Mathematics<\/i>, Springer, Berlin, 1978.","DOI":"10.1007\/BFb0103100"},{"key":"6","doi-asserted-by":"crossref","unstructured":"[6] Gentzen, G., \u201cUntersuchungen \u00fcber das logische Schlie\u00dfen, I,\u201d <i>Mathematische Zeitschrift<\/i>, vol. 39 (1935), pp. 176\u2013210; \u201cII,\u201d pp. 405\u2013431.","DOI":"10.1007\/BF01201363"},{"key":"7","doi-asserted-by":"publisher","unstructured":"[7] Gentzen, G., \u201cDie Widerspruchsfreiheit der reinen Zahlentheorie,\u201d <i>Mathematische Annalen<\/i>, vol. 112 (1936), pp. 493\u2013565.","DOI":"10.1007\/BF01565428"},{"key":"8","unstructured":"[8] Girard, J.-Y., \u201cInterpr\u00e9tation fonctionelle et \u00e9limination des coupures de l\u2019arithm\u00e9tique d\u2019ordre sup\u00e9rieur,\u201d Ph.D. thesis, Universit\u00e9 Paris 7, 1972."},{"key":"9","doi-asserted-by":"publisher","unstructured":"[9] G\u00f6del, K., \u201c\u00dcber eine bisher noch nicht ben\u00fctzte Erweiterung des finiten Standpunktes,\u201d <i>Dialectica<\/i>, vol. 12 (1958), pp. 280\u2013287.","DOI":"10.1111\/j.1746-8361.1958.tb01464.x"},{"key":"10","unstructured":"[10] H\u00e1jek, P., and P. Pudl\u00e1k, <i>Metamathematics of First-Order Arithmetic<\/i>, Perspectives in Mathematical Logic, Springer-Verlag, Berlin, 1998."},{"key":"11","doi-asserted-by":"publisher","unstructured":"[11] Kleene, S. C., \u201cOn the interpretation of intuitionistic number theory,\u201d <i>Journal of Symbolic Logic<\/i>, vol. 10 (1945), pp. 109\u2013124.","DOI":"10.2307\/2269016"},{"key":"12","unstructured":"[12] Kohlenbach, U., <i>Applied Proof Theory: Proof Interpretations and Their Use in Mathematics<\/i>, Springer Monographs in Mathematics, Springer, Berlin, 2008."},{"key":"13","doi-asserted-by":"publisher","unstructured":"[13] Kraj\u00ed\u010dek, J., \u201cInterpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic,\u201d <i>Journal of Symbolic Logic<\/i>, vol. 62 (1997), pp. 457\u2013486.","DOI":"10.2307\/2275541"},{"key":"14","doi-asserted-by":"publisher","unstructured":"[14] Kreisel, G., \u201cOn the interpretation of non-finitist proofs, II: Interpretation of number theory,\u201d <i>Journal of Symbolic Logic<\/i>, vol. 17 (1952), pp. 43\u201358.","DOI":"10.2307\/2267457"},{"key":"15","doi-asserted-by":"crossref","unstructured":"[15] Kreisel, G., \u201cFiniteness theorems in arithmetic: An application of Herbrand\u2019s theorem for $\\Sigma_{2}$-formulas,\u201d pp. 39\u201355, in <i>Logic Colloquium \u201981<\/i> (<i>Marseilles, 1981<\/i>), edited by J. Stern, vol. 107 of <i>Studies in Logic and the Foundations of Mathematics<\/i>, North-Holland, Amsterdam, 1982.","DOI":"10.1016\/S0049-237X(08)71876-7"},{"key":"16","doi-asserted-by":"publisher","unstructured":"[16] Parigot, M., \u201c$\\lambda\\mu$-Calculus: An algorithmic interpretation of classical natural deduction,\u201d pp. 190\u2013201, in <i>Logic Programming and Automated Reasoning (St. Petersburg, 1992)<\/i>, vol. 624 in <i>Lecture Notes in Computer Science<\/i>, Springer, Berlin, 1992.","DOI":"10.1007\/BFb0013061"},{"key":"17","doi-asserted-by":"publisher","unstructured":"[17] Ratiu, D., and T. Trifonov, \u201cExploring the computational content of the infinite pigeonhole principle,\u201d <i>Journal of Logic and Computation<\/i>, vol. 22 (2012), 329\u2013350.","DOI":"10.1093\/logcom\/exq011"},{"key":"18","unstructured":"[18] Urban, C., and G. Bierman, \u201cStrong normalisation of cut-elimination in classical logic,\u201d <i>Fundamenta Informaticae<\/i>, vol. 45 (2000), pp. 123\u2013155."}],"container-title":["Notre Dame Journal of Formal Logic"],"original-title":[],"link":[{"URL":"https:\/\/projecteuclid.org\/journalArticle\/Download?urlid=10.1215\/00294527-1716811","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,1,30]],"date-time":"2024-01-30T20:57:55Z","timestamp":1706648275000},"score":1,"resource":{"primary":{"URL":"https:\/\/projecteuclid.org\/journals\/notre-dame-journal-of-formal-logic\/volume-53\/issue-3\/The-Computational-Content-of-Arithmetical-Proofs\/10.1215\/00294527-1716811.full"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,1,1]]},"references-count":18,"journal-issue":{"issue":"3","published-online":{"date-parts":[[2012,1,1]]}},"URL":"https:\/\/doi.org\/10.1215\/00294527-1716811","relation":{},"ISSN":["0029-4527"],"issn-type":[{"value":"0029-4527","type":"print"}],"subject":[],"published":{"date-parts":[[2012,1,1]]}}}