{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,10]],"date-time":"2025-09-10T21:58:06Z","timestamp":1757541486528,"version":"3.40.3"},"publisher-location":"Cham","reference-count":31,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031635007"},{"type":"electronic","value":"9783031635014"}],"license":[{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,7,2]],"date-time":"2024-07-02T00:00:00Z","timestamp":1719878400000},"content-version":"vor","delay-in-days":183,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2024]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Enhancing cut-free expressiveness through minimal structural additions to sequent calculus is a natural step. We focus on \u00c5qvist\u2019s system <jats:inline-formula><jats:alternatives><jats:tex-math>$$\\textbf{F}$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                    <mml:mi>F<\/mml:mi>\n                  <\/mml:math><\/jats:alternatives><\/jats:inline-formula> with cautious monotonicity (<jats:bold>CM<\/jats:bold>), a deontic logic extension of <jats:inline-formula><jats:alternatives><jats:tex-math>$$\\textbf{S5}$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                    <mml:mrow>\n                      <mml:mi>S<\/mml:mi>\n                      <mml:mn>5<\/mml:mn>\n                    <\/mml:mrow>\n                  <\/mml:math><\/jats:alternatives><\/jats:inline-formula>, for which we define a sequent calculus employing (semi) analytic cuts.The transition to hypersequents is key to develop modular and cut-free calculi for <jats:inline-formula><jats:alternatives><jats:tex-math>$$\\mathbf{F + (CM)}$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                    <mml:mrow>\n                      <mml:mi>F<\/mml:mi>\n                      <mml:mo>+<\/mml:mo>\n                      <mml:mo>(<\/mml:mo>\n                      <mml:mi>CM<\/mml:mi>\n                      <mml:mo>)<\/mml:mo>\n                    <\/mml:mrow>\n                  <\/mml:math><\/jats:alternatives><\/jats:inline-formula> and <jats:inline-formula><jats:alternatives><jats:tex-math>$$\\textbf{G}$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                    <mml:mi>G<\/mml:mi>\n                  <\/mml:math><\/jats:alternatives><\/jats:inline-formula>, also supporting countermodel construction.<\/jats:p>","DOI":"10.1007\/978-3-031-63501-4_10","type":"book-chapter","created":{"date-parts":[[2024,7,1]],"date-time":"2024-07-01T09:02:00Z","timestamp":1719824520000},"page":"176-195","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Sequents vs Hypersequents for\u00a0\u00c5qvist Systems"],"prefix":"10.1007","author":[{"given":"Agata","family":"Ciabattoni","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Matteo","family":"Tesi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2024,7,2]]},"reference":[{"key":"10_CR1","series-title":"Synthese Library","doi-asserted-by":"publisher","first-page":"605","DOI":"10.1007\/978-94-009-6259-0_11","volume-title":"Handbook of Philosophical Logic","author":"L \u00c5qvist","year":"1984","unstructured":"\u00c5qvist, L.: Deontic logic. In: Gabbay, D., Guenthner, F. (eds.) Handbook of Philosophical Logic. Synthese Library, vol. 165, pp. 605\u2013714. Springer, Dordrecht (1984). https:\/\/doi.org\/10.1007\/978-94-009-6259-0_11"},{"issue":"4","key":"10_CR2","doi-asserted-by":"publisher","first-page":"939","DOI":"10.2307\/2273828","volume":"52","author":"A Avron","year":"1987","unstructured":"Avron, A.: A constructive analysis of RM. J. Symb. Logic 52(4), 939\u2013951 (1987)","journal-title":"J. Symb. Logic"},{"key":"10_CR3","doi-asserted-by":"publisher","first-page":"225","DOI":"10.1007\/BF01531058","volume":"4","author":"A Avron","year":"1991","unstructured":"Avron, A.: Hypersequents, logical consequence and intermediate logics for concurrency. Ann. Math. Artif. Intell. 4, 225\u2013248 (1991)","journal-title":"Ann. Math. Artif. Intell."},{"key":"10_CR4","doi-asserted-by":"crossref","unstructured":"Avron, A.: The method of hypersequents in the proof theory of propositional non-classical logics. In: Logic: From Foundations to Applications, pp. 1\u201332. OUP, New York (1996)","DOI":"10.1093\/oso\/9780198538622.003.0001"},{"issue":"4","key":"10_CR5","doi-asserted-by":"publisher","first-page":"375","DOI":"10.1007\/BF00284976","volume":"11","author":"ND Belnap Jr","year":"1982","unstructured":"Belnap, N.D., Jr.: Display logic. J. Philos. Logic 11(4), 375\u2013417 (1982)","journal-title":"J. Philos. Logic"},{"issue":"3","key":"10_CR6","doi-asserted-by":"crossref","first-page":"76","DOI":"10.1305\/ndjfl\/1093883456","volume":"22","author":"J Burgess","year":"1981","unstructured":"Burgess, J.: Quick completeness proofs for some logics of conditionals. Notre Dame J. Formal Logic 22(3), 76\u201384 (1981)","journal-title":"Notre Dame J. Formal Logic"},{"key":"10_CR7","doi-asserted-by":"crossref","unstructured":"Ciabattoni, A., Lang, T., Ramanayake, R.: Cut-restriction: from cuts to analytic cuts. In: LICS, pp. 1\u201313 (2023)","DOI":"10.1109\/LICS56636.2023.10175785"},{"key":"10_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"54","DOI":"10.1007\/978-3-031-21203-1_4","volume-title":"PRIMA 2022: Principles and Practice of Multi-Agent Systems","author":"A Ciabattoni","year":"2022","unstructured":"Ciabattoni, A., Olivetti, N., Parent, X.: Dyadic obligations: proofs and countermodels via hypersequents. In: Aydo\u011fan, R., Criado, N., Lang, J., Sanchez-Anguix, V., Serramia, M. (eds.) PRIMA 2022. LNCS, vol. 13753, pp. 54\u201371. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-21203-1_4"},{"key":"10_CR9","unstructured":"Ciabattoni, A., Olivetti, N., Parent, X., Ramanayake, R., Rozplokhas, D.: Analytic proof theory for Aqvist\u2019s system F. In: Maranh\u00e3o, J., Peterson, C., Stra\u00dfer, C., van\u00a0der Torre, L. (eds.) DEON 2023, pp. 79\u201398 (2023)"},{"key":"10_CR10","doi-asserted-by":"publisher","first-page":"96","DOI":"10.2307\/2964753","volume":"24","author":"M Dummett","year":"1959","unstructured":"Dummett, M.: A propositional logic with denumerable matrix. J. Symb. Log. 24, 96\u2013107 (1959)","journal-title":"J. Symb. Log."},{"key":"10_CR11","unstructured":"Gabbay, D., Horty, J., Parent, X., van\u00a0der Torre, L., van\u00a0der Meyden, R. (eds.) Handbook of Deontic Logic and Normative Systems, vol. 2. College Publications, London (2021)"},{"key":"10_CR12","series-title":"NATO ASI Series","doi-asserted-by":"publisher","first-page":"439","DOI":"10.1007\/978-3-642-82453-1_15","volume-title":"Logics and Models of Concurrent Systems","author":"DM Gabbay","year":"1985","unstructured":"Gabbay, D.M.: Theoretical foundations for non-monotonic reasoning in expert systems. In: Apt, K.R. (ed.) Logics and Models of Concurrent Systems. NATO ASI Series, vol. 13, pp. 439\u2013457. Springer, Heidelberg (1985). https:\/\/doi.org\/10.1007\/978-3-642-82453-1_15"},{"key":"10_CR13","doi-asserted-by":"crossref","unstructured":"Giordano, L., Gliozzi, V., Olivetti, N., Pozzato, G.L.: Analytic tableaux calculi for KLM logics of nonmonotonic reasoning. ACM Trans. Comput. Log. 10(3), 18:1\u201318:47 (2009)","DOI":"10.1145\/1507244.1507248"},{"key":"10_CR14","doi-asserted-by":"crossref","unstructured":"Girlando, M., Lellmann, B., Olivetti, N., Pozzato, G.L.: Hypersequent calculi for Lewis\u2019 conditional logics with uniformity and reflexivity. In: Proceedings of Tableaux (2017)","DOI":"10.1007\/978-3-319-66902-1_8"},{"key":"10_CR15","doi-asserted-by":"publisher","DOI":"10.1007\/978-90-481-8785-0","volume-title":"Natural Deduction, Hybrid Systems and Modal Logics","author":"A Indrzejczak","year":"2010","unstructured":"Indrzejczak, A.: Natural Deduction, Hybrid Systems and Modal Logics. Springer, Dordrecht (2010). https:\/\/doi.org\/10.1007\/978-90-481-8785-0"},{"key":"10_CR16","unstructured":"Indrzejczak, A.: Cut-free hypersequent calculus for S4.3. Bull. Sect. Logic Univ. \u0141\u00f3d\u017a 41(1\u20132), 89\u2013104 (2012)"},{"issue":"2","key":"10_CR17","doi-asserted-by":"publisher","first-page":"259","DOI":"10.1017\/S175502031600040X","volume":"10","author":"T Kowalski","year":"2017","unstructured":"Kowalski, T., Ono, H.: Analytic cut and interpolation for bi-intuitionistic logic. Rev. Symb. Log. 10(2), 259\u2013283 (2017)","journal-title":"Rev. Symb. Log."},{"issue":"1\u20132","key":"10_CR18","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1016\/0004-3702(90)90101-5","volume":"44","author":"S Kraus","year":"1990","unstructured":"Kraus, S., Lehmann, D., Magidor, M.: Nonmonotonic reasoning, preferential models and cumulative logics. Artif. Intell. 44(1\u20132), 167\u2013207 (1990)","journal-title":"Artif. Intell."},{"key":"10_CR19","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"51","DOI":"10.1007\/978-3-319-10061-6_4","volume-title":"New Frontiers in Artificial Intelligence","author":"H Kurokawa","year":"2014","unstructured":"Kurokawa, H.: Hypersequent calculi for modal logics extending S4. In: Nakano, Y., Satoh, K., Bekki, D. (eds.) JSAI-isAI 2013. LNCS (LNAI), vol. 8417, pp. 51\u201368. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-10061-6_4"},{"key":"10_CR20","unstructured":"Schr\u00f6der, L., Pattinson, D., Hausmann, D.: Optimal tableaux for conditional logics with cautious monotonicity. In: Wooldridge, M. Coelho, H., Studer, R. (eds.) Proceedings of the 2010 conference on ECAI 2010: 19th European Conference on Artificial Intelligence, pp. 707\u2013712. IOS Press, Amsterdam (2010)"},{"key":"10_CR21","volume-title":"Counterfactuals","author":"D Lewis","year":"1973","unstructured":"Lewis, D.: Counterfactuals. Blackwell, Oxford (1973)"},{"key":"10_CR22","unstructured":"Lyon, T.S., et al.: Internal and external calculi: ordering the jungle without being lost in translations. CoRR, abs\/2312.03426 (2023)"},{"key":"10_CR23","first-page":"88","volume":"98","author":"G Minc","year":"1968","unstructured":"Minc, G.: Some calculi of modal logic. Trudy Mat. Inst. Steklov 98, 88\u2013111 (1968)","journal-title":"Trudy Mat. Inst. Steklov"},{"key":"10_CR24","doi-asserted-by":"crossref","unstructured":"Negri, S., Olivetti, N.: A sequent calculus for preferential conditional logic based on neighbourhood semantics. In: Proceedings of Tableaux, vol. 9323, pp. 115\u2013134 (2015)","DOI":"10.1007\/978-3-319-24312-2_9"},{"key":"10_CR25","first-page":"113","volume":"9","author":"M Ohnishi","year":"1957","unstructured":"Ohnishi, M., Matsumoto, K.: Gentzen method in modal calculi. Osaka Math. J. 9, 113\u2013130 (1957)","journal-title":"Osaka Math. J."},{"key":"10_CR26","unstructured":"Ono, H., Sano, K.: Analytic cut and Mints\u2019 symmetric interpolation method for Bi-intuitionistic tense logic. In: Advances in Modal Logic, pp. 601\u2013624. College Publications (2022)"},{"key":"10_CR27","doi-asserted-by":"crossref","unstructured":"Parent, X.: Maximality vs. optimality in dyadic deontic logic. J. Philos. Log. 43(6), 1101\u20131128 (2014)","DOI":"10.1007\/s10992-013-9308-0"},{"key":"10_CR28","unstructured":"Parent, X.: Preference semantics for Hansson-type dyadic deontic logic: a survey of results. In: Gabbay, et\u00a0al. [11], pp. 7\u201370"},{"key":"10_CR29","doi-asserted-by":"publisher","first-page":"560","DOI":"10.2307\/2271362","volume":"33","author":"RM Smullyan","year":"1968","unstructured":"Smullyan, R.M.: Analytic cut. J. Symb. Log. 33, 560\u2013564 (1968)","journal-title":"J. Symb. Log."},{"key":"10_CR30","first-page":"1129","volume":"37","author":"M Takano","year":"1992","unstructured":"Takano, M.: Subformula property as a substitute for cut-elimination in modal propositional logics. Math. Japon. 37, 1129\u20131145 (1992)","journal-title":"Math. Japon."},{"key":"10_CR31","first-page":"08","volume":"49","author":"M Takano","year":"2020","unstructured":"Takano, M.: New modification of the subformula property for a modal logic. Bull. Sect. Log. 49, 08 (2020)","journal-title":"Bull. Sect. Log."}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-63501-4_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,7,1]],"date-time":"2024-07-01T09:03:40Z","timestamp":1719824620000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-63501-4_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031635007","9783031635014"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-63501-4_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"2 July 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"IJCAR","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Joint Conference on Automated Reasoning","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Nancy","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"France","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"3 July 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"6 July 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"12","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"ijcar2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/merz.gitlabpages.inria.fr\/2024-ijcar\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}