{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,27]],"date-time":"2025-09-27T06:40:15Z","timestamp":1758955215539,"version":"3.44.0"},"reference-count":28,"publisher":"Springer Science and Business Media LLC","issue":"3-4","license":[{"start":{"date-parts":[[2025,9,11]],"date-time":"2025-09-11T00:00:00Z","timestamp":1757548800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,9,11]],"date-time":"2025-09-11T00:00:00Z","timestamp":1757548800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J of Log Lang and Inf"],"published-print":{"date-parts":[[2025,10]]},"DOI":"10.1007\/s10849-025-09435-x","type":"journal-article","created":{"date-parts":[[2025,9,11]],"date-time":"2025-09-11T01:30:13Z","timestamp":1757554213000},"page":"273-317","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Sequent Images of Normal Derivations and Natural Deduction Images of Derivations without M-cuts"],"prefix":"10.1007","volume":"34","author":[{"given":"Mirjana","family":"Borisavljevi\u0107","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2025,9,11]]},"reference":[{"key":"9435_CR1","unstructured":"Borisavljevi\u0107, M. (1997). Sequents, natural deduction and multicategories, Ph. D. thesis, University of Belgrade (in Serbian)."},{"issue":"6","key":"9435_CR2","doi-asserted-by":"publisher","first-page":"769","DOI":"10.1093\/logcom\/14.6.769","volume":"14","author":"M Borisavljevi\u0107","year":"2004","unstructured":"Borisavljevi\u0107, M. (2004). Extended natural-deduction images of conversions from the system of sequents. Journal of Logic and Computation, 14(6), 769\u2013799.","journal-title":"Journal of Logic and Computation"},{"issue":"2","key":"9435_CR3","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1007\/s00153-005-0295-x","volume":"45","author":"M Borisavljevi\u0107","year":"2006","unstructured":"Borisavljevi\u0107, M. (2006). A connection between cut elimination and normalization. Archive for Mathematical Logic, 45(2), 113\u2013148.","journal-title":"Archive for Mathematical Logic"},{"key":"9435_CR4","unstructured":"Borisavljevi\u0107, M. (2006a). Maximum segments and cuts. Proceedings of the 6th Panhellenic Logic Symposium, July 25-28, 2005, University of Athens, Greece, 40-48."},{"issue":"6","key":"9435_CR5","doi-asserted-by":"publisher","first-page":"521","DOI":"10.1007\/s10992-008-9084-4","volume":"37","author":"M Borisavljevi\u0107","year":"2008","unstructured":"Borisavljevi\u0107, M. (2008). Normal derivations and sequent derivations. Journal of Philosophical Logic, 37(6), 521\u2013548.","journal-title":"Journal of Philosophical Logic"},{"issue":"2","key":"9435_CR6","doi-asserted-by":"publisher","first-page":"347","DOI":"10.1017\/S1755020318000102","volume":"11","author":"M Borisavljevi\u0107","year":"2018","unstructured":"Borisavljevi\u0107, M. (2018). An analysis of the rules of Gentzen\u2019s $$LJ$$ and $$NJ$$. Review of Symbolic Logic, 11(2), 347\u2013370.","journal-title":"Review of Symbolic Logic"},{"issue":"5","key":"9435_CR7","doi-asserted-by":"publisher","first-page":"739","DOI":"10.1093\/jigpal\/jzaa017","volume":"29","author":"M Borisavljevi\u0107","year":"2021","unstructured":"Borisavljevi\u0107, M. (2021). The subformula property of natural deduction derivations and analytic cuts. Logic Journal of the IGPL, 29(5), 739\u2013768.","journal-title":"Logic Journal of the IGPL"},{"issue":"3","key":"9435_CR8","doi-asserted-by":"publisher","first-page":"499","DOI":"10.1007\/s11787-022-00309-5","volume":"16","author":"M Borisavljevi\u0107","year":"2022","unstructured":"Borisavljevi\u0107, M. (2022). Maximum segments as natural deduction images of some cuts. Logica Universalis, 16(3), 499\u2013533.","journal-title":"Logica Universalis"},{"key":"9435_CR9","doi-asserted-by":"publisher","first-page":"75","DOI":"10.1016\/0168-0072(91)90059-U","volume":"53","author":"SR Buss","year":"1991","unstructured":"Buss, S. R. (1991). The undecidability of k-provability. Annals of Pure and Applied Logic, 53, 75\u2013102.","journal-title":"Annals of Pure and Applied Logic"},{"key":"9435_CR10","doi-asserted-by":"publisher","first-page":"249","DOI":"10.1016\/S0168-0072(96)00019-X","volume":"83","author":"A Carbone","year":"1997","unstructured":"Carbone, A. (1997). Interpolants, Cut Elimination and Flow Graphs for the Propositional Calculus. Annals of Pure and Applied Logic, 83, 249\u2013299.","journal-title":"Annals of Pure and Applied Logic"},{"issue":"6","key":"9435_CR11","doi-asserted-by":"publisher","first-page":"733","DOI":"10.1093\/jigpal\/8.6.733","volume":"8","author":"C Cellucci","year":"2000","unstructured":"Cellucci, C. (2000). Analytic cut trees. Logic Journal of the IGPL, 8(6), 733\u2013750.","journal-title":"Logic Journal of the IGPL"},{"key":"9435_CR12","doi-asserted-by":"crossref","unstructured":"Dyckhoff, R. (2015). Cut elimination, substitution and normalisation. In Wansing, H.(ed.)Dag Prawitz on Proofs and Meaning, Springer, 163\u2013187.","DOI":"10.1007\/978-3-319-11041-7_7"},{"key":"9435_CR13","doi-asserted-by":"crossref","unstructured":"Gentzen, G. (1935). Untersuchungen \u00fcber das logische Schlie\u00dfen. Mathematische Zeitschrift 39 176-210, 405\u2013431 (English trans. in [Gentzen 1969]).","DOI":"10.1007\/BF01201363"},{"key":"9435_CR14","unstructured":"Gentzen, G. (1969). The Collected Papers of Gerhard Gentzen, Szabo, M.E. (ed.), North-Holland."},{"key":"9435_CR15","doi-asserted-by":"publisher","first-page":"259","DOI":"10.1017\/S175502031600040X","volume":"10","author":"T Kowalski","year":"2017","unstructured":"Kowalski, T., & Ono, H. (2017). Analytic cut and interpolation for bi-intuitionistic logic. Review of Symbolic Logic, 10, 259\u2013283.","journal-title":"Review of Symbolic Logic"},{"key":"9435_CR16","unstructured":"Minc, G. E. (1996). Normal forms for sequent derivations. In Odifreddi, P. (ed.) Kreiseliana: About and Around Georg Kreisel, Peters 469-492."},{"key":"9435_CR17","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511527340","volume-title":"Structural Proof Theory","author":"S Negri","year":"2001","unstructured":"Negri, S., & von Plato, J. (2001). Structural Proof Theory. New York: Cambridge University Press."},{"issue":"4","key":"9435_CR18","doi-asserted-by":"publisher","first-page":"1803","DOI":"10.2307\/2694976","volume":"66","author":"S Negri","year":"2001","unstructured":"Negri, S., & von Plato, J. (2001). Sequent calculus in natural deduction style. The Journal of Symbolic Logic, 66(4), 1803\u20131816.","journal-title":"The Journal of Symbolic Logic"},{"issue":"5","key":"9435_CR19","doi-asserted-by":"publisher","first-page":"435","DOI":"10.1002\/malq.200310047","volume":"49","author":"S Negri","year":"2003","unstructured":"Negri, S., & von Plato, J. (2003). Translations from natural deduction to sequent calculus. Mathematical Logic Quarterly, 49(5), 435\u2013443.","journal-title":"Mathematical Logic Quarterly"},{"issue":"1","key":"9435_CR20","doi-asserted-by":"publisher","first-page":"541","DOI":"10.1007\/s001530100091","volume":"40","author":"J von Plato","year":"2001","unstructured":"von Plato, J. (2001). Natural deduction with general elimination rules. Archive for Mathematical Logic, 40(1), 541\u2013567.","journal-title":"Archive for Mathematical Logic"},{"issue":"2","key":"9435_CR21","doi-asserted-by":"publisher","first-page":"240","DOI":"10.2178\/bsl\/1208442829","volume":"14","author":"J von Plato","year":"2008","unstructured":"von Plato, J. (2008). Gentzen\u2019s proof of normalization for natural deduction. The Bulletin of Symbolic Logic, 14(2), 240\u2013257.","journal-title":"The Bulletin of Symbolic Logic"},{"key":"9435_CR22","doi-asserted-by":"crossref","unstructured":"von Plato, J. (2011). \u201cA sequent calculus isomorphic to Gentzen\u2019s natural deduction. Review of Symbolic Logic,4(1), 43\u201353.","DOI":"10.1017\/S1755020310000195"},{"key":"9435_CR23","first-page":"323","volume":"12","author":"G Pottinger","year":"1977","unstructured":"Pottinger, G. (1977). Normalization as a homomorphic image of cut elimination. Annals of Pure and Applied Logic, 12, 323\u2013357.","journal-title":"Annals of Pure and Applied Logic"},{"key":"9435_CR24","volume-title":"Natural Deduction","author":"D Prawitz","year":"1965","unstructured":"Prawitz, D. (1965). Natural Deduction. Stockholm: Almquist and Wiksell."},{"issue":"4","key":"9435_CR25","doi-asserted-by":"publisher","first-page":"1284","DOI":"10.2307\/2274279","volume":"49","author":"P Schroeder-Heister","year":"1984","unstructured":"Schroeder-Heister, P. (1984). A natural extension of natural deduction. The Journal of Symbolic Logic, 49(4), 1284\u20131300.","journal-title":"The Journal of Symbolic Logic"},{"key":"9435_CR26","volume-title":"Basic proof Theory","author":"AS Troelstra","year":"1996","unstructured":"Troelstra, A. S., & Schwichtenberg, H. (1996). Basic proof Theory. New York: Cambridge University Press."},{"key":"9435_CR27","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1007\/978-94-007-7548-0_2","volume-title":"Advances in Natural Deduction","author":"C Urban","year":"2014","unstructured":"Urban, C. (2014). Revisiting Zucker\u2019s Work on the Correspondence Between Cut-Elimination and Normalisation. In L. C. Pereira, E. H. Edward, & V. de Paiva (Eds.), Advances in Natural Deduction (pp. 31\u201350). A Celebration of Dag Prawitz\u2019s Work: Springer."},{"key":"9435_CR28","first-page":"1","volume":"7","author":"J Zucker","year":"1974","unstructured":"Zucker, J. (1974). The correspondence between cut-elimination and normalization. Annals of Pure and Applied Logic, 7, 1\u2013112.","journal-title":"Annals of Pure and Applied Logic"}],"container-title":["Journal of Logic, Language and Information"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10849-025-09435-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10849-025-09435-x\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10849-025-09435-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,9,27]],"date-time":"2025-09-27T06:12:13Z","timestamp":1758953533000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10849-025-09435-x"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,9,11]]},"references-count":28,"journal-issue":{"issue":"3-4","published-print":{"date-parts":[[2025,10]]}},"alternative-id":["9435"],"URL":"https:\/\/doi.org\/10.1007\/s10849-025-09435-x","relation":{},"ISSN":["0925-8531","1572-9583"],"issn-type":[{"type":"print","value":"0925-8531"},{"type":"electronic","value":"1572-9583"}],"subject":[],"published":{"date-parts":[[2025,9,11]]},"assertion":[{"value":"14 May 2025","order":1,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"11 September 2025","order":2,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}