{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,13]],"date-time":"2025-05-13T21:57:29Z","timestamp":1747173449636,"version":"3.40.5"},"reference-count":50,"publisher":"Cambridge University Press (CUP)","issue":"9","license":[{"start":{"date-parts":[[2022,11,22]],"date-time":"2022-11-22T00:00:00Z","timestamp":1669075200000},"content-version":"unspecified","delay-in-days":52,"URL":"http:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["cambridge.org"],"crossmark-restriction":true},"short-container-title":["Math. Struct. Comp. Sci."],"published-print":{"date-parts":[[2022,10]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>One of the most fundamental properties of a proof system is <jats:italic>analyticity<\/jats:italic>, expressing the fact that a proof of a given formula <jats:italic>F<\/jats:italic> only uses subformulas of <jats:italic>F<\/jats:italic>. In sequent calculus, this property is usually proved by showing that the <jats:inline-formula><jats:alternatives><jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"png\" xlink:href=\"S0960129522000366_inline1.png\"\/><jats:tex-math>\n$\\mathsf{cut}$\n<\/jats:tex-math><\/jats:alternatives><\/jats:inline-formula> rule is admissible, i.e., the introduction of the auxiliary lemma H in the reasoning \u201cif <jats:italic>H<\/jats:italic> follows from <jats:italic>G<\/jats:italic> and <jats:italic>F<\/jats:italic> follows from <jats:italic>H<\/jats:italic>, then <jats:italic>F<\/jats:italic> follows from <jats:italic>G<\/jats:italic>\u201d can be eliminated. The proof of cut admissibility is usually a tedious, error-prone process through several proof transformations, thus requiring the assistance of (semi-)automatic procedures. In a previous work by Miller and Pimentel, linear logic (<jats:inline-formula><jats:alternatives><jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"png\" xlink:href=\"S0960129522000366_inline2.png\"\/><jats:tex-math>\n$\\mathsf{LL}$\n<\/jats:tex-math><\/jats:alternatives><\/jats:inline-formula>) was used as a logical framework for establishing sufficient conditions for cut admissibility of object logical systems (OL). The OL\u2019s inference rules are specified as an <jats:inline-formula><jats:alternatives><jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"png\" xlink:href=\"S0960129522000366_inline3.png\"\/><jats:tex-math>\n$\\mathsf{LL}$\n<\/jats:tex-math><\/jats:alternatives><\/jats:inline-formula> theory and an easy-to-verify criterion sufficed to establish the cut-admissibility theorem for the OL at hand. However, there are many logical systems that cannot be adequately encoded in <jats:inline-formula><jats:alternatives><jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"png\" xlink:href=\"S0960129522000366_inline4.png\"\/><jats:tex-math>\n$\\mathsf{LL}$\n<\/jats:tex-math><\/jats:alternatives><\/jats:inline-formula>, the most symptomatic cases being sequent systems for modal logics. In this paper, we use a linear-nested sequent (<jats:inline-formula><jats:alternatives><jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"png\" xlink:href=\"S0960129522000366_inline5.png\"\/><jats:tex-math>\n$\\mathsf{LNS}$\n<\/jats:tex-math><\/jats:alternatives><\/jats:inline-formula>) presentation of <jats:inline-formula><jats:alternatives><jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"png\" xlink:href=\"S0960129522000366_inline6.png\"\/><jats:tex-math>\n$\\mathsf{MMLL}$\n<\/jats:tex-math><\/jats:alternatives><\/jats:inline-formula> (a variant of LL with subexponentials), and show that it is possible to establish a cut-admissibility criterion for <jats:inline-formula><jats:alternatives><jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"png\" xlink:href=\"S0960129522000366_inline7.png\"\/><jats:tex-math>\n$\\mathsf{LNS}$\n<\/jats:tex-math><\/jats:alternatives><\/jats:inline-formula> systems for (classical or substructural) multimodal logics. We show that the same approach is suitable for handling the <jats:inline-formula><jats:alternatives><jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"png\" xlink:href=\"S0960129522000366_inline8.png\"\/><jats:tex-math>\n$\\mathsf{LNS}$\n<\/jats:tex-math><\/jats:alternatives><\/jats:inline-formula> system for intuitionistic logic.<\/jats:p>","DOI":"10.1017\/s0960129522000366","type":"journal-article","created":{"date-parts":[[2022,11,22]],"date-time":"2022-11-22T04:41:03Z","timestamp":1669092063000},"page":"1176-1204","update-policy":"https:\/\/doi.org\/10.1017\/policypage","source":"Crossref","is-referenced-by-count":0,"title":["A linear logic framework for multimodal logics"],"prefix":"10.1017","volume":"32","author":[{"given":"Bruno","family":"Xavier","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7264-7773","authenticated-orcid":false,"given":"Carlos","family":"Olarte","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7113-0801","authenticated-orcid":false,"given":"Elaine","family":"Pimentel","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"56","published-online":{"date-parts":[[2022,11,22]]},"reference":[{"key":"S0960129522000366_ref3","doi-asserted-by":"publisher","DOI":"10.1007\/s00153-009-0137-3"},{"key":"S0960129522000366_ref5","doi-asserted-by":"publisher","DOI":"10.1002\/malq.19920380107"},{"key":"S0960129522000366_ref34","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2017.06.009"},{"key":"S0960129522000366_ref32","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-74915-8_31"},{"key":"S0960129522000366_ref36","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08587-6_18"},{"key":"S0960129522000366_ref38","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-99840-4_7"},{"key":"S0960129522000366_ref37","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2016.03.029"},{"key":"S0960129522000366_ref17","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(87)90045-4"},{"key":"S0960129522000366_ref14","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129521000323"},{"key":"S0960129522000366_ref44","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4020-9084-4_3"},{"key":"S0960129522000366_ref4","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2005.11.047"},{"key":"S0960129522000366_ref46","unstructured":"Stark, K. (2020). Mechanising Syntax with Binders in Coq. Phd thesis, Saarland University, Saarbr\u00fccken, Germany."},{"key":"S0960129522000366_ref7","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-48899-7_11"},{"key":"S0960129522000366_ref40","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1999.2832"},{"key":"S0960129522000366_ref8","doi-asserted-by":"publisher","DOI":"10.1145\/1411204.1411226"},{"key":"S0960129522000366_ref27","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2009.07.041"},{"key":"S0960129522000366_ref41","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-57669-4_3"},{"key":"S0960129522000366_ref49","unstructured":"Xavier, B. and Olarte, C. (2021). Multi-modalities in linear logic. https:\/\/github.com\/meta-logic\/MMLL."},{"key":"S0960129522000366_ref20","first-page":"1521","article-title":"Formalizing the meta-theory of first-order predicate logic","volume":"54","author":"Heberlin","year":"2017","journal-title":"Journal of the Korean Mathematical Society"},{"key":"S0960129522000366_ref19","doi-asserted-by":"publisher","DOI":"10.1093\/jigpal\/6.5.735"},{"key":"S0960129522000366_ref30","doi-asserted-by":"publisher","DOI":"10.2307\/2275915"},{"key":"S0960129522000366_ref22","doi-asserted-by":"publisher","DOI":"10.1007\/BF01053026"},{"key":"S0960129522000366_ref10","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0022564"},{"key":"S0960129522000366_ref12","doi-asserted-by":"publisher","DOI":"10.1145\/1599410.1599422"},{"key":"S0960129522000366_ref26","doi-asserted-by":"publisher","DOI":"10.1145\/3288757"},{"key":"S0960129522000366_ref23","doi-asserted-by":"crossref","unstructured":"Laurent, O. (2021). An anti-locally-nameless approach to formalizing quantifiers. In: Hritcu, C. and Popescu, A. (eds.) CPP\u201921: 10th ACM SIGPLAN International Conference on Certified Programs and Proofs, Virtual Event, Denmark, January 17\u201319, 2021, ACM, 300\u2013312.","DOI":"10.1145\/3437992.3439926"},{"key":"S0960129522000366_ref29","doi-asserted-by":"publisher","DOI":"10.1017\/S0027763000018055"},{"key":"S0960129522000366_ref47","doi-asserted-by":"crossref","unstructured":"Stark, K. , Sch\u00e4fer, S. and Kaiser, J. (2019). Autosubst 2: reasoning with multi-sorted de bruijn terms and vector substitutions. In: Mahboubi, A. and Myreen, M. O. (eds.) Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2019, Cascais, Portugal, January 14\u201315, 2019, 166\u2013180. ACM.","DOI":"10.1145\/3293880.3294101"},{"key":"S0960129522000366_ref2","first-page":"1","volume-title":"Logic: From Foundations to Applications: European Logic Colloquium","author":"Avron","year":"1996"},{"key":"S0960129522000366_ref6","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2019.02.023"},{"key":"S0960129522000366_ref31","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2012.12.008"},{"key":"S0960129522000366_ref25","unstructured":"Lellmann, B. , Olarte, C. and Pimentel, E. (2017). A uniform framework for substructural logics with modalities. In: LPAR-21, 435\u2013455."},{"key":"S0960129522000366_ref1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/2.3.297"},{"key":"S0960129522000366_ref39","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2020.08.008"},{"key":"S0960129522000366_ref21","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129518000117"},{"key":"S0960129522000366_ref13","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-010-9194-x"},{"key":"S0960129522000366_ref43","doi-asserted-by":"publisher","DOI":"10.1016\/S0890-5401(03)00138-X"},{"key":"S0960129522000366_ref9","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-86059-2_17"},{"key":"S0960129522000366_ref24","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-24312-2_10"},{"key":"S0960129522000366_ref35","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/exu029"},{"key":"S0960129522000366_ref11","doi-asserted-by":"publisher","DOI":"10.1007\/10722086_17"},{"key":"S0960129522000366_ref16","doi-asserted-by":"crossref","unstructured":"Gentzen, G. (1969). Investigations into logical deduction. In: Szabo, M. E. (ed.) The Collected Papers of Gerhard Gentzen, North-Holland, 68\u2013131.","DOI":"10.1016\/S0049-237X(08)70822-X"},{"key":"S0960129522000366_ref42","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-29026-9_9"},{"key":"S0960129522000366_ref45","unstructured":"Simpson, A. K. (1994). The Proof Theory and Semantics of Intuitionistic Modal Logic. Phd thesis, College of Science and Engineering, School of Informatics, University of Edinburgh."},{"key":"S0960129522000366_ref15","unstructured":"Forster, Y. (2021). Computability in Constructive Type Theory. Phd thesis, Saarland University."},{"key":"S0960129522000366_ref50","doi-asserted-by":"crossref","unstructured":"Xavier, B. , Olarte, C. , Reis, G. and Nigam, V. (2017). Mechanizing focused linear logic in coq. In: Alves, S. and Wasserman, R. (eds.) LSFA 2017, ENTCS, vol. 338, Elsevier, 219\u2013236.","DOI":"10.1016\/j.entcs.2018.10.014"},{"key":"S0960129522000366_ref18","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1998.2700"},{"key":"S0960129522000366_ref28","unstructured":"Licata, D. R. , Shulman, M. and Riley, M. (2017). A fibrational framework for substructural and modal logics. In: Miller, D. (ed.), FSCD 2017, LIPIcs, vol. 84, Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, 25:1\u201325:22."},{"key":"S0960129522000366_ref33","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-010-9182-1"},{"key":"S0960129522000366_ref48","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4757-3208-5"}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129522000366","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,3,29]],"date-time":"2023-03-29T02:33:32Z","timestamp":1680057212000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129522000366\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,10]]},"references-count":50,"journal-issue":{"issue":"9","published-print":{"date-parts":[[2022,10]]}},"alternative-id":["S0960129522000366"],"URL":"https:\/\/doi.org\/10.1017\/s0960129522000366","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"type":"print","value":"0960-1295"},{"type":"electronic","value":"1469-8072"}],"subject":[],"published":{"date-parts":[[2022,10]]},"assertion":[{"value":"\u00a9 The Author(s), 2022. Published by Cambridge University Press","name":"copyright","label":"Copyright","group":{"name":"copyright_and_licensing","label":"Copyright and Licensing"}},{"value":"This is an Open Access article, distributed under the terms of the Creative Commons Attribution licence (http:\/\/creativecommons.org\/licenses\/by\/4.0\/), which permits unrestricted re-use, distribution and reproduction, provided the original article is properly cited.","name":"license","label":"License","group":{"name":"copyright_and_licensing","label":"Copyright and Licensing"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}