{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,20]],"date-time":"2025-11-20T12:33:21Z","timestamp":1763642001726},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783662488980"},{"type":"electronic","value":"9783662488997"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-662-48899-7_39","type":"book-chapter","created":{"date-parts":[[2015,11,21]],"date-time":"2015-11-21T03:59:28Z","timestamp":1448078368000},"page":"558-574","source":"Crossref","is-referenced-by-count":7,"title":["Proof Search in Nested Sequent Calculi"],"prefix":"10.1007","author":[{"given":"Bj\u00f6rn","family":"Lellmann","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Elaine","family":"Pimentel","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2015,11,22]]},"reference":[{"issue":"3","key":"39_CR1","doi-asserted-by":"publisher","first-page":"297","DOI":"10.1093\/logcom\/2.3.297","volume":"2","author":"JM Andreoli","year":"1992","unstructured":"Andreoli, J.M.: Logic programming with focusing proofs in linear logic. J. Logic Comput. 2(3), 297\u2013347 (1992)","journal-title":"J. Logic Comput."},{"key":"39_CR2","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. 48, 551\u2013577 (2009)","journal-title":"Arch. Math. Log."},{"key":"39_CR3","unstructured":"Chaudhuri, K., Guenot, N., Stra\u00dfburger, L.: The focused calculus of structures. In: Bezem, M. (ed.) CSL 2011, pp. 159\u2013173. Leibniz International Proceedings in Informatics (2011)"},{"key":"39_CR4","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511621192","volume-title":"Modal Logic","author":"BF Chellas","year":"1980","unstructured":"Chellas, B.F.: Modal Logic. Cambridge University Press, Cambridge (1980)"},{"key":"39_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"190","DOI":"10.1007\/10722086_17","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"S Demri","year":"2000","unstructured":"Demri, S.: Complexity of simple dependent bimodal logics. In: Dyckhoff, R. (ed.) TABLEAUX 2000. LNCS, vol. 1847, pp. 190\u2013204. Springer, Heidelberg (2000)"},{"key":"39_CR6","unstructured":"Gor\u00e9, R., Ramanayake, R.: Labelled tree sequents, tree hypersequents and nested (deep) sequents. In: AiML, vol. 9, pp. 279\u2013299 (2012)"},{"key":"39_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"54","DOI":"10.1007\/3-540-44802-0_5","volume-title":"Computer Science Logic","author":"A Guglielmi","year":"2001","unstructured":"Guglielmi, A., Stra\u00dfburger, L.: Non-commutativity and MELL in the calculus of structures. In: Fribourg, L. (ed.) CSL 2001. LNCS, vol. 2142, pp. 54\u201368. Springer, Heidelberg (2001)"},{"key":"39_CR8","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1023\/A:1026753129680","volume":"65","author":"R Lavendhomme","year":"2000","unstructured":"Lavendhomme, R., Lucas, T.: Sequent calculi and decision procedures for weak modal systems. Studia Logica 65, 121\u2013145 (2000)","journal-title":"Studia Logica"},{"key":"39_CR9","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1007\/978-3-319-24312-2_10","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"B Lellmann","year":"2015","unstructured":"Lellmann, B.: Linear nested sequents, 2-sequents and hypersequents. In: De Nivelle, H. (ed.) TABLEAUX 2015. LNCS (LNAI), vol. 9323, pp. 135\u2013150. Springer, Heidelberg (2015)"},{"key":"39_CR10","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"148","DOI":"10.1007\/978-3-642-36039-8_14","volume-title":"Logic and Its Applications","author":"B Lellmann","year":"2013","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. 7750, pp. 148\u2013160. Springer, Heidelberg (2013)"},{"key":"39_CR11","doi-asserted-by":"publisher","first-page":"229","DOI":"10.1016\/0168-0072(92)90029-Y","volume":"58","author":"A Masini","year":"1992","unstructured":"Masini, A.: 2-sequent calculus: a proof theory of modalities. Ann. Pure Appl. Logic 58, 229\u2013246 (1992)","journal-title":"Ann. Pure Appl. Logic"},{"key":"39_CR12","doi-asserted-by":"publisher","first-page":"1465","DOI":"10.1016\/j.ic.2011.10.003","volume":"209","author":"M Mendler","year":"2011","unstructured":"Mendler, M., Scheele, S.: Cut-free Gentzen calculus for multimodal CK. Inf. Comput. (IANDC) 209, 1465\u20131490 (2011)","journal-title":"Inf. Comput. (IANDC)"},{"key":"39_CR13","doi-asserted-by":"publisher","first-page":"98","DOI":"10.1016\/j.tcs.2012.12.008","volume":"474","author":"D Miller","year":"2013","unstructured":"Miller, D., Pimentel, E.: A formal framework for specifying sequent calculus proof systems. Theor. Comput. Sci. 474, 98\u2013116 (2013)","journal-title":"Theor. Comput. Sci."},{"key":"39_CR14","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139003513","volume-title":"Proof Analysis: A Contribution to Hilbert\u2019s Last Problem","author":"S Negri","year":"2011","unstructured":"Negri, S., van Plato, J.: Proof Analysis: A Contribution to Hilbert\u2019s Last Problem. Cambridge University Press, Cambridge (2011)"},{"issue":"2","key":"39_CR15","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1007\/s10817-010-9182-1","volume":"45","author":"V Nigam","year":"2010","unstructured":"Nigam, V., Miller, D.: A framework for proof systems. J. Autom. Reasoning 45(2), 157\u2013188 (2010)","journal-title":"J. Autom. Reasoning"},{"key":"39_CR16","doi-asserted-by":"publisher","unstructured":"Nigam, V., Pimentel, E., Reis, G.: An extended framework for specifying and reasoning about proof systems. J. Logic Comput. (2014). doi:\n                    10.1093\/logcom\/exu029\n                    \n                  , \n                    http:\/\/logcom.oxfordjournals.org\/content\/early\/2014\/06\/06\/logcom.exu029.abstract","DOI":"10.1093\/logcom\/exu029"},{"key":"39_CR17","series-title":"Trends in Logic","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1007\/978-1-4020-9084-4_3","volume-title":"Towards Mathematical Philosophy","author":"F Poggiolesi","year":"2009","unstructured":"Poggiolesi, F.: The method of tree-hypersequents for modal propositional logic. In: Makinson, D., Malinowski, J., Wansing, H. (eds.) Towards Mathematical Philosophy. Trends in Logic, vol. 28, pp. 31\u201351. Springer, Heidelberg (2009)"},{"key":"39_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1007\/978-3-642-37075-5_14","volume-title":"Foundations of Software Science and Computation Structures","author":"L Stra\u00dfburger","year":"2013","unstructured":"Stra\u00dfburger, L.: Cut elimination in nested sequents for intuitionistic modal logics. In: Pfenning, F. (ed.) FOSSACS 2013. LNCS, vol. 7794, pp. 209\u2013224. Springer, Heidelberg (2013)"}],"container-title":["Lecture Notes in Computer Science","Logic for Programming, Artificial Intelligence, and Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-48899-7_39","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,31]],"date-time":"2019-05-31T19:31:19Z","timestamp":1559331079000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-48899-7_39"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783662488980","9783662488997"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-48899-7_39","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]}}}