{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,6]],"date-time":"2025-11-06T20:08:30Z","timestamp":1762459710658,"version":"3.41.0"},"reference-count":65,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2019,2,22]],"date-time":"2019-02-22T00:00:00Z","timestamp":1550793600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2019,4,30]]},"abstract":"<jats:p>In this work, we explore the connections between (linear) nested sequent calculi and ordinary sequent calculi for normal and non-normal modal logics. By proposing local versions to ordinary sequent rules, we obtain linear nested sequent calculi for a number of logics, including, to our knowledge, the first nested sequent calculi for a large class of simply dependent multimodal logics and for many standard non-normal modal logics. The resulting systems are modular and have separate left and right introduction rules for the modalities, which makes them amenable to specification as bipole clauses. While this granulation of the sequent rules introduces more choices for proof search, we show how linear nested sequent calculi can be restricted to blocked derivations, which directly correspond to ordinary sequent derivations.<\/jats:p>","DOI":"10.1145\/3288757","type":"journal-article","created":{"date-parts":[[2019,2,22]],"date-time":"2019-02-22T22:19:21Z","timestamp":1550873961000},"page":"1-46","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":22,"title":["Modularisation of Sequent Calculi for Normal and Non-normal Modalities"],"prefix":"10.1145","volume":"20","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-5335-1838","authenticated-orcid":false,"given":"Bj\u00f6rn","family":"Lellmann","sequence":"first","affiliation":[{"name":"Institute of Logic 8 Computation, TU-Wien, Vienna, Austria"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7113-0801","authenticated-orcid":false,"given":"Elaine","family":"Pimentel","sequence":"additional","affiliation":[{"name":"Departamento de Matem\u00e1tica, UFRN, Natal, RN, Brazil"}]}],"member":"320","published-online":{"date-parts":[[2019,2,22]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-27683-0_1"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/2.3.297"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.03.009"},{"volume-title":"The method of hypersequents in the proof theory of propositional non-classical logics","author":"Avron Arnon","key":"e_1_2_1_4_1","unstructured":"Arnon Avron . 1996. The method of hypersequents in the proof theory of propositional non-classical logics . In Logic : From Foundations to Applications, Wilfrid Hodges, Martin Hyland, Charles Steinhorn, and John Truss (Eds.). Clarendon Press , New York, NY. Arnon Avron. 1996. The method of hypersequents in the proof theory of propositional non-classical logics. In Logic: From Foundations to Applications, Wilfrid Hodges, Martin Hyland, Charles Steinhorn, and John Truss (Eds.). Clarendon Press, New York, NY."},{"volume-title":"Modal Logic","author":"Blackburn Patrick","key":"e_1_2_1_5_1","unstructured":"Patrick Blackburn , Maarten de Rijke , and Yde Venema . 2001. Modal Logic . Cambridge University Press . Patrick Blackburn, Maarten de Rijke, and Yde Venema. 2001. Modal Logic. Cambridge University Press."},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00153-009-0137-3"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1002\/malq.19920380107"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49630-5_23"},{"key":"e_1_2_1_9_1","volume-title":"Proceedings of the 1st International Conference on Formal Structures for Computation and Deduction (FSCD\u201916)","volume":"52","author":"Chaudhuri Kaustuv","year":"2016","unstructured":"Kaustuv Chaudhuri , Sonia Marin , and Lutz Stra\u00dfburger . 2016 . Modular focused proof systems for intuitionistic modal logics . In Proceedings of the 1st International Conference on Formal Structures for Computation and Deduction (FSCD\u201916) , Delia Kesner and Brigitte Pientka (Eds.) , Vol. 52 . Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, 16:1--16:18. Kaustuv Chaudhuri, Sonia Marin, and Lutz Stra\u00dfburger. 2016. Modular focused proof systems for intuitionistic modal logics. In Proceedings of the 1st International Conference on Formal Structures for Computation and Deduction (FSCD\u201916), Delia Kesner and Brigitte Pientka (Eds.), Vol. 52. Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, 16:1--16:18."},{"volume-title":"Modal Logic","author":"Chellas Brian F.","key":"e_1_2_1_10_1","unstructured":"Brian F. Chellas . 1980. Modal Logic . Cambridge University Press . Brian F. Chellas. 1980. Modal Logic. Cambridge University Press."},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.5555\/646891.709408"},{"key":"e_1_2_1_12_1","volume-title":"Proceedings of the Advances in Modal Logic Conference (AiML\u201918)","author":"Dalmonte Tiziano","year":"2018","unstructured":"Tiziano Dalmonte , Nicola Olivetti , and Sara Negri . 2018 . Non-normal modal logics: Bi-neighbourhood semantics and its labelled calculi . In Proceedings of the Advances in Modal Logic Conference (AiML\u201918) , Guram Bezhanishvili, Giovanna D\u2019Agostino, George Metcalfe, and Thomas Studer (Eds.). College Publications. Tiziano Dalmonte, Nicola Olivetti, and Sara Negri. 2018. Non-normal modal logics: Bi-neighbourhood semantics and its labelled calculi. In Proceedings of the Advances in Modal Logic Conference (AiML\u201918), Guram Bezhanishvili, Giovanna D\u2019Agostino, George Metcalfe, and Thomas Studer (Eds.). College Publications."},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.5555\/648039.744568"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.5555\/646891.709296"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.apal.2011.09.004"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1215\/00294527-2377869"},{"volume-title":"Labelled Deductive Systems","author":"Gabbay Dov","key":"e_1_2_1_17_1","unstructured":"Dov Gabbay . 1996. Labelled Deductive Systems . Clarendon Press . Dov Gabbay. 1996. Labelled Deductive Systems. Clarendon Press."},{"key":"e_1_2_1_19_1","doi-asserted-by":"crossref","unstructured":"Gerhard Gentzen. 1969. Investigations into logical deduction. In The Collected Papers of Gerhard Gentzen. 68--131.  Gerhard Gentzen. 1969. Investigations into logical deduction. In The Collected Papers of Gerhard Gentzen. 68--131.","DOI":"10.1016\/S0049-237X(08)70822-X"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/s11225-014-9556-1"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(87)90045-4"},{"volume-title":"Tableau Methods for Modal and Temporal Logics","author":"Gor\u00e9 Rajeev","key":"e_1_2_1_22_1","unstructured":"Rajeev Gor\u00e9 . 1999. Tableau Methods for Modal and Temporal Logics . Kluwer , Dordrecht , 297--396. Rajeev Gor\u00e9. 1999. Tableau Methods for Modal and Temporal Logics. Kluwer, Dordrecht, 297--396."},{"key":"e_1_2_1_23_1","volume-title":"Proceedings of the Advances in Modal Logic Conference (AiML-9). 279--299","author":"Gor\u00e9 Rajeev","year":"2012","unstructured":"Rajeev Gor\u00e9 and Revantha Ramanayake . 2012 . Labelled tree sequents, tree hypersequents and nested (deep) sequents . In Proceedings of the Advances in Modal Logic Conference (AiML-9). 279--299 . www.aiml.net\/volumes\/volume9\/Gore-Ramanayake.pdf. Rajeev Gor\u00e9 and Revantha Ramanayake. 2012. Labelled tree sequents, tree hypersequents and nested (deep) sequents. In Proceedings of the Advances in Modal Logic Conference (AiML-9). 279--299. www.aiml.net\/volumes\/volume9\/Gore-Ramanayake.pdf."},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1093\/jigpal\/6.5.735"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.5555\/647851.737397"},{"volume-title":"Monotonic Modal Logics. Master\u2019s thesis","author":"Hansen Helle Hvid","key":"e_1_2_1_26_1","unstructured":"Helle Hvid Hansen . 2003. Monotonic Modal Logics. Master\u2019s thesis . University of Amsterdam , ILLC. Helle Hvid Hansen. 2003. Monotonic Modal Logics. Master\u2019s thesis. University of Amsterdam, ILLC."},{"key":"e_1_2_1_27_1","first-page":"151","article-title":"Sequent calculi for monotonic modal logics","volume":"34","author":"Indrzejczak Andrzej","year":"2005","unstructured":"Andrzej Indrzejczak . 2005 . Sequent calculi for monotonic modal logics . Bull. Sect. Log. 34 , 3 (2005), 151 -- 164 . Andrzej Indrzejczak. 2005. Sequent calculi for monotonic modal logics. Bull. Sect. Log. 34, 3 (2005), 151--164.","journal-title":"Bull. Sect. Log."},{"key":"e_1_2_1_28_1","first-page":"189","article-title":"Admissibility of cut in congruent modal logics","volume":"20","author":"Indrzejczak Andrzej","year":"2011","unstructured":"Andrzej Indrzejczak . 2011 . Admissibility of cut in congruent modal logics . Logic Logic. Philos. 20 , 3 (2011), 189 -- 203 . Andrzej Indrzejczak. 2011. Admissibility of cut in congruent modal logics. Logic Logic. Philos. 20, 3 (2011), 189--203.","journal-title":"Logic Logic. Philos."},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1017\/bsl.2016.2"},{"key":"e_1_2_1_30_1","first-page":"135","article-title":"Cut elimination theorem for non-commutative hypersequent calculus","volume":"46","author":"Indrzejczak Andrzej","year":"2017","unstructured":"Andrzej Indrzejczak . 2017 . Cut elimination theorem for non-commutative hypersequent calculus . Bull. Sect. Logic 46 , 1\/2 (2017), 135 -- 149 . Andrzej Indrzejczak. 2017. Cut elimination theorem for non-commutative hypersequent calculus. Bull. Sect. Logic 46, 1\/2 (2017), 135--149.","journal-title":"Bull. Sect. Logic"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01053026"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2017.8005089"},{"key":"e_1_2_1_33_1","first-page":"83","article-title":"Semantical considerations on modal logic","volume":"16","author":"Kripke Saul A.","year":"1963","unstructured":"Saul A. Kripke . 1963 . Semantical considerations on modal logic . Acta Philos. Fenn. 16 (1963), 83 -- 94 . Saul A. Kripke. 1963. Semantical considerations on modal logic. Acta Philos. Fenn. 16 (1963), 83--94.","journal-title":"Acta Philos. Fenn."},{"key":"e_1_2_1_34_1","volume-title":"Proceedings of the Conference on Advances in Modal Logic","author":"Kuznets Roman","year":"2018","unstructured":"Roman Kuznets and Bj\u00f6rn Lellmann . 2018 . Interpolation for intermediate logics via hyper- and linear nested sequents . In Proceedings of the Conference on Advances in Modal Logic 2018, Guram Bezhanishvili, Giovanna D\u2019Agostino, George Metcalfe, and Thomas Studer (Eds.). College Publications, 473--492. Roman Kuznets and Bj\u00f6rn Lellmann. 2018. Interpolation for intermediate logics via hyper- and linear nested sequents. In Proceedings of the Conference on Advances in Modal Logic 2018, Guram Bezhanishvili, Giovanna D\u2019Agostino, George Metcalfe, and Thomas Studer (Eds.). College Publications, 473--492."},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1026753129680"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-24312-2_10"},{"key":"e_1_2_1_38_1","volume-title":"Proceedings of the 21st International Conference on Logic for Programming Artificial Intelligence and Reasoning (LPAR-21)","author":"Lellmann Bj\u00f6rn","year":"2017","unstructured":"Bj\u00f6rn Lellmann , Carlos Olarte , and Elaine Pimentel . 2017 . A uniform framework for substructural logics with modalities . In Proceedings of the 21st International Conference on Logic for Programming Artificial Intelligence and Reasoning (LPAR-21) . 435--455. Bj\u00f6rn Lellmann, Carlos Olarte, and Elaine Pimentel. 2017. A uniform framework for substructural logics with modalities. In Proceedings of the 21st International Conference on Logic for Programming Artificial Intelligence and Reasoning (LPAR-21). 435--455."},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-36039-8_14"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-48899-7_39"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2009.07.041"},{"key":"e_1_2_1_42_1","volume-title":"Proceedings of the 11th Conference on Advances in Modal Logic, Lev D. Beklemishev, St\u00e9phane Demri, and Andr\u00e1s Mat\u00e9 (Eds.). College Publications, 469--488","author":"Marin Sonia","year":"2016","unstructured":"Sonia Marin , Dale Miller , and Marco Volpe . 2016 . A focused framework for emulating modal proof systems . In Proceedings of the 11th Conference on Advances in Modal Logic, Lev D. Beklemishev, St\u00e9phane Demri, and Andr\u00e1s Mat\u00e9 (Eds.). College Publications, 469--488 . Sonia Marin, Dale Miller, and Marco Volpe. 2016. A focused framework for emulating modal proof systems. In Proceedings of the 11th Conference on Advances in Modal Logic, Lev D. Beklemishev, St\u00e9phane Demri, and Andr\u00e1s Mat\u00e9 (Eds.). College Publications, 469--488."},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1016\/0168-0072(92)90029-Y"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1006155811656"},{"key":"e_1_2_1_45_1","doi-asserted-by":"crossref","unstructured":"J. McCarthy M. Sato T. Hayashi and S. Igarishi. 1978. On the Model Theory of Knowledge. Technical Report. Retrieved from http:\/\/www-formal.stanford.edu\/jmc\/model\/.   J. McCarthy M. Sato T. Hayashi and S. Igarishi. 1978. On the Model Theory of Knowledge. Technical Report. Retrieved from http:\/\/www-formal.stanford.edu\/jmc\/model\/.","DOI":"10.21236\/ADA065502"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2011.10.003"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.5555\/646892.709436"},{"key":"e_1_2_1_48_1","volume-title":"Proceedings of the Annual European Summer Meeting of the Association for Symbolic Logic (Logic Colloquium\u201999)","author":"Miller Dale","year":"2004","unstructured":"Dale Miller and Elaine Pimentel . 2004 . Linear logic as a framework for specifying sequent calculus . In Proceedings of the Annual European Summer Meeting of the Association for Symbolic Logic (Logic Colloquium\u201999) , Jan van Eijck, Vincent van Oostrom, and Albert Visser (Eds.). A K Peters Ltd, 111--135. Dale Miller and Elaine Pimentel. 2004. Linear logic as a framework for specifying sequent calculus. In Proceedings of the Annual European Summer Meeting of the Association for Symbolic Logic (Logic Colloquium\u201999), Jan van Eijck, Vincent van Oostrom, and Albert Visser (Eds.). A K Peters Ltd, 111--135."},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2012.12.008"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-48899-7_19"},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10992-005-2267-3"},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/exu037"},{"key":"e_1_2_1_53_1","first-page":"1241","article-title":"Proof theory for non-normal modal logics: The neighbourhood formalism and basic results","volume":"4","author":"Negri Sara","year":"2017","unstructured":"Sara Negri . 2017 . Proof theory for non-normal modal logics: The neighbourhood formalism and basic results . IfCoLog J. Log. Appl. 4 , 4 (2017), 1241 -- 1286 . Sara Negri. 2017. Proof theory for non-normal modal logics: The neighbourhood formalism and basic results. IfCoLog J. Log. Appl. 4, 4 (2017), 1241--1286.","journal-title":"IfCoLog J. Log. Appl."},{"key":"e_1_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139003513"},{"key":"e_1_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-010-9182-1"},{"key":"e_1_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/exu029"},{"key":"e_1_2_1_57_1","first-page":"113","article-title":"Gentzen method in modal calculi","volume":"9","author":"Ohnishi Masao","year":"1957","unstructured":"Masao Ohnishi and Kazuo Matsumoto . 1957 . Gentzen method in modal calculi . Osaka Math. J. 9 (1957), 113 -- 130 . http:\/\/hdl.handle.net\/11094\/6054 Masao Ohnishi and Kazuo Matsumoto. 1957. Gentzen method in modal calculi. Osaka Math. J. 9 (1957), 113--130. http:\/\/hdl.handle.net\/11094\/6054","journal-title":"Osaka Math. J."},{"key":"e_1_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08615-6_11"},{"key":"e_1_2_1_60_1","volume-title":"Slides for an invited talk at LFMTP","author":"Pfenning Frank","year":"2015","unstructured":"Frank Pfenning . 2015. Decomposing Modalities . ( 2015 ). Slides for an invited talk at LFMTP 2015, Berlin, Germany . Retrieved Feb 2017 from http:\/\/www.cs.cmu.edu\/ fp\/talks\/lfmtp15-talk.pdf. Frank Pfenning. 2015. Decomposing Modalities. (2015). Slides for an invited talk at LFMTP 2015, Berlin, Germany. Retrieved Feb 2017 from http:\/\/www.cs.cmu.edu\/ fp\/talks\/lfmtp15-talk.pdf."},{"key":"e_1_2_1_61_1","doi-asserted-by":"publisher","DOI":"10.1007\/11591191_25"},{"key":"e_1_2_1_62_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4020-9084-4_3"},{"key":"e_1_2_1_63_1","doi-asserted-by":"publisher","DOI":"10.1080\/11663081.2015.1080422"},{"key":"e_1_2_1_64_1","doi-asserted-by":"publisher","DOI":"10.5555\/646798.705320"},{"key":"e_1_2_1_66_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37075-5_14"},{"key":"e_1_2_1_67_1","doi-asserted-by":"publisher","DOI":"10.5555\/351148"},{"key":"e_1_2_1_68_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4757-3208-5"},{"volume-title":"Handbook of Philosophical Logic","author":"Wansing Heinrich","key":"e_1_2_1_69_1","unstructured":"Heinrich Wansing . 2002. Sequent systems for modal logics . In Handbook of Philosophical Logic , Vol. 8 , Dov M. Gabbay and Franz Guenthner (Eds.). Springer-Verlag , Berlin. Heinrich Wansing. 2002. Sequent systems for modal logics. In Handbook of Philosophical Logic, Vol. 8, Dov M. Gabbay and Franz Guenthner (Eds.). Springer-Verlag, Berlin."}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3288757","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3288757","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T01:02:23Z","timestamp":1750208543000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3288757"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,2,22]]},"references-count":65,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2019,4,30]]}},"alternative-id":["10.1145\/3288757"],"URL":"https:\/\/doi.org\/10.1145\/3288757","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"type":"print","value":"1529-3785"},{"type":"electronic","value":"1557-945X"}],"subject":[],"published":{"date-parts":[[2019,2,22]]},"assertion":[{"value":"2017-02-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2018-10-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2019-02-22","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}