{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,12,3]],"date-time":"2023-12-03T02:40:02Z","timestamp":1701571202943},"reference-count":32,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2022,12,15]],"date-time":"2022-12-15T00:00:00Z","timestamp":1671062400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2022,12,15]],"date-time":"2022-12-15T00:00:00Z","timestamp":1671062400000},"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":["Stud Logica"],"published-print":{"date-parts":[[2023,6]]},"DOI":"10.1007\/s11225-022-10023-4","type":"journal-article","created":{"date-parts":[[2022,12,15]],"date-time":"2022-12-15T11:04:03Z","timestamp":1671102243000},"page":"391-429","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["The Elimination of Maximum Cuts in Linear Logic and BCK Logic"],"prefix":"10.1007","volume":"111","author":[{"given":"Mirjana","family":"Borisavljevic","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2022,12,15]]},"reference":[{"key":"10023_CR1","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1016\/S0168-0072(98)00062-1","volume":"99","author":"M Borisavljevi\u0107","year":"1999","unstructured":"Borisavljevi\u0107, M., A cut-elimination proof in intuitionistic predicate logic, Annals of Pure and Applied Logic 99: 105\u2013136, 1999.","journal-title":"Annals of Pure and Applied Logic"},{"key":"10023_CR2","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1017\/S0960129599003011","volume":"10","author":"M Borisavljevi\u0107","year":"2000","unstructured":"Borisavljevi\u0107, M., K. Do\u0161en, and Z. Petri\u0107, On permuting cut with contraction, Mathematical Structures in Computer Science 10: 99\u2013136, 2000.","journal-title":"Mathematical Structures in Computer Science"},{"key":"10023_CR3","doi-asserted-by":"publisher","first-page":"371","DOI":"10.1007\/s00153-002-0155-x","volume":"42","author":"M Borisavljevi\u0107","year":"2003","unstructured":"Borisavljevi\u0107, M., Two mesuares for proving Gentzen\u2019s Hauptsatz without mix, Archive for Mathematical Logic 42: 371\u2013387, 2003.","journal-title":"Archive for Mathematical Logic"},{"issue":"2","key":"10023_CR4","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., A connection between cut elimination and normalization, Archive for Mathematical Logic 45(2): 113\u2013148, 2006.","journal-title":"Archive for Mathematical Logic"},{"key":"10023_CR5","unstructured":"Borisavljevi\u0107, M., Maximum segments and cuts, in Proceedings of the 6th Panhellenic Logic Symposium, July 25\u201328 2005, University of Athens, Greece, 2006, pp. 40\u201348."},{"issue":"6","key":"10023_CR6","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., Normal derivations and sequent derivations, Journal of Philosophical Logic 37(6): 521\u2013548, 2008.","journal-title":"Journal of Philosophical Logic"},{"issue":"2","key":"10023_CR7","doi-asserted-by":"publisher","first-page":"347","DOI":"10.1017\/S1755020318000102","volume":"11","author":"M Borisavljevi\u0107","year":"2018","unstructured":"Borisavljevi\u0107, M., An analysis of the rules of Gentzen\u2019s $$LJ$$ and $$NJ$$, Review of Symbolic Logic 11(2): 347\u2013370, 2018.","journal-title":"Review of Symbolic Logic"},{"issue":"5","key":"10023_CR8","doi-asserted-by":"publisher","first-page":"739","DOI":"10.1093\/jigpal\/jzaa017","volume":"29","author":"M Borisavljevi\u0107","year":"2021","unstructured":"Borisavljevi\u0107, M., The subformula property of natural deduction derivations and analytic cuts, Logic Journal of the IGPL 29(5): 739\u2013768, 2021.","journal-title":"Logic Journal of the IGPL"},{"key":"10023_CR9","unstructured":"Borisavljevi\u0107, M., Maximum segments as natural deduction images of some cuts, Journal of Logica Universalis, to appear."},{"key":"10023_CR10","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., The undecidability of k-provability, Annals of Pure and Applied Logic 53: 75\u2013102, 1991.","journal-title":"Annals of Pure and Applied Logic"},{"key":"10023_CR11","doi-asserted-by":"publisher","first-page":"207","DOI":"10.1016\/0304-3975(92)90300-5","volume":"102","author":"K Do\u0161en","year":"1992","unstructured":"Do\u0161en, K., Nonmodal classical linear predicate logic is a fragment of intuitionistic linear logic, Theoretical Computer Science 102: 207\u2013214, 1992.","journal-title":"Theoretical Computer Science"},{"key":"10023_CR12","doi-asserted-by":"crossref","unstructured":"Dyckhoff, R., Cut elimination, substitution and normalisation, in H. Wansing, (ed.), Dag Prawitz on Proofs and Meaning, Springer, 2015, pp. 163\u2013187.","DOI":"10.1007\/978-3-319-11041-7_7"},{"key":"10023_CR13","doi-asserted-by":"crossref","unstructured":"Gentzen, G., Untersuchungen \u00fcber das logische Schlie\u00dfen, Mathematische Zeitschrift 39: 176\u2013210, 405\u2013431, 1935 (English translation in [Gentzen 1969]).","DOI":"10.1007\/BF01201363"},{"key":"10023_CR14","unstructured":"Gentzen, G., in M. E. Szabo, (ed.), The Collected Papers of Gerhard Gentzen, North-Holland, 1969."},{"key":"10023_CR15","doi-asserted-by":"crossref","unstructured":"Girard, J. Y., Linear logic, Theoretical Computer Science 50: l\u2013102, 1987.","DOI":"10.1016\/0304-3975(87)90045-4"},{"key":"10023_CR16","unstructured":"Girard, J.-Y., and P.Taylor, Proofs and Types, 7 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1989."},{"key":"10023_CR17","doi-asserted-by":"crossref","unstructured":"Lambek, J., Logic without stuctural rules (another look at cut elimination), in K. Do\u0161en, and P. Schroeder-Heister, (eds.), Structural Logics, Calarendon Press, Oxford, 1993, pp. 179\u2013206.","DOI":"10.1093\/oso\/9780198537779.003.0007"},{"key":"10023_CR18","unstructured":"Minc, G. E., Normal forms for sequent derivations, in P. Odifreddi, (ed.), Kreiseliana: About and Around Georg Kreisel, Peters, 1996, pp. 469\u2013492."},{"key":"10023_CR19","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1023\/A:1005016206457","volume":"60","author":"GE Minc","year":"1998","unstructured":"Minc, G. E., Linear lambda-terms and natural deduction, Studia Logica 60: 209\u2013231, 1998.","journal-title":"Studia Logica"},{"key":"10023_CR20","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511527340","volume-title":"Structural Proof Theory","author":"S Negri","year":"2001","unstructured":"Negri, S., and J. von Plato, Structural Proof Theory, 4th edition, Cambridge University Press, Cambridge, 2001.","edition":"4"},{"key":"10023_CR21","doi-asserted-by":"publisher","first-page":"789","DOI":"10.1007\/s001530100136","volume":"41","author":"S Negri","year":"2002","unstructured":"Negri, S., A normalizing system of natural deduction for intuitionistic linear logic, Archive for Mathematical Logic 41: 789\u2013810, 2002.","journal-title":"Archive for Mathematical Logic"},{"issue":"5","key":"10023_CR22","doi-asserted-by":"publisher","first-page":"435","DOI":"10.1002\/malq.200310047","volume":"49","author":"S Negri","year":"2003","unstructured":"Negri, S., and J. von Plato, Translations from natural deduction to sequent calculus, Mathematical Logic Quarterly 49(5): 435\u2013443, 2003.","journal-title":"Mathematical Logic Quarterly"},{"key":"10023_CR23","first-page":"323","volume":"12","author":"G Pottinger","year":"1977","unstructured":"Pottinger, G., Normalization as a homomorrhic image of cut elimination, Annals of Pure and Applied Logic 12: 323\u2013357, 1977.","journal-title":"Annals of Pure and Applied Logic"},{"key":"10023_CR24","volume-title":"Natural Deduction","author":"D Prawitz","year":"1965","unstructured":"Prawitz, D., Natural Deduction, Almquist and Wiksell, Stockholm, 1965."},{"key":"10023_CR25","volume-title":"Lectures on Linear Logic, CSLI-Lectures Notes 29","author":"AS Troelstra","year":"1992","unstructured":"Troelstra, A. S., Lectures on Linear Logic, CSLI-Lectures Notes 29, Center for the Study of Language and Information, Stanford, California, 1992."},{"key":"10023_CR26","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1016\/0168-0072(93)E0078-3","volume":"73","author":"AS Troelstra","year":"1995","unstructured":"Troelstra, A. S., Natural deduction for intuitionistic linear logic, Annals of Pure and Applied Logic 73: 79\u2013108, 1995.","journal-title":"Annals of Pure and Applied Logic"},{"key":"10023_CR27","unstructured":"Troelstra, A. S., and H. Schwichtenberg, Basic Proof Theory, Cambridge University Press, 1996."},{"key":"10023_CR28","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., Revisiting Zucker\u2019s work on the correspondence between cut-elimination and normalisation, in L. C. Pereira, E. H. Edward, and V. de Paiva, (eds.), Advances in Natural Deduction, A Celebration of Dag Prawitz\u2019s Work, Springer, 2014, pp. 31\u201350."},{"issue":"1","key":"10023_CR29","doi-asserted-by":"publisher","first-page":"9","DOI":"10.1007\/s001530050170","volume":"40","author":"J von Plato","year":"2001","unstructured":"von Plato, J., A proof of Gentzen\u2019s Hauptsatz without multicut, Archive for Mathematical Logic 40(1): 9\u201318, 2001.","journal-title":"Archive for Mathematical Logic"},{"issue":"2","key":"10023_CR30","doi-asserted-by":"publisher","first-page":"240","DOI":"10.2178\/bsl\/1208442829","volume":"14","author":"J von Plato","year":"2008","unstructured":"von Plato, J., Gentzen\u2019s proof of normalization for natural deduction, The Bulletin of Symbolic Logic 14(2): 240\u2013257, 2008.","journal-title":"The Bulletin of Symbolic Logic"},{"issue":"1","key":"10023_CR31","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1017\/S1755020310000195","volume":"4","author":"J von Plato","year":"2011","unstructured":"von Plato, J., A sequent calculus isomorphic to Gentzen\u2019s natural deduction, Review of Symbolic Logic 4(1): 43\u201353, 2011.","journal-title":"Review of Symbolic Logic"},{"key":"10023_CR32","first-page":"1","volume":"7","author":"J Zucker","year":"1974","unstructured":"Zucker, J., The correspondence between cut-elimination and normalization, Annals of Pure and Applied Logic 7: 1\u2013112, 1974.","journal-title":"Annals of Pure and Applied Logic"}],"container-title":["Studia Logica"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s11225-022-10023-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s11225-022-10023-4\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s11225-022-10023-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,12,3]],"date-time":"2023-12-03T02:21:39Z","timestamp":1701570099000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s11225-022-10023-4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,12,15]]},"references-count":32,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2023,6]]}},"alternative-id":["10023"],"URL":"https:\/\/doi.org\/10.1007\/s11225-022-10023-4","relation":{},"ISSN":["0039-3215","1572-8730"],"issn-type":[{"value":"0039-3215","type":"print"},{"value":"1572-8730","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,12,15]]},"assertion":[{"value":"9 November 2021","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"23 September 2022","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"15 December 2022","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}