{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,20]],"date-time":"2025-11-20T12:28:19Z","timestamp":1763641699639},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642405365"},{"type":"electronic","value":"9783642405372"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-40537-2_19","type":"book-chapter","created":{"date-parts":[[2013,9,11]],"date-time":"2013-09-11T12:33:51Z","timestamp":1378902831000},"page":"219-233","source":"Crossref","is-referenced-by-count":8,"title":["Correspondence between Modal Hilbert Axioms and Sequent Rules with an Application to S5"],"prefix":"10.1007","author":[{"given":"Bj\u00f6rn","family":"Lellmann","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Dirk","family":"Pattinson","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"19_CR1","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1007\/978-3-642-22119-4_6","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"A. Avron","year":"2011","unstructured":"Avron, A., Lahav, O.: Kripke semantics for basic sequent systems. In: Br\u00fcnnler, K., Metcalfe, G. (eds.) TABLEAUX 2011. LNCS (LNAI), vol.\u00a06793, pp. 43\u201357. Springer, Heidelberg (2011)"},{"key":"19_CR2","doi-asserted-by":"crossref","unstructured":"Blackburn, P., de Rijke, M., Venema, Y.: Modal Logic. Cambridge University Press (2001)","DOI":"10.1017\/CBO9781107050884"},{"key":"19_CR3","doi-asserted-by":"publisher","first-page":"551","DOI":"10.1007\/s00153-009-0137-3","volume":"48","author":"K. Br\u00fcnnler","year":"2009","unstructured":"Br\u00fcnnler, K.: Deep sequent systems for modal logic. Arch. Math. Log.\u00a048, 551\u2013577 (2009)","journal-title":"Arch. Math. Log."},{"key":"19_CR4","doi-asserted-by":"crossref","unstructured":"Chellas, B.F.: Modal Logic. Cambridge University Press (1980)","DOI":"10.1017\/CBO9780511621192"},{"key":"19_CR5","doi-asserted-by":"publisher","first-page":"266","DOI":"10.1016\/j.apal.2011.09.003","volume":"163","author":"A. Ciabattoni","year":"2012","unstructured":"Ciabattoni, A., Galatos, N., Terui, K.: Algebraic proof theory for substructural logics: Cut-elimination and completions. Ann. Pure Appl. Logic\u00a0163, 266\u2013290 (2012)","journal-title":"Ann. Pure Appl. Logic"},{"key":"19_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"119","DOI":"10.1007\/978-3-642-35722-0_9","volume-title":"Logical Foundations of Computer Science","author":"A. Ciabattoni","year":"2013","unstructured":"Ciabattoni, A., Lahav, O., Spendier, L., Zamansky, A.: Automated support for the investigation of paraconsistent and other logics. In: Artemov, S., Nerode, A. (eds.) LFCS 2013. LNCS, vol.\u00a07734, pp. 119\u2013133. Springer, Heidelberg (2013)"},{"issue":"2","key":"19_CR7","first-page":"176","volume":"39","author":"G. Gentzen","year":"1934","unstructured":"Gentzen, G.: Untersuchungen \u00fcber das logische Schlie\u00dfen. I. Math. Z.\u00a039(2), 176\u2013210 (1934)","journal-title":"I. Math. Z."},{"issue":"2","key":"19_CR8","doi-asserted-by":"publisher","first-page":"859","DOI":"10.2307\/2586506","volume":"64","author":"S. Ghilardi","year":"1999","unstructured":"Ghilardi, S.: Unification in intuitionistic logic. J. Symb. Log.\u00a064(2), 859\u2013880 (1999)","journal-title":"J. Symb. Log."},{"key":"19_CR9","doi-asserted-by":"publisher","first-page":"433","DOI":"10.1007\/BF01057938","volume":"53","author":"R. Gor\u00e9","year":"1994","unstructured":"Gor\u00e9, R.: Cut-free sequent and tableau systems for propositional diodorean modal logics. Studia Logica\u00a053, 433\u2013457 (1994)","journal-title":"Studia Logica"},{"key":"19_CR10","doi-asserted-by":"crossref","unstructured":"Kracht, M.: Power and weakness of the modal display calculus. In: Wansing, H. (ed.) Proof Theory of Modal Logic, pp. 93\u2013121. Kluwer (1996)","DOI":"10.1007\/978-94-017-2798-3_7"},{"key":"19_CR11","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"211","DOI":"10.1007\/978-3-642-22119-4_17","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"B. Lellmann","year":"2011","unstructured":"Lellmann, B., Pattinson, D.: Cut elimination for shallow modal logics. In: Br\u00fcnnler, K., Metcalfe, G. (eds.) TABLEAUX 2011. LNCS (LNAI), vol.\u00a06793, pp. 211\u2013225. Springer, Heidelberg (2011)"},{"key":"19_CR12","doi-asserted-by":"crossref","unstructured":"Lellmann, B., Pattinson, D.: Constructing cut free sequent systems with context restrictions based on classical or intuitionistic logic. In: Lodaya, K. (ed.) ICLA 2013. LNCS (LNAI), vol.\u00a07750, pp. 148\u2013160. Springer, Heidelberg (2013)","DOI":"10.1007\/978-3-642-36039-8_14"},{"key":"19_CR13","doi-asserted-by":"publisher","first-page":"507","DOI":"10.1007\/s10992-005-2267-3","volume":"34","author":"S. Negri","year":"2005","unstructured":"Negri, S.: Proof analysis in modal logic. J. Philos. Logic\u00a034, 507\u2013544 (2005)","journal-title":"J. Philos. Logic"},{"key":"19_CR14","doi-asserted-by":"crossref","unstructured":"Negri, S., von Plato, J.: Structural proof theory. Cambridge University Press (2001)","DOI":"10.1017\/CBO9780511527340"},{"key":"19_CR15","doi-asserted-by":"crossref","unstructured":"Poggiolesi, F.: Gentzen Calculi for Modal Propositional Logic. Trends in Logic, vol.\u00a032. Springer, Heidelberg (2011)","DOI":"10.1007\/978-90-481-9670-8"},{"key":"19_CR16","doi-asserted-by":"crossref","unstructured":"Troelstra, A.S., Schwichtenberg, H.: Basic Proof Theory. Cambridge Tracts in Theoretical Computer Science, 2nd edn., vol.\u00a043. Cambridge University Press (2000)","DOI":"10.1017\/CBO9781139168717"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning with Analytic Tableaux and Related Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-40537-2_19","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,3,6]],"date-time":"2022-03-06T01:01:18Z","timestamp":1646528478000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-40537-2_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642405365","9783642405372"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-40537-2_19","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}