{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,15]],"date-time":"2025-10-15T00:24:34Z","timestamp":1760487874484,"version":"build-2065373602"},"reference-count":33,"publisher":"Springer Science and Business Media LLC","issue":"7-8","license":[{"start":{"date-parts":[[2025,5,14]],"date-time":"2025-05-14T00:00:00Z","timestamp":1747180800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,5,14]],"date-time":"2025-05-14T00:00:00Z","timestamp":1747180800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100005760","name":"University of Gothenburg","doi-asserted-by":"crossref","id":[{"id":"10.13039\/501100005760","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Arch. Math. Logic"],"published-print":{"date-parts":[[2025,11]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>This article provides a language-theoretic rendering of Herbrand\u2019s theorem. To each first-order proof is associated a higher-order recursion scheme that abstracts the computation of Herbrand sets obtained through Gentzen-style multicut elimination. The representation extends previous results in this area by lifting the prenex restriction on cut formulas and relaxing the cut-elimination strategies. Features of the new approach are the interpretation of cut as simple composition and contraction as \u2018call with current continuation\u2019.<\/jats:p>","DOI":"10.1007\/s00153-024-00959-w","type":"journal-article","created":{"date-parts":[[2025,5,14]],"date-time":"2025-05-14T15:01:06Z","timestamp":1747234866000},"page":"1007-1076","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Herbrand schemes for first-order logic"],"prefix":"10.1007","volume":"64","author":[{"given":"Bahareh","family":"Afshari","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sebastian","family":"Enqvist","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Graham E.","family":"Leigh","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2025,5,14]]},"reference":[{"issue":"5","key":"959_CR1","doi-asserted-by":"publisher","first-page":"633","DOI":"10.1007\/s00153-005-0275-1","volume":"44","author":"P Gerhardy","year":"2005","unstructured":"Gerhardy, P., Kohlenbach, U.: Extracting Herbrand disjunctions by functional interpretation. Arch. Math. Log. 44(5), 633\u2013644 (2005). https:\/\/doi.org\/10.1007\/s00153-005-0275-1","journal-title":"Arch. Math. Log."},{"issue":"11","key":"959_CR2","doi-asserted-by":"publisher","first-page":"1346","DOI":"10.1016\/j.apal.2010.04.006","volume":"161","author":"W Heijltjes","year":"2010","unstructured":"Heijltjes, W.: Classical proof forestry. Annals of Pure and Applied Logic 161(11), 1346\u20131366 (2010)","journal-title":"Annals of Pure and Applied Logic"},{"issue":"1","key":"959_CR3","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/2422085.2422090","volume":"14","author":"R McKinley","year":"2013","unstructured":"McKinley, R.: Proof nets for Herbrand\u2019s theorem. ACM Transactions on Computational Logic (TOCL) 14(1), 1\u201331 (2013)","journal-title":"ACM Transactions on Computational Logic (TOCL)"},{"key":"959_CR4","doi-asserted-by":"publisher","first-page":"347","DOI":"10.1007\/BF00370646","volume":"46","author":"DA Miller","year":"1987","unstructured":"Miller, D.A.: A compact representation of proofs. Studia Logica 46, 347\u2013370 (1987)","journal-title":"Studia Logica"},{"issue":"8","key":"959_CR5","doi-asserted-by":"publisher","first-page":"1009","DOI":"10.1017\/S0960129519000069","volume":"29","author":"F Aschieri","year":"2019","unstructured":"Aschieri, F., Hetzl, S., Weller, D.: Expansion trees with cut. Mathematical Structures in Computer Science 29(8), 1009\u20131029 (2019)","journal-title":"Mathematical Structures in Computer Science"},{"key":"959_CR6","doi-asserted-by":"publisher","unstructured":"Afshari, B., Hetzl, S., Leigh, G.E.: Herbrand\u2019s theorem as higher order recursion. Ann. Pure Appl. Log. 171(6) (2020) https:\/\/doi.org\/10.1016\/j.apal.2020.102792","DOI":"10.1016\/j.apal.2020.102792"},{"key":"959_CR7","doi-asserted-by":"publisher","unstructured":"Hetzl, S.: Applying tree languages in proof theory. In: Dediu, A., Mart\u00edn-Vide, C. (eds.) Language and Automata Theory and Applications - 6th International Conference, LATA 2012, Proceedings. Lecture Notes in Computer Science, vol. 7183, pp. 301\u2013312. Springer, Berlin (2012). https:\/\/doi.org\/10.1007\/978-3-642-28332-1_26","DOI":"10.1007\/978-3-642-28332-1_26"},{"key":"959_CR8","doi-asserted-by":"publisher","unstructured":"Afshari, B., Hetzl, S., Leigh, G.E.: Herbrand disjunctions, cut elimination and context-free tree grammars. In: Altenkirch, T. (ed.) 13th International Conference on Typed Lambda Calculi and Applications, TLCA 2015, July 1-3, 2015, Warsaw, Poland. LIPIcs, vol. 38, pp. 1\u201316. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, Dagstuhl (2015). https:\/\/doi.org\/10.4230\/LIPIcs.TLCA.2015.1","DOI":"10.4230\/LIPIcs.TLCA.2015.1"},{"key":"959_CR9","doi-asserted-by":"crossref","unstructured":"Constable, R., Murthy, C.: Finding computational content in classical proofs, pp. 341\u2013362. Cambridge University Press, USA (1991)","DOI":"10.1017\/CBO9780511569807.014"},{"key":"959_CR10","doi-asserted-by":"publisher","unstructured":"Downen, P., Ariola, Z.M.: A tutorial on computational classical logic and the sequent calculus. Journal of Functional Programming 28, 3 (2018) https:\/\/doi.org\/10.1017\/S0956796818000023","DOI":"10.1017\/S0956796818000023"},{"key":"959_CR11","doi-asserted-by":"publisher","unstructured":"Coquand, T.: Computational content of classical logic. In: Pitts, A.M., Dybjer, P.E. (eds.) Semantics and Logics of Computation. Publications of the Newton Institute, pp. 33\u201378. Cambridge University Press, Cambridge (1997). https:\/\/doi.org\/10.1017\/CBO9780511526619.003","DOI":"10.1017\/CBO9780511526619.003"},{"key":"959_CR12","doi-asserted-by":"publisher","unstructured":"Powell, T.: Computational interpretations of classical reasoning: From the epsilon calculus to stateful programs. In: Centrone, S., Negri, S., Sarikaya, D., Schuster, P.M. (eds.) Mathesis Universalis, Computability and Proof, pp. 255\u2013290. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-20447-1_14","DOI":"10.1007\/978-3-030-20447-1_14"},{"key":"959_CR13","volume-title":"Applied Proof Theory: Proof Interpretations and Their Use in Mathematics","author":"U Kohlenbach","year":"2008","unstructured":"Kohlenbach, U.: Applied Proof Theory: Proof Interpretations and Their Use in Mathematics. Springer monographs in mathematics. Springer, Berlin (2008)"},{"issue":"4","key":"959_CR14","first-page":"241","volume":"16","author":"G Kreisel","year":"1951","unstructured":"Kreisel, G.: On the interpretation of non-finitist proofs-part i. The Journal of Symbolic Logic 16(4), 241\u2013267 (1951)","journal-title":"The Journal of Symbolic Logic"},{"key":"959_CR15","doi-asserted-by":"publisher","unstructured":"Shoenfield, J.R.: Mathematical Logic. A K Peters\/CRC Press, New York (2018).https:\/\/doi.org\/10.1201\/9780203749456","DOI":"10.1201\/9780203749456"},{"issue":"5","key":"959_CR16","doi-asserted-by":"publisher","first-page":"523","DOI":"10.1007\/s00153-017-0555-6","volume":"56","author":"F Ferreira","year":"2017","unstructured":"Ferreira, F., Ferreira, G.: A herbrandized functional interpretation of classical first-order logic. Archive for Mathematical Logic 56(5), 523\u2013539 (2017). https:\/\/doi.org\/10.1007\/s00153-017-0555-6","journal-title":"Archive for Mathematical Logic"},{"issue":"15","key":"959_CR17","first-page":"183","volume":"5","author":"VI Glivenko","year":"1929","unstructured":"Glivenko, V.I.: Sur quelque points de la logique de M Brouwer. Acad\u00e9mie Royale de Belgique, Bulletin de la Classe des Sciences 5(15), 183\u2013188 (1929)","journal-title":"Acad\u00e9mie Royale de Belgique, Bulletin de la Classe des Sciences"},{"key":"959_CR18","doi-asserted-by":"publisher","unstructured":"G\u00f6del, K.: On intuitionistic arithmetic and number theory. In: Feferman, S., Dawson, J.W., Kleene, S.C., Moore, G.H., Heijenoort, J. (eds.) Collected Works I: Publications 1929\u20131936 vol. I. Oxford University Press, New York (1986). https:\/\/doi.org\/10.1093\/oso\/9780195147209.001.0001","DOI":"10.1093\/oso\/9780195147209.001.0001"},{"key":"959_CR19","doi-asserted-by":"publisher","unstructured":"Friedman, H.: Classically and intuitionistically provably recursive functions. In: M\u00fcller, G.H., Scott, D.S. (eds.) Higher Set Theory, pp. 21\u201327. Springer, Berlin, Heidelberg (1978). https:\/\/doi.org\/10.1007\/BFb0103100","DOI":"10.1007\/BFb0103100"},{"key":"959_CR20","unstructured":"Krivine, J.-L.: Realizability in classical logic. Panoramas & Synth\u00e9ses, 199\u2013231 (2009)"},{"issue":"2","key":"959_CR21","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1016\/0304-3975(75)90017-1","volume":"1","author":"GD Plotkin","year":"1975","unstructured":"Plotkin, G.D.: Call-by-name, call-by-value and the $$\\lambda $$-calculus. Theoretical Computer Science 1(2), 125\u2013159 (1975). https:\/\/doi.org\/10.1016\/0304-3975(75)90017-1","journal-title":"Theoretical Computer Science"},{"key":"959_CR22","volume-title":"The Stanford Encyclopedia of Philosophy, Fall","author":"J Avigad","year":"2020","unstructured":"Avigad, J., Zach, R.: The Epsilon Calculus. In: Zalta, E.N. (ed.) The Stanford Encyclopedia of Philosophy, Fall, 2020th edn. Stanford Univesity, Metaphysics Research Lab (2020)","edition":"2020"},{"key":"959_CR23","doi-asserted-by":"publisher","unstructured":"Fortier, J., Santocanale, L.: Cuts for circular proofs: semantics and cut-elimination. In: Rocca, S.R.D. (ed.) Computer Science Logic 2013 (CSL 2013), CSL 2013, September 2-5, 2013, Torino, Italy. LIPIcs, vol. 23, pp. 248\u2013262. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, (2013). https:\/\/doi.org\/10.4230\/LIPICS.CSL.2013.248","DOI":"10.4230\/LIPICS.CSL.2013.248"},{"key":"959_CR24","unstructured":"Baelde, D., Doumane, A., Saurin, A.: Infinitary proof theory: the multiplicative additive case. Computer Science Logic 2016 (2016)"},{"key":"959_CR25","doi-asserted-by":"crossref","unstructured":"Baelde, D., Doumane, A., Kuperberg, D., Saurin, A.: Bouncing threads for circular and non-wellfounded proofs: Towards compositionality with circular proofs. In: Proceedings of the 37th Annual ACM\/IEEE Symposium on Logic in Computer Science, pp. 1\u201313 (2022)","DOI":"10.1145\/3531130.3533375"},{"key":"959_CR26","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1007\/978-3-031-43513-3_12","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"A Saurin","year":"2023","unstructured":"Saurin, A.: A linear perspective on cut-elimination for non-wellfounded sequent calculi with least and greatest fixed-points. In: Ramanayake, R., Urban, J. (eds.) Automated Reasoning with Analytic Tableaux and Related Methods, pp. 203\u2013222. Springer, Cham (2023)"},{"key":"959_CR27","unstructured":"Alcolei, A., Clairambault, P., Hyland, M., Winskel, G.: The true concurrency of Herbrand\u2019s theorem. In: 27th EACSL Annual Conference on Computer Science Logic (CSL 2018) (2018). Schloss-Dagstuhl-Leibniz Zentrum f\u00fcr Informatik"},{"key":"959_CR28","doi-asserted-by":"publisher","unstructured":"Troelstra, A.S., Schwichtenberg, H.: Basic Proof Theory, 2nd edn. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, Cambridge (2000). https:\/\/doi.org\/10.1017\/CBO9781139168717","DOI":"10.1017\/CBO9781139168717"},{"key":"959_CR29","doi-asserted-by":"crossref","unstructured":"Hague, M., Murawski, A.S., Ong, C.-H., Serre, O.: Collapsible pushdown automata and recursion schemes. In: 2008 23rd Annual IEEE Symposium on Logic in Computer Science, pp. 452\u2013461 (2008)","DOI":"10.1109\/LICS.2008.34"},{"key":"959_CR30","doi-asserted-by":"publisher","unstructured":"Simpson, A.: Cyclic Arithmetic Is Equivalent to Peano Arithmetic. In: Esparza, J., Murawski, A.S. (eds.) Foundations of Software Science and Computation Structures vol. 10203, pp. 283\u2013300. Springer, Berlin, Heidelberg (2017). https:\/\/doi.org\/10.1007\/978-3-662-54458-7_17 . Series Title: Lecture Notes in Computer Science. https:\/\/link.springer.com\/10.1007\/978-3-662-54458-7_17 Accessed 2024-06-09","DOI":"10.1007\/978-3-662-54458-7_17"},{"key":"959_CR31","doi-asserted-by":"publisher","unstructured":"Curzi, G., Das, A.: Computational expressivity of (circular) proofs with fixed points. In: 2023 38th Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS), pp. 1\u201313. IEEE, Boston, MA, USA (2023).https:\/\/doi.org\/10.1109\/lics56636.2023.10175772 . https:\/\/ieeexplore.ieee.org\/document\/10175772\/ Accessed 2025-01-14","DOI":"10.1109\/lics56636.2023.10175772"},{"key":"959_CR32","unstructured":"Afshari, B., Enqvist, S., Leigh, G.E.: Herbrand schemes for cyclic proofs. Journal of Logic and Computation (To appear)"},{"key":"959_CR33","doi-asserted-by":"publisher","unstructured":"Brotherston, J., Simpson, A.: Complete Sequent Calculi for Induction and Infinite Descent. In: 22nd Annual IEEE Symposium on Logic in Computer Science (LICS 2007), pp. 51\u201362. IEEE, Wroclaw, Poland (2007). https:\/\/doi.org\/10.1109\/LICS.2007.16 . http:\/\/ieeexplore.ieee.org\/document\/4276551\/ Accessed 2024-06-09","DOI":"10.1109\/LICS.2007.16"}],"container-title":["Archive for Mathematical Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s00153-024-00959-w.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s00153-024-00959-w\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s00153-024-00959-w.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,14]],"date-time":"2025-10-14T06:06:55Z","timestamp":1760422015000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s00153-024-00959-w"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,5,14]]},"references-count":33,"journal-issue":{"issue":"7-8","published-print":{"date-parts":[[2025,11]]}},"alternative-id":["959"],"URL":"https:\/\/doi.org\/10.1007\/s00153-024-00959-w","relation":{},"ISSN":["0933-5846","1432-0665"],"issn-type":[{"type":"print","value":"0933-5846"},{"type":"electronic","value":"1432-0665"}],"subject":[],"published":{"date-parts":[[2025,5,14]]},"assertion":[{"value":"14 October 2023","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"17 December 2024","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"14 May 2025","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}