{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,18]],"date-time":"2026-09-18T15:56:44Z","timestamp":1789747004806,"version":"4.0.1"},"reference-count":20,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2011,3,17]],"date-time":"2011-03-17T00:00:00Z","timestamp":1300320000000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/arxiv.org\/licenses\/nonexclusive-distrib\/1.0"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>We develop a general criterion for cut elimination in sequent calculi for propositional modal logics, which rests on absorption of cut, contraction, weakening and inversion by the purely modal part of the rule system. Our criterion applies also to a wide variety of logics outside the realm of normal modal logic. We give extensive example instantiations of our framework to various conditional logics. For these, we obtain fully internalised calculi which are substantially simpler than those known in the literature, along with leaner proofs of cut elimination and complexity. In one case, conditional logic with modus ponens and conditional excluded middle, cut elimination and complexity were explicitly stated as open in the literature.<\/jats:p>","DOI":"10.2168\/lmcs-7(1:4)2011","type":"journal-article","created":{"date-parts":[[2011,9,23]],"date-time":"2011-09-23T08:18:47Z","timestamp":1316765927000},"source":"Crossref","is-referenced-by-count":10,"title":["Generic Modal Cut Elimination Applied to Conditional Logics"],"prefix":"10.46298","volume":"Volume 7, Issue 1","author":[{"given":"Dirk","family":"Pattinson","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3146-5906","authenticated-orcid":false,"given":"Lutz","family":"Schr\u00f6der","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"25203","published-online":{"date-parts":[[2011,3,17]]},"reference":[{"key":"10.2168\/LMCS-7(1:4)2011_AvronLev01","unstructured":"A. Avron and I. Lev. Canonical propositional Gentzen-type systems. In\n                      International Joint Conferences on Automated Reasoning, IJCAR 01\n                      , vol. 2083 of\n                      LNCS\n                      , pp. 529-544. Springer, 2001."},{"key":"10.2168\/LMCS-7(1:4)2011_Burgess81","doi-asserted-by":"crossref","first-page":"76","DOI":"10.1305\/ndjfl\/1093883341","volume":"22","author":"J. Burgess","year":"1981","journal-title":"Notre Dame J. Formal Logic"},{"key":"10.2168\/LMCS-7(1:4)2011_Chellas80","doi-asserted-by":"crossref","unstructured":"B. Chellas.\n                      Modal Logic\n                      . Cambridge University Press, 1980.","DOI":"10.1017\/CBO9780511621192"},{"key":"10.2168\/LMCS-7(1:4)2011_CiabattoniEA08","doi-asserted-by":"crossref","unstructured":"A. Ciabattoni, N. Galatos, and K. Terui. From axioms to analytic rules in nonclassical logics. In\n                      Logic in Computer Science, LICS 08\n                      , pp. 229-240. IEEE Press, 2008.","DOI":"10.1109\/LICS.2008.39"},{"key":"10.2168\/LMCS-7(1:4)2011_CiabattoniTerui06","doi-asserted-by":"crossref","first-page":"95","DOI":"10.1007\/s11225-006-6607-2","volume":"82","author":"A. Ciabattoni and K. Terui","year":"2006","journal-title":"Stud. Log."},{"key":"10.2168\/LMCS-7(1:4)2011_Cross09","doi-asserted-by":"publisher","DOI":"10.1007\/s10670-008-9146-6"},{"key":"10.2168\/LMCS-7(1:4)2011_Gentzen34","doi-asserted-by":"crossref","first-page":"176","DOI":"10.1007\/BF01201353","volume":"39","author":"G. Gentzen","year":"1934","journal-title":"Math. Z."},{"key":"10.2168\/LMCS-7(1:4)2011_GiordanoSchwind04","doi-asserted-by":"crossref","first-page":"239","DOI":"10.1016\/j.artint.2004.04.009","volume":"157","author":"L. Giordano and C. Schwind","year":"2004","journal-title":"Artif. Intell."},{"key":"10.2168\/LMCS-7(1:4)2011_Gore:1999:TMM","doi-asserted-by":"crossref","unstructured":"R. Gor\u00e9. Tableau methods for modal and temporal logics. In M. D'Agostino, D. Gabbay, R. H\u00e4hnle, and J. Posegga, eds.,\n                      Handbook of Tableau Methods\n                      , pp. 297-396. Kluwer, 1999.","DOI":"10.1007\/978-94-017-1754-0_6"},{"key":"10.2168\/LMCS-7(1:4)2011_HeuerdingEA96","unstructured":"A. Heuerding, M. Seyfried, and H. Zimmermann. Efficient loop-check for backward proof search in some non-classical propositional logics. In\n                      Theorem Proving with Analytic Tableaux and Related Methods, TABLEAUX\n                      1996, vol. 1071 of\n                      LNCS\n                      , pp. 210-225. Springer, 1996."},{"key":"10.2168\/LMCS-7(1:4)2011_KrausLehmannMagidor90","doi-asserted-by":"crossref","first-page":"167","DOI":"10.1016\/0004-3702(90)90101-5","volume":"44","author":"S. Kraus, D. J. Lehmann, and M. Magidor","year":"1990","journal-title":"Artif. Intell."},{"key":"10.2168\/LMCS-7(1:4)2011_Ladner77","doi-asserted-by":"crossref","first-page":"467","DOI":"10.1137\/0206033","volume":"6","author":"R. Ladner","year":"1977","journal-title":"SIAM J. Comput."},{"issue":"4:22","key":"10.2168\/LMCS-7(1:4)2011_OlivettiEA07","first-page":"1","volume":"8","author":"N. Olivetti, G. L. Pozzato, and C. Schwi","year":"2007","journal-title":"ACM Trans. Comput. Logic"},{"key":"10.2168\/LMCS-7(1:4)2011_PattinsonSchroder10","unstructured":"D. Pattinson and L. Schr\u00f6der. Cut elimination in coalgebraic logics.\n                      Inform. Comput.\n                      To appear."},{"key":"10.2168\/LMCS-7(1:4)2011_PattinsonSchroder09","unstructured":"D. Pattinson and L. Schr\u00f6der. Generic modal cut elimination applied to conditional logics. In\n                      Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX 09\n                      , vol. 5607 of\n                      LNCS\n                      , pp. 280-294. Springer, 2009."},{"key":"10.2168\/LMCS-7(1:4)2011_Rasga07","doi-asserted-by":"crossref","first-page":"81","DOI":"10.1016\/j.apal.2007.08.001","volume":"149","author":"J. Rasga","year":"2007","journal-title":"Ann. Pure Appl. Logic"},{"key":"10.2168\/LMCS-7(1:4)2011_SchroderPattinson08d","unstructured":"L. Schr\u00f6der and D. Pattinson. Shallow models for non-iterative modal logics. In\n                      Advances in Artificial Intelligence, KI 2008\n                      , vol. 5243 of\n                      LNAI\n                      , pp. 324-331. Springer, 2008."},{"issue":"2:13","key":"10.2168\/LMCS-7(1:4)2011_SchroderPattinson09","first-page":"1","volume":"10","author":"L. Schr\u00f6der and D. Pattinson","year":"2009","journal-title":"ACM Trans. Comput. Logic"},{"key":"10.2168\/LMCS-7(1:4)2011_SchroderEA10","unstructured":"L. Schr\u00f6der, D. Pattinson, and D. Hausmann. Optimal tableaux for conditional logics with cautious monotonicity. In M. Wooldridge, ed.,\n                      European Conf. on Artificial Intelligence, ECAI 2010\n                      , vol. 215 of\n                      Frontiers in Artificial Intelligence and Applications\n                      , pp. 707-712. IOS Press, 2010."},{"key":"10.2168\/LMCS-7(1:4)2011_Vardi89","doi-asserted-by":"crossref","unstructured":"M. Vardi. On the complexity of epistemic reasoning. In\n                      Logic in Computer Science\n                      , pp. 243-251. IEEE, 1989.","DOI":"10.1109\/LICS.1989.39179"}],"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/968\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/968\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,11]],"date-time":"2025-03-11T17:26:25Z","timestamp":1741713985000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/968"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011,3,17]]},"references-count":20,"URL":"https:\/\/doi.org\/10.2168\/lmcs-7(1:4)2011","relation":{"is-same-as":[{"id-type":"arxiv","id":"1011.3479","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.1011.3479","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"value":"1860-5974","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011,3,17]]},"article-number":"968"}}