{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,8,18]],"date-time":"2024-08-18T13:40:04Z","timestamp":1723988404766},"reference-count":41,"publisher":"Oxford University Press (OUP)","issue":"1","license":[{"start":{"date-parts":[[2020,12,29]],"date-time":"2020-12-29T00:00:00Z","timestamp":1609200000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/academic.oup.com\/journals\/pages\/open_access\/funder_policies\/chorus\/standard_publication_model"}],"funder":[{"name":"ANR project TICAMORE","award":["ANR-16-CE91-0002-01"]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021,1,22]]},"abstract":"Abstract<\/jats:title>We present some hypersequent calculi for all systems of the classical cube and their extensions with axioms ${T}$, ${P}$ and ${D}$ and for every $n \\geq 1$, rule ${RD}_n^+$. The calculi are internal as they only employ the language of the logic, plus additional structural connectives. We show that the calculi are complete with respect to the corresponding axiomatization by a syntactic proof of cut elimination. Then, we define a terminating proof search strategy in the hypersequent calculi and show that it is optimal for coNP-complete logics. Moreover, we show that from every failed proof of a formula or hypersequent it is possible to directly extract a countermodel of it in the bi-neighbourhood semantics of polynomial size for coNP logics, and for regular logics also in the relational semantics. We finish the paper by giving a translation between hypersequent rule applications and derivations in a labelled system for the classical cube.<\/jats:p>","DOI":"10.1093\/logcom\/exaa072","type":"journal-article","created":{"date-parts":[[2020,12,3]],"date-time":"2020-12-03T12:38:51Z","timestamp":1606999131000},"page":"67-111","source":"Crossref","is-referenced-by-count":5,"title":["Hypersequent calculi for non-normal modal and deontic logics: countermodels and optimal complexity"],"prefix":"10.1093","volume":"31","author":[{"given":"Tiziano","family":"Dalmonte","sequence":"first","affiliation":[{"name":"Aix-Marseille University, Universit\u00e9 de Toulon, CNRS, LIS, Marseille 13013, France"}]},{"given":"Bj\u00f6rn","family":"Lellmann","sequence":"additional","affiliation":[{"name":"Technische Universit\u00e4t Wien, Vienna 1040, Austria"}]},{"given":"Nicola","family":"Olivetti","sequence":"additional","affiliation":[{"name":"Aix-Marseille University, Universit\u00e9 de Toulon, CNRS, LIS, Marseille 13013, France"}]},{"given":"Elaine","family":"Pimentel","sequence":"additional","affiliation":[{"name":"Departamento de Matem\u00e1tica, UFRN, Natal 59.078-970, Brazil"}]}],"member":"286","published-online":{"date-parts":[[2020,12,29]]},"reference":[{"key":"2021032411480274800_ref1","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-33353-8_4","article-title":"Knowledge means \u2018all\u2019, belief means \u2018most\u2019","volume-title":"Logics in Artificial Intelligence, 13th European Conference, JELIA 2012","author":"Askounis","year":"2012"},{"key":"2021032411480274800_ref2","doi-asserted-by":"crossref","DOI":"10.1093\/oso\/9780198538622.003.0001","article-title":"The method of hypersequents in the proof theory of propositional non-classical logics","volume-title":"Logic: From Foundations to Applications, pp. 1\u201332","author":"Avron","year":"1996"},{"key":"2021032411480274800_ref3","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9781107050884","volume-title":"Modal Logic","author":"Blackburn","year":"2001"},{"key":"2021032411480274800_ref4","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511621192","volume-title":"Modal Logic: An Introduction","author":"Chellas","year":"1980"},{"key":"2021032411480274800_ref5","doi-asserted-by":"crossref","DOI":"10.1109\/LICS.2008.39","article-title":"From axioms to analytic rules in nonclassical logics","volume-title":"Proceedings of the 23rd Annual IEEE Symposium on Logic in Computer Science, LICS 2008","author":"Ciabattoni","year":"2008"},{"key":"2021032411480274800_ref6","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-40537-2_9","article-title":"Hypersequent and labelled calculi for intermediate logics","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods, 22th International Conference, TABLEAUX 2013","author":"Ciabattoni","year":"2013"},{"volume-title":"Non-Normal Modal Logics: Neighbourhood Semantics and their Calculi","year":"2020","author":"Dalmonte","key":"2021032411480274800_ref7"},{"key":"2021032411480274800_ref8","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-030-36755-8_3","article-title":"Countermodel construction via optimal hypersequent calculi for non-normal modal logics","volume-title":"Logical Foundations of Computer Science, International Symposium, LFCS 2020","author":"Dalmonte","year":"2020"},{"key":"2021032411480274800_ref9","article-title":"Non-normal modal logics: Bi-neighbourhood semantics and its labelled calculi","volume-title":"Advances in Modal Logic 12, Proceedings of the 12th Conference on Advances in Modal Logic","author":"Dalmonte","year":"2018"},{"key":"2021032411480274800_ref10","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-030-51054-1_23","article-title":"HYPNO: Theorem proving with hypersequent calculi for non-normal modal logics (system description)","volume-title":"Automated Reasoning, 10th International Joint Conference, IJCAR 2020","author":"Dalmonte","year":"2020"},{"key":"2021032411480274800_ref11","first-page":"1","article-title":"The modal logic of agency","volume":"2","author":"Elgesem","year":"1997","journal-title":"Nordic Journal of Philosophical Logic"},{"key":"2021032411480274800_ref12","doi-asserted-by":"crossref","DOI":"10.1007\/978-94-017-2794-5","article-title":"Proof methods for modal and intuitionistic logics","volume-title":"Number 169 in Synthese Library","author":"Fitting","year":"1983"},{"key":"2021032411480274800_ref13","doi-asserted-by":"crossref","first-page":"91","DOI":"10.1016\/0743-1066(91)90014-G","article-title":"Bilattices and the semantics of logic programming","volume":"11","author":"Fitting","year":"1991","journal-title":"The Journal of Logic Programming"},{"key":"2021032411480274800_ref14","article-title":"Investigations into logical deduction","volume-title":"The Collected Papers of Gerhard Gentzen","author":"Gentzen","year":"1969"},{"key":"2021032411480274800_ref15","doi-asserted-by":"crossref","first-page":"175","DOI":"10.1007\/s11225-014-9556-1","article-title":"Modular sequent calculi for classical modal logics","volume":"103","author":"Gilbert","year":"2015","journal-title":"Studia Logica"},{"key":"2021032411480274800_ref16","doi-asserted-by":"crossref","first-page":"265","DOI":"10.1111\/j.1467-8640.1988.tb00280.x","article-title":"Multivalued logics: A uniform approach to reasoning in artificial intelligence","volume":"4","author":"Ginsberg","year":"1988","journal-title":"Computational Intelligence"},{"key":"2021032411480274800_ref17","article-title":"Counterfactual logic: Labelled and internal calculi, two sides of the same coin?","volume-title":"Advances in Modal Logic 12, Proceedings of the 12th Conference on Advances in Modal Logic","author":"Girlando","year":"2018"},{"key":"2021032411480274800_ref18","doi-asserted-by":"crossref","first-page":"143","DOI":"10.1023\/A:1015071400913","article-title":"Sat-based decision procedures for classical modal logics","volume":"28","author":"Giunchiglia","year":"2002","journal-title":"Journal of Automated Reasoning"},{"key":"2021032411480274800_ref19","first-page":"241","article-title":"Prima facie norms, normative conflicts, and dilemmas","volume":"1","author":"Goble","year":"2013","journal-title":"Handbook of Deontic Logic and Normative Systems"},{"key":"2021032411480274800_ref20","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-319-77434-3_1","article-title":"Formalization","volume-title":"Introduction to Formal Philosophy","author":"Hansson","year":"2018"},{"key":"2021032411480274800_ref21","first-page":"151","article-title":"Sequent calculi for monotonic modal logics","volume":"34","author":"Indrzejczak","year":"2005","journal-title":"Bulletin of the Section of logic"},{"key":"2021032411480274800_ref22","first-page":"189","article-title":"Admissibility of cut in congruent modal logics","volume":"20","author":"Indrzejczak","year":"2011","journal-title":"Logic and Logical Philosophy"},{"key":"2021032411480274800_ref23","article-title":"Semantical analysis of modal logic ii. Non-normal modal propositional calculi","volume-title":"The Theory of Models, pp. 206\u2013220","author":"Kripke","year":"1965"},{"key":"2021032411480274800_ref24","doi-asserted-by":"crossref","first-page":"1369","DOI":"10.1016\/j.apal.2018.08.007","article-title":"Multicomponent proof-theoretic method for proving interpolation properties","volume":"169","author":"Kuznets","year":"2018","journal-title":"Annals of Pure and Applied Logic"},{"key":"2021032411480274800_ref25","doi-asserted-by":"crossref","first-page":"121","DOI":"10.1023\/A:1026753129680","article-title":"Sequent calculi and decision procedures for weak modal systems","volume":"65","author":"Lavendhomme","year":"2000","journal-title":"Studia Logica"},{"key":"2021032411480274800_ref26","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-030-29026-9_12","article-title":"Combining monotone and normal modal logic in nested sequents - with countermodels","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods, 28th International Conference, TABLEAUX 2019","author":"Lellmann","year":"2019"},{"key":"2021032411480274800_ref27","doi-asserted-by":"crossref","first-page":"7:1","DOI":"10.1145\/3288757","article-title":"Modularisation of sequent calculi for normal and non-normal modalities","volume":"20","author":"Lellmann","year":"2019","journal-title":"ACM Transactions on Computational Logic (TOCL)"},{"key":"2021032411480274800_ref28","doi-asserted-by":"crossref","first-page":"4747","DOI":"10.1016\/j.tcs.2009.07.041","article-title":"Focusing and polarization in linear, intuitionistic, and classical logics","volume":"410","author":"Liang","year":"2009","journal-title":"Theoretical Computer Science"},{"key":"2021032411480274800_ref29","first-page":"1241","article-title":"Proof theory for non-normal modal logics: The neighbourhood formalism and basic results","volume":"4","author":"Negri","year":"2017","journal-title":"IfCoLog Journal of Logics and Their Applications"},{"journal-title":"Logic and Logical Philosophy","article-title":"Sequent calculi and interpolation for non-normal modal and deontic logics","author":"Orlandelli","key":"2021032411480274800_ref30"},{"key":"2021032411480274800_ref31","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-319-08615-6_11","article-title":"Proof analysis in deontic logics","volume-title":"Deontic Logic and Normative Systems - 12th International Conference, DEON 2014","author":"Orlandelli","year":"2014"},{"key":"2021032411480274800_ref32","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-319-67149-9","volume-title":"Neighborhood Semantics for Modal Logic","author":"Pacuit","year":"2017"},{"key":"2021032411480274800_ref33","doi-asserted-by":"crossref","DOI":"10.1109\/LICS.2013.48","article-title":"The logic of exact covers: Completeness and uniform interpolation","volume-title":"28th Annual ACM\/IEEE Symposium on Logic in Computer Science, LICS 2013","author":"Pattinson","year":"2013"},{"key":"2021032411480274800_ref34","doi-asserted-by":"crossref","first-page":"149","DOI":"10.1093\/logcom\/12.1.149","article-title":"A modal logic for coalitional power in games","volume":"12","author":"Pauly","year":"2002","journal-title":"Journal of Logic and Computation"},{"key":"2021032411480274800_ref35","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511801174","volume-title":"An Introduction to Non-classical Logic: From If To Is","author":"Priest","year":"2008"},{"key":"2021032411480274800_ref36","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-540-85845-4_40","article-title":"Shallow models for non-iterative modal logics","volume-title":"KI 2008: Advances in Artificial Intelligence, 31st Annual German Conference on AI, KI 2008","author":"Schr\u00f6der","year":"2008"},{"key":"2021032411480274800_ref37","article-title":"Uniform interpolation in coalgebraic modal logic","volume-title":"7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017), Leibniz International Proceedings in Informatics, pp. 21:1\u201321:16","author":"Seifan","year":"2017"},{"volume-title":"The Proof Theory and Semantics of Intuitionistic Modal Logic","year":"1994","author":"Simpson","key":"2021032411480274800_ref38"},{"key":"2021032411480274800_ref39","doi-asserted-by":"crossref","DOI":"10.1016\/B978-0-934613-04-0.50024-7","article-title":"On epistemic logic and logical omniscience","volume-title":"Proceedings of the 1st Conference on Theoretical Aspects of Reasoning about Knowledge","author":"Vardi","year":"1986"},{"key":"2021032411480274800_ref40","doi-asserted-by":"crossref","DOI":"10.1109\/LICS.1989.39179","article-title":"On the complexity of epistemic reasoning","volume-title":"Proceedings of the Fourth Annual Symposium on Logic in Computer Science (LICS \u201989)","author":"Vardi","year":"1989"},{"key":"2021032411480274800_ref41","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4757-3208-5","volume-title":"Labelled Non-classical Logics","author":"Vigan\u00f2","year":"2000"}],"container-title":["Journal of Logic and Computation"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/academic.oup.com\/logcom\/article-pdf\/31\/1\/67\/36677685\/exaa072.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"http:\/\/academic.oup.com\/logcom\/article-pdf\/31\/1\/67\/36677685\/exaa072.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,8,18]],"date-time":"2024-08-18T13:14:04Z","timestamp":1723986844000},"score":1,"resource":{"primary":{"URL":"https:\/\/academic.oup.com\/logcom\/article\/31\/1\/67\/6054064"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,12,29]]},"references-count":41,"journal-issue":{"issue":"1","published-online":{"date-parts":[[2020,12,29]]},"published-print":{"date-parts":[[2021,1,22]]}},"URL":"https:\/\/doi.org\/10.1093\/logcom\/exaa072","relation":{},"ISSN":["0955-792X","1465-363X"],"issn-type":[{"type":"print","value":"0955-792X"},{"type":"electronic","value":"1465-363X"}],"subject":[],"published-other":{"date-parts":[[2021,1]]},"published":{"date-parts":[[2020,12,29]]}}}