{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,10,6]],"date-time":"2024-10-06T00:49:35Z","timestamp":1728175775963},"reference-count":59,"publisher":"Elsevier BV","license":[{"start":{"date-parts":[[2016,12,1]],"date-time":"2016-12-01T00:00:00Z","timestamp":1480550400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2020,12,20]],"date-time":"2020-12-20T00:00:00Z","timestamp":1608422400000},"content-version":"vor","delay-in-days":1480,"URL":"http:\/\/www.elsevier.com\/open-access\/userlicense\/1.0\/"}],"funder":[{"DOI":"10.13039\/501100002428","name":"FWF","doi-asserted-by":"publisher","award":["START Y544-N23"],"id":[{"id":"10.13039\/501100002428","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100007601","name":"Horizon 2020","doi-asserted-by":"publisher","award":["660047"],"id":[{"id":"10.13039\/501100007601","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["elsevier.com","sciencedirect.com"],"crossmark-restriction":true},"short-container-title":["Theoretical Computer Science"],"published-print":{"date-parts":[[2016,12]]},"DOI":"10.1016\/j.tcs.2016.10.004","type":"journal-article","created":{"date-parts":[[2016,10,19]],"date-time":"2016-10-19T18:02:10Z","timestamp":1476900130000},"page":"76-105","update-policy":"http:\/\/dx.doi.org\/10.1016\/elsevier_cm_policy","source":"Crossref","is-referenced-by-count":15,"special_numbering":"PA","title":["Hypersequent rules with restricted contexts for propositional modal logics"],"prefix":"10.1016","volume":"656","author":[{"ORCID":"http:\/\/orcid.org\/0000-0002-5335-1838","authenticated-orcid":false,"given":"Bj\u00f6rn","family":"Lellmann","sequence":"first","affiliation":[]}],"member":"78","reference":[{"key":"10.1016\/j.tcs.2016.10.004_br0010","series-title":"Schnittfreie Tableau- und Sequenzenkalk\u00fcle f\u00fcr normale modale Aussagenlogiken","author":"Amerbauer","year":"1993"},{"key":"10.1016\/j.tcs.2016.10.004_br0020","doi-asserted-by":"crossref","first-page":"359","DOI":"10.1007\/BF00370840","article-title":"Cut-free tableau calculi for some propositional normal modal logics","volume":"57","author":"Amerbauer","year":"1996","journal-title":"Studia Logica"},{"issue":"3","key":"10.1016\/j.tcs.2016.10.004_br0030","doi-asserted-by":"crossref","first-page":"297","DOI":"10.1093\/logcom\/2.3.297","article-title":"Logic programming with focusing proofs in linear logic","volume":"2","author":"Andreoli","year":"1992","journal-title":"J. Logic Comput."},{"key":"10.1016\/j.tcs.2016.10.004_br0040","series-title":"Logic: From Foundations to Applications","article-title":"The method of hypersequents in the proof theory of propositional non-classical logics","author":"Avron","year":"1996"},{"key":"10.1016\/j.tcs.2016.10.004_br0050","series-title":"IJCAR 2001","first-page":"529","article-title":"Canonical propositional Gentzen-type systems","volume":"vol. 2083","author":"Avron","year":"2001"},{"issue":"6","key":"10.1016\/j.tcs.2016.10.004_br0060","doi-asserted-by":"crossref","first-page":"835","DOI":"10.1093\/logcom\/13.6.835","article-title":"Hypersequent calculi for G\u00f6del logics \u2013 a survey","volume":"13","author":"Baaz","year":"2003","journal-title":"J. Logic Comput."},{"key":"10.1016\/j.tcs.2016.10.004_br0070","doi-asserted-by":"crossref","first-page":"375","DOI":"10.1007\/BF00284976","article-title":"Display logic","volume":"11","author":"Belnap","year":"1982","journal-title":"J. Philos. Logic"},{"key":"10.1016\/j.tcs.2016.10.004_br0080","series-title":"TABLEAUX 2013","first-page":"44","article-title":"Bounded proofs and step frames","volume":"vol. 8123","author":"Bezhanishvili","year":"2013"},{"issue":"12","key":"10.1016\/j.tcs.2016.10.004_br0090","doi-asserted-by":"crossref","first-page":"1832","DOI":"10.1016\/j.apal.2014.07.005","article-title":"The bounded proof property via step algebras and step frames","volume":"165","author":"Bezhanishvili","year":"2014","journal-title":"Ann. Pure Appl. Logic"},{"key":"10.1016\/j.tcs.2016.10.004_br0100","series-title":"Advances in Modal Logic","first-page":"54","article-title":"Multiple-conclusion rules, hypersequents syntax and step frames","volume":"vol. 10","author":"Bezhanishvili","year":"2014"},{"key":"10.1016\/j.tcs.2016.10.004_br0110","series-title":"Modal Logic","author":"Blackburn","year":"2001"},{"key":"10.1016\/j.tcs.2016.10.004_br0120","doi-asserted-by":"crossref","first-page":"551","DOI":"10.1007\/s00153-009-0137-3","article-title":"Deep sequent systems for modal logic","volume":"48","author":"Br\u00fcnnler","year":"2009","journal-title":"Arch. Math. Logic"},{"issue":"1","key":"10.1016\/j.tcs.2016.10.004_br0130","doi-asserted-by":"crossref","first-page":"114","DOI":"10.1145\/322234.322243","article-title":"Alternation","volume":"28","author":"Chandra","year":"1981","journal-title":"J. ACM"},{"key":"10.1016\/j.tcs.2016.10.004_br0140","series-title":"FOSSACS 2016","first-page":"390","article-title":"Focused and synthetic nested sequents","volume":"vol. 9634","author":"Chaudhuri","year":"2016"},{"key":"10.1016\/j.tcs.2016.10.004_br0150","series-title":"Modal Logic","author":"Chellas","year":"1980"},{"key":"10.1016\/j.tcs.2016.10.004_br0160","series-title":"LICS 2008","first-page":"229","article-title":"From axioms to analytic rules in nonclassical logics","author":"Ciabattoni","year":"2008"},{"key":"10.1016\/j.tcs.2016.10.004_br0170","doi-asserted-by":"crossref","first-page":"266","DOI":"10.1016\/j.apal.2011.09.003","article-title":"Algebraic proof theory for substructural logics: cut-elimination and completions","volume":"163","author":"Ciabattoni","year":"2012","journal-title":"Ann. Pure Appl. Logic"},{"key":"10.1016\/j.tcs.2016.10.004_br0180","series-title":"LFCS 2013","first-page":"119","article-title":"Automated support for the investigation of paraconsistent and other logics","volume":"vol. 7734","author":"Ciabattoni","year":"2013"},{"key":"10.1016\/j.tcs.2016.10.004_br0190","series-title":"TABLEAUX 2013","first-page":"81","article-title":"Hypersequent and labelled calculi for intermediate logics","volume":"vol. 8123","author":"Ciabattoni","year":"2013"},{"key":"10.1016\/j.tcs.2016.10.004_br0200","doi-asserted-by":"crossref","first-page":"369","DOI":"10.1016\/j.fss.2009.09.001","article-title":"Algebraic and proof-theoretic characterizations of truth stressers for MTL and its extensions","volume":"161","author":"Ciabattoni","year":"2010","journal-title":"Fuzzy Sets and Systems"},{"key":"10.1016\/j.tcs.2016.10.004_br0210","series-title":"WoLLIC 2013","first-page":"81","article-title":"Structural extensions of display calculi: a general recipe","volume":"vol. 8071","author":"Ciabattoni","year":"2013"},{"key":"10.1016\/j.tcs.2016.10.004_br0220","doi-asserted-by":"crossref","first-page":"95","DOI":"10.1007\/s11225-006-6607-2","article-title":"Towards a semantic characterization of cut-elimination","volume":"82","author":"Ciabattoni","year":"2006","journal-title":"Studia Logica"},{"key":"10.1016\/j.tcs.2016.10.004_br0230","doi-asserted-by":"crossref","first-page":"713","DOI":"10.1007\/s11225-013-9496-1","article-title":"The proof by cases property and its variants in structural consequence relations","volume":"101","author":"Cintula","year":"2013","journal-title":"Studia Logica"},{"key":"10.1016\/j.tcs.2016.10.004_br0240","series-title":"TABLEAUX 2000","first-page":"190","article-title":"Complexity of simple dependent bimodal logics","volume":"vol. 1847","author":"Demri","year":"2000"},{"issue":"3","key":"10.1016\/j.tcs.2016.10.004_br0250","doi-asserted-by":"crossref","first-page":"291","DOI":"10.1016\/j.apal.2011.09.004","article-title":"Prefixed tableaus and nested sequents","volume":"163","author":"Fitting","year":"2012","journal-title":"Ann. Pure Appl. Logic"},{"key":"10.1016\/j.tcs.2016.10.004_br0260","article-title":"First-Order Modal Logic","volume":"vol. 277","author":"Fitting","year":"1998"},{"issue":"2","key":"10.1016\/j.tcs.2016.10.004_br0270","first-page":"176","article-title":"Untersuchungen \u00fcber das logische Schlie\u00dfen, I","volume":"39","author":"Gentzen","year":"1934","journal-title":"Math. Z."},{"issue":"2","key":"10.1016\/j.tcs.2016.10.004_br0280","doi-asserted-by":"crossref","first-page":"859","DOI":"10.2307\/2586506","article-title":"Unification in intuitionistic logic","volume":"64","author":"Ghilardi","year":"1999","journal-title":"J. Symbolic Logic"},{"key":"10.1016\/j.tcs.2016.10.004_br0290","series-title":"A New Introduction to Modal Logic","author":"Hughes","year":"1996"},{"key":"10.1016\/j.tcs.2016.10.004_br0300","first-page":"89","article-title":"Cut-free hypersequent calculus for S4.3","volume":"41","author":"Indrzejczak","year":"2012","journal-title":"Bull. Sec. Logic"},{"key":"10.1016\/j.tcs.2016.10.004_br0310","doi-asserted-by":"crossref","first-page":"75","DOI":"10.1016\/j.ipl.2014.07.002","article-title":"Eliminability of cut in hypersequent calculi for some modal logics of linear frames","volume":"115","author":"Indrzejczak","year":"2015","journal-title":"Inform. Process. Lett."},{"issue":"4","key":"10.1016\/j.tcs.2016.10.004_br0320","doi-asserted-by":"crossref","first-page":"411","DOI":"10.1093\/logcom\/exi029","article-title":"Admissible rules of modal logics","volume":"15","author":"Je\u0159\u00e1bek","year":"2005","journal-title":"J. Logic Comput."},{"issue":"1","key":"10.1016\/j.tcs.2016.10.004_br0330","doi-asserted-by":"crossref","first-page":"119","DOI":"10.1007\/BF01053026","article-title":"Cut-free sequent calculi for some tense logics","volume":"53","author":"Kashima","year":"1994","journal-title":"Studia Logica"},{"key":"10.1016\/j.tcs.2016.10.004_br0340","series-title":"Introduction to Metamathematics","author":"Kleene","year":"1952"},{"key":"10.1016\/j.tcs.2016.10.004_br0350","series-title":"Proof Theory of Modal Logic","first-page":"93","article-title":"Power and weakness of the modal display calculus","author":"Kracht","year":"1996"},{"key":"10.1016\/j.tcs.2016.10.004_br0360","series-title":"New Frontiers in Artificial Intelligence","first-page":"51","article-title":"Hypersequent calculi for modal logics extending S4","volume":"vol. 8417","author":"Kurokawa","year":"2014"},{"key":"10.1016\/j.tcs.2016.10.004_br0370","series-title":"LICS 2013","article-title":"From frame properties to hypersequent rules in modal logics","author":"Lahav","year":"2013"},{"key":"10.1016\/j.tcs.2016.10.004_br0380","series-title":"Sequent Calculi with Context Restrictions and Applications to Conditional Logic","author":"Lellmann","year":"2013"},{"key":"10.1016\/j.tcs.2016.10.004_br0390","series-title":"IJCAR 2014","first-page":"307","article-title":"Axioms vs hypersequent rules with context restrictions: theory and applications","volume":"vol. 8562","author":"Lellmann","year":"2014"},{"key":"10.1016\/j.tcs.2016.10.004_br0400","series-title":"ICLA 2013","first-page":"148","article-title":"Constructing cut free sequent systems with context restrictions based on classical or intuitionistic logic","volume":"vol. 7750","author":"Lellmann","year":"2013"},{"key":"10.1016\/j.tcs.2016.10.004_br0410","series-title":"TABLEAUX 2013","first-page":"219","article-title":"Correspondence between modal Hilbert axioms and sequent rules with an application to S5","volume":"vol. 8123","author":"Lellmann","year":"2013"},{"key":"10.1016\/j.tcs.2016.10.004_br0420","series-title":"LPAR-20 2015","first-page":"558","article-title":"Proof search in nested sequent calculi","author":"Lellmann","year":"2015"},{"key":"10.1016\/j.tcs.2016.10.004_br0430","series-title":"Advances in Modal Logic","first-page":"387","article-title":"Label-free modular systems for classical and intuitionistic modal logics","volume":"vol. 10","author":"Marin","year":"2014"},{"key":"10.1016\/j.tcs.2016.10.004_br0440","article-title":"Proof Theory for Fuzzy Logics","volume":"vol. 36","author":"Metcalfe","year":"2008"},{"key":"10.1016\/j.tcs.2016.10.004_br0450","series-title":"Modal Logic","first-page":"422","article-title":"Sistemy Lyuisa i sistema T (Supplement to the Russian translation)","author":"Mints","year":"1974"},{"key":"10.1016\/j.tcs.2016.10.004_br0460","series-title":"Selected Papers in Proof Theory","first-page":"221","article-title":"Lewis' systems and system T","volume":"vol. 3","author":"Mints","year":"1992"},{"key":"10.1016\/j.tcs.2016.10.004_br0470","doi-asserted-by":"crossref","first-page":"507","DOI":"10.1007\/s10992-005-2267-3","article-title":"Proof analysis in modal logic","volume":"34","author":"Negri","year":"2005","journal-title":"J. Philos. Logic"},{"key":"10.1016\/j.tcs.2016.10.004_br0480","first-page":"34","article-title":"Logic engineering: Konstruktion von Logiken","volume":"3","author":"Ohlbach","year":"1992","journal-title":"KI"},{"key":"10.1016\/j.tcs.2016.10.004_br0490","series-title":"Computational Complexity","author":"Papadimitriou","year":"1994"},{"issue":"12","key":"10.1016\/j.tcs.2016.10.004_br0500","doi-asserted-by":"crossref","first-page":"1447","DOI":"10.1016\/j.ic.2009.11.008","article-title":"Cut elimination in coalgebraic logics","volume":"208","author":"Pattinson","year":"2010","journal-title":"Inform. and Comput."},{"issue":"1","key":"10.1016\/j.tcs.2016.10.004_br0510","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1017\/S1755020308080040","article-title":"A cut-free simple sequent calculus for modal logic S5","volume":"1","author":"Poggiolesi","year":"2008","journal-title":"Rev. Symb. Log."},{"key":"10.1016\/j.tcs.2016.10.004_br0520","article-title":"Gentzen Calculi for Modal Propositional Logic","volume":"vol. 32","author":"Poggiolesi","year":"2011"},{"issue":"3","key":"10.1016\/j.tcs.2016.10.004_br0530","first-page":"900","article-title":"Uniform, cut-free formulations of T, S4 and S5 (abstract)","volume":"48","author":"Pottinger","year":"1983","journal-title":"J. Symbolic Logic"},{"key":"10.1016\/j.tcs.2016.10.004_br0540","series-title":"Logic Colloquium 2005","first-page":"151","article-title":"Proofnets for S5: sequents and circuits for modal logic","volume":"vol. 28","author":"Restall","year":"2007"},{"key":"10.1016\/j.tcs.2016.10.004_br0550","series-title":"DEON 2012","first-page":"139","article-title":"The logic of obligation as weakest permission","volume":"vol. 7393","author":"Roy","year":"2012"},{"issue":"1\u20132","key":"10.1016\/j.tcs.2016.10.004_br0560","doi-asserted-by":"crossref","first-page":"97","DOI":"10.1016\/j.jlap.2006.11.004","article-title":"A finite model construction for coalgebraic modal logic","volume":"73","author":"Schr\u00f6der","year":"2007","journal-title":"J. Log. Algebr. Program."},{"key":"10.1016\/j.tcs.2016.10.004_br0570","first-page":"1129","article-title":"Subformula property as a substitute for cut-elimination in modal propositional logics","volume":"37","author":"Takano","year":"1992","journal-title":"Math. Jpn."},{"key":"10.1016\/j.tcs.2016.10.004_br0580","series-title":"Labelled Non-Classical Logics","author":"Vigan\u00f2","year":"2000"},{"key":"10.1016\/j.tcs.2016.10.004_br0590","series-title":"Handbook of Philosophical Logic","article-title":"Sequent systems for modal logics","volume":"vol. 8","author":"Wansing","year":"2002"}],"container-title":["Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0304397516305187?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0304397516305187?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2020,12,19]],"date-time":"2020-12-19T22:05:03Z","timestamp":1608415503000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S0304397516305187"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,12]]},"references-count":59,"alternative-id":["S0304397516305187"],"URL":"https:\/\/doi.org\/10.1016\/j.tcs.2016.10.004","relation":{},"ISSN":["0304-3975"],"issn-type":[{"value":"0304-3975","type":"print"}],"subject":[],"published":{"date-parts":[[2016,12]]},"assertion":[{"value":"Elsevier","name":"publisher","label":"This article is maintained by"},{"value":"Hypersequent rules with restricted contexts for propositional modal logics","name":"articletitle","label":"Article Title"},{"value":"Theoretical Computer Science","name":"journaltitle","label":"Journal Title"},{"value":"https:\/\/doi.org\/10.1016\/j.tcs.2016.10.004","name":"articlelink","label":"CrossRef DOI link to publisher maintained version"},{"value":"article","name":"content_type","label":"Content Type"},{"value":"\u00a9 2016 Elsevier B.V.","name":"copyright","label":"Copyright"}]}}