{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,29]],"date-time":"2025-09-29T11:58:09Z","timestamp":1759147089424},"publisher-location":"Berlin, Heidelberg","reference-count":19,"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_19","type":"book-chapter","created":{"date-parts":[[2015,11,21]],"date-time":"2015-11-21T03:59:28Z","timestamp":1448078368000},"page":"266-280","source":"Crossref","is-referenced-by-count":13,"title":["Focused Labeled Proof Systems for Modal Logic"],"prefix":"10.1007","author":[{"given":"Dale","family":"Miller","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marco","family":"Volpe","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2015,11,22]]},"reference":[{"issue":"3","key":"19_CR1","doi-asserted-by":"publisher","first-page":"297","DOI":"10.1093\/logcom\/2.3.297","volume":"2","author":"J-M 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":"19_CR2","doi-asserted-by":"crossref","unstructured":"Blackburn, P., Van Benthem, J.: Modal logic: a semantic perspective. In: Handbook of Modal Logic, pp. 1\u201382. Elsevier (2007)","DOI":"10.1016\/S1570-2464(07)80004-8"},{"key":"19_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1007\/978-3-642-38574-2_11","volume-title":"Automated Deduction \u2013 CADE-24","author":"Z Chihani","year":"2013","unstructured":"Chihani, Z., Miller, D., Renaud, F.: Foundational proof certificates in first-order logic. In: Bonacina, M.P. (ed.) CADE 2013. LNCS, vol. 7898, pp. 162\u2013177. Springer, Heidelberg (2013)"},{"key":"19_CR4","doi-asserted-by":"crossref","unstructured":"Chihani, Z., Libal, T., Reis, G.: The Proof Certifier Checkers. To appear in Tableaux, System Description (2015)","DOI":"10.1007\/978-3-319-24312-2_14"},{"issue":"1\u20132","key":"19_CR5","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1007\/s00153-011-0254-7","volume":"51","author":"R Dyckhoff","year":"2012","unstructured":"Dyckhoff, R., Negri, S.: Proof analysis in intermediate logics. Arch. Math. Logic 51(1\u20132), 71\u201392 (2012)","journal-title":"Arch. Math. Logic"},{"key":"19_CR6","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1017\/bsl.2015.7","volume":"21","author":"R Dyckhoff","year":"2015","unstructured":"Dyckhoff, R., Negri, S.: Geometrisation of first-order logic. Bull. Symbolic Logic 21, 123\u2013163 (2015)","journal-title":"Bull. Symbolic Logic"},{"key":"19_CR7","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1016\/S1570-2464(07)80005-X","volume-title":"Handbook of Modal Logic","author":"M Fitting","year":"2007","unstructured":"Fitting, M.: Modal proof theory. In: Wolter, F., Blackburn, P., van Benthem, J. (eds.) Handbook of Modal Logic, pp. 85\u2013138. Elsevier, New York (2007)"},{"key":"19_CR8","doi-asserted-by":"crossref","DOI":"10.1093\/oso\/9780198538332.001.0001","volume-title":"Labelled Deductive Systems","author":"DM Gabbay","year":"1996","unstructured":"Gabbay, D.M.: Labelled Deductive Systems. Clarendon Press, Oxford (1996)"},{"key":"19_CR9","series-title":"NATO ASI Series","doi-asserted-by":"publisher","first-page":"215","DOI":"10.1007\/978-3-642-58622-4_7","volume-title":"Computational Logic","author":"J-Y Girard","year":"1999","unstructured":"Girard, J.-Y.: On the meaning of logical rules I: syntax vs. semantics. In: Berger, U., Schwichtenberg, H. (eds.) Computational Logic. NATO ASI, pp. 215\u2013272. Springer, Heidelberg (1999)"},{"issue":"46","key":"19_CR10","doi-asserted-by":"publisher","first-page":"4747","DOI":"10.1016\/j.tcs.2009.07.041","volume":"410","author":"C Liang","year":"2009","unstructured":"Liang, C., Miller, D.: Focusing and polarization in linear, intuitionistic, and classical logics. Theo. Comput. Sci. 410(46), 4747\u20134768 (2009)","journal-title":"Theo. Comput. Sci."},{"key":"19_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"54","DOI":"10.1007\/978-3-642-25379-9_6","volume-title":"Certified Programs and Proofs","author":"D Miller","year":"2011","unstructured":"Miller, D.: A proposal for broad spectrum proof certificates. In: Jouannaud, J.-P., Shao, Z. (eds.) CPP 2011. LNCS, vol. 7086, pp. 54\u201369. Springer, Heidelberg (2011)"},{"key":"19_CR12","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139021326","volume-title":"Programming with Higher-Order Logic","author":"D Miller","year":"2012","unstructured":"Miller, D., Nadathur, G.: Programming with Higher-Order Logic. Cambridge University Press, Cambridge (2012)"},{"key":"19_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. Theo. Comput. Sci. 474, 98\u2013116 (2013)","journal-title":"Theo. Comput. Sci."},{"issue":"5\u20136","key":"19_CR14","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 34(5\u20136), 507\u2013544 (2005)","journal-title":"J. Philos. Logic"},{"issue":"4","key":"19_CR15","doi-asserted-by":"publisher","first-page":"418","DOI":"10.2307\/420956","volume":"4","author":"S Negri","year":"1998","unstructured":"Negri, S., von Plato, J.: Cut elimination in the presence of axioms. Bull. Symbolic Logic 4(4), 418\u2013435 (1998)","journal-title":"Bull. Symbolic Logic"},{"key":"19_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: 10.1093\/logcom\/exu029","DOI":"10.1093\/logcom\/exu029"},{"key":"19_CR17","doi-asserted-by":"crossref","unstructured":"Sahlqvist, H.: Completeness and correspondence in first and second order semantics for modal logic. In: Kanger, S., (ed.) Proceedings of the Third Scandinavian Logic Symposium, pp. 110\u2013143, North Holland (1975)","DOI":"10.1016\/S0049-237X(08)70728-6"},{"key":"19_CR18","unstructured":"Simpson, A.K.: The Proof Theory and Semantics of Intuitionistic Modal Logic. Ph.D. thesis, School of Informatics, University of Edinburgh (1994)"},{"key":"19_CR19","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4757-3208-5","volume-title":"Labelled Non-Classical Logics","author":"L Vigan\u00f2","year":"2000","unstructured":"Vigan\u00f2, L.: Labelled Non-Classical Logics. Kluwer Academic Publishers, Dordrecht (2000)"}],"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_19","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,6,12]],"date-time":"2024-06-12T16:05:06Z","timestamp":1718208306000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-48899-7_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783662488980","9783662488997"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-48899-7_19","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]}}}