{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T07:38:58Z","timestamp":1742974738082,"version":"3.40.3"},"publisher-location":"Cham","reference-count":34,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031781155"},{"type":"electronic","value":"9783031781162"}],"license":[{"start":{"date-parts":[[2024,11,29]],"date-time":"2024-11-29T00:00:00Z","timestamp":1732838400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,11,29]],"date-time":"2024-11-29T00:00:00Z","timestamp":1732838400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"DOI":"10.1007\/978-3-031-78116-2_8","type":"book-chapter","created":{"date-parts":[[2024,11,28]],"date-time":"2024-11-28T07:31:15Z","timestamp":1732779075000},"page":"120-138","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Soundness-Preserving Fusion of\u00a0Modal Logics in\u00a0Coq"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-3997-8474","authenticated-orcid":false,"given":"Miguel Alfredo","family":"Nunes","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5194-5870","authenticated-orcid":false,"given":"Karina Girardi","family":"Roggia","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3838-652X","authenticated-orcid":false,"given":"Paulo Henrique","family":"Torrens","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2024,11,29]]},"reference":[{"key":"8_CR1","unstructured":"Azurat, A., Prasetya, W.: A survey on embedding programming logics in a theorem prover. Tech. rep., Utrecht University: Institute of Information and Computing Sciences, Utrecht (2002)"},{"issue":"3","key":"8_CR2","doi-asserted-by":"publisher","first-page":"369","DOI":"10.1007\/s11225-006-9013-x","volume":"84","author":"JV Benthem","year":"2006","unstructured":"Benthem, J.V., Bezhanishvili, G., Cate, B.T., Sarenac, D.: Multimodal logics of products of topologies. Stud. Logica. 84(3), 369\u2013392 (2006)","journal-title":"Stud. Logica."},{"key":"8_CR3","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"459","DOI":"10.1007\/978-3-030-89391-0_25","volume-title":"Logic and Argumentation","author":"B Bentzen","year":"2021","unstructured":"Bentzen, B.: A Henkin-style completeness proof for\u00a0the modal logic S5. In: Baroni, P., Benzm\u00fcller, C., W\u00e1ng, Y.N. (eds.) CLAR 2021. LNCS (LNAI), vol. 13040, pp. 459\u2013467. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-89391-0_25"},{"key":"8_CR4","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1007\/978-3-642-14977-1_6","volume-title":"Computational Logic in Multi-Agent Systems","author":"C Benzm\u00fcller","year":"2010","unstructured":"Benzm\u00fcller, C.: Combining logics in simple type theory. In: Dix, J., Leite, J., Governatori, G., Jamroga, W. (eds.) CLIMA 2010. LNCS (LNAI), vol. 6245, pp. 33\u201348. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-14977-1_6"},{"key":"8_CR5","doi-asserted-by":"publisher","unstructured":"Benzm\u00fcller, C., Parent, X., van der Torre, L.: Designing normative theories for ethical and legal reasoning: logikey framework, methodology, and tool support. Artif. Intell. 287, 103348 (2020). https:\/\/doi.org\/10.1016\/j.artint.2020.103348, https:\/\/www.sciencedirect.com\/science\/article\/pii\/S0004370219301110","DOI":"10.1016\/j.artint.2020.103348"},{"key":"8_CR6","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781107050884","volume-title":"Modal Logic","author":"P Blackburn","year":"2001","unstructured":"Blackburn, P., De Rijke, M., Venema, Y.: Modal Logic, vol. 53. Cambridge University Press, Cambridge (2001)"},{"key":"8_CR7","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4020-6782-2","volume-title":"Analysis and Synthesis of Logics: How to Cut and Paste Reasoning Systems","author":"W Carnielli","year":"2008","unstructured":"Carnielli, W., Coniglio, M., Gabbay, D.M., Gouveia, P., Sernadas, C.: Analysis and Synthesis of Logics: How to Cut and Paste Reasoning Systems, vol. 35. Springer Science & Business Media, Netherlands (2008). https:\/\/doi.org\/10.1007\/978-1-4020-6782-2"},{"key":"8_CR8","unstructured":"Carnielli, W., Coniglio, M.E.: Combining logics. In: Zalta, E.N. (ed.) The Stanford Encyclopedia of Philosophy. Metaphysics Research Lab, Stanford University, Stanford, Fall 2020 edn. (2020)"},{"key":"8_CR9","doi-asserted-by":"publisher","unstructured":"Carnielli, W.A., Pizzi, C., Bueno-Soler, J.: Modalities and Multimodalities, vol.\u00a020. Springer (2008). https:\/\/doi.org\/10.1007\/978-1-4020-8590-1","DOI":"10.1007\/978-1-4020-8590-1"},{"key":"8_CR10","doi-asserted-by":"publisher","unstructured":"Da\u00a0Silveira, A.A., Ribeiro, R., Nunes, M.A., Torrens, P., Roggia, K.: A sound deep embedding of arbitrary normal modal logics in coq. In: SBLP 2022: XXVI Brazilian Symposium on Programming Languages, pp.\u00a01\u20137. Association for Computing Machinery, New York, NY, USA (2022). https:\/\/doi.org\/10.1145\/3561320.3561329","DOI":"10.1145\/3561320.3561329"},{"key":"8_CR11","doi-asserted-by":"crossref","unstructured":"Fine, K., Schurz, G.: Transfer theorems for multimodal logics. Logic and Reality: Essays on the Legacy of Arthur Prior 169\u2013213 (1996)","DOI":"10.1093\/oso\/9780198240600.003.0009"},{"issue":"3","key":"8_CR12","doi-asserted-by":"publisher","first-page":"259","DOI":"10.1111\/j.1755-2567.1969.tb00372.x","volume":"35","author":"M Fitting","year":"1969","unstructured":"Fitting, M.: Logics with several modal operators. Theoria 35(3), 259\u2013266 (1969)","journal-title":"Theoria"},{"key":"8_CR13","doi-asserted-by":"publisher","first-page":"418","DOI":"10.1007\/978-3-030-29908-8_34","volume-title":"PRICAI 2019: Trends in Artificial Intelligence","author":"D Fuenmayor","year":"2019","unstructured":"Fuenmayor, D., Benzm\u00fcller, C.: Harnessing higher-order (meta-)logic to represent and reason with complex ethical theories. In: Nayak, A.C., Sharma, A. (eds.) PRICAI 2019: Trends in Artificial Intelligence, pp. 418\u2013432. Springer International Publishing, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-29908-8_34"},{"key":"8_CR14","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"112","DOI":"10.1007\/978-3-030-29007-8_7","volume-title":"Frontiers of Combining Systems","author":"D Fuenmayor","year":"2019","unstructured":"Fuenmayor, D., Benzm\u00fcller, C.: Mechanised assessment of complex natural-language arguments using expressive logic combinations. In: Herzig, A., Popescu, A. (eds.) FroCoS 2019. LNCS (LNAI), vol. 11715, pp. 112\u2013128. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-29007-8_7"},{"key":"8_CR15","unstructured":"Gabbay, D.: Many-dimensional Modal Logics: Theory and Applications. Studies in logic and the foundations of mathematics, North Holland Publishing Company, Amsterdam (2003)"},{"key":"8_CR16","first-page":"301","volume":"1","author":"K G\u00f6del","year":"1986","unstructured":"G\u00f6del, K.: An interpretation of the intuitionistic propositional calculus. Collect. Works 1, 301\u2013303 (1986)","journal-title":"Collect. Works"},{"key":"8_CR17","volume-title":"Mathematics of Modality","author":"R Goldblatt","year":"1993","unstructured":"Goldblatt, R.: Mathematics of Modality. Center for the Study of Language and Information Publications, Stanford (1993)"},{"issue":"4","key":"8_CR18","doi-asserted-by":"publisher","first-page":"1469","DOI":"10.2307\/2275487","volume":"56","author":"M Kracht","year":"1991","unstructured":"Kracht, M., Wolter, F.: Properties of independently axiomatizable bimodal logics. J. Symbolic Logic 56(4), 1469\u20131485 (1991)","journal-title":"J. Symbolic Logic"},{"issue":"1","key":"8_CR19","doi-asserted-by":"publisher","first-page":"1","DOI":"10.2307\/2964568","volume":"24","author":"SA Kripke","year":"1959","unstructured":"Kripke, S.A.: A completeness theorem in modal logic. J. Symbolic Logic 24(1), 1\u201314 (1959)","journal-title":"J. Symbolic Logic"},{"issue":"5\u20136","key":"8_CR20","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1002\/malq.19630090502","volume":"9","author":"SA Kripke","year":"1963","unstructured":"Kripke, S.A.: Semantical analysis of modal logic i normal modal propositional calculi. Math. Log. Q. 9(5\u20136), 67\u201396 (1963)","journal-title":"Math. Log. Q."},{"key":"8_CR21","unstructured":"Kuhn, S.: Modal Logic, vol.\u00a010. Routledge, London, 1 edn. (1998)"},{"key":"8_CR22","unstructured":"Leroy, X.: The CompCert C verified compiler: documentation and user\u2019s manual. Ph. D. thesis, Inria (2021)"},{"key":"8_CR23","unstructured":"Lescanne, P., Puiss\u00e9gur, J.: Dynamic logic of common knowledge in a proof assistant. arXiv preprint arXiv:0712.3146 (2007)"},{"key":"8_CR24","doi-asserted-by":"publisher","DOI":"10.1525\/9780520398252","volume-title":"A Survey of Symbolic Logic","author":"CI Lewis","year":"1918","unstructured":"Lewis, C.I.: A Survey of Symbolic Logic. University of California press, Berkeley (1918)"},{"key":"8_CR25","volume-title":"Symbolic Logic","author":"CI Lewis","year":"1932","unstructured":"Lewis, C.I., Langford, C.H.: Symbolic Logic, vol. 170. Dover Publications New York, New York (1932)"},{"key":"8_CR26","doi-asserted-by":"publisher","unstructured":"Maggesi, M., Perini\u00a0Brogi, C.: A formal proof of modal completeness for provability logic. In: Cohen, L., Kaliszyk, C. (eds.) 12th International Conference on Interactive Theorem Proving (ITP 2021). Leibniz International Proceedings in Informatics (LIPIcs), vol.\u00a0193, pp. 1\u201318. Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik, Dagstuhl, Germany (2021). https:\/\/doi.org\/10.4230\/LIPIcs.ITP.2021.26, https:\/\/drops.dagstuhl.de\/entities\/document\/10.4230\/LIPIcs.ITP.2021.26","DOI":"10.4230\/LIPIcs.ITP.2021.26"},{"key":"8_CR27","first-page":"263","volume":"35","author":"IE Orlov","year":"1928","unstructured":"Orlov, I.E.: The calculus of compatibility of propositions mathematics of the USSR. Sbornik 35, 263\u2013286 (1928)","journal-title":"Sbornik"},{"key":"8_CR28","unstructured":"Paiva, N., Caleiro, C.: Temporal logic in Coq. Projeto de diploma\u00c3\u00a7\u00c3\u00a3o, Licenciatura em Matem\u00e1tica Aplicada e Computa\u00e7\u00e3o \u2013 Instituto Superior T\u00e9cnico (1998)"},{"key":"8_CR29","volume-title":"All about Proofs, Proofs for All, Studies in Logic (Mathematical logic and foundations)","author":"C Paulin-Mohring","year":"2015","unstructured":"Paulin-Mohring, C.: Introduction to the calculus of inductive constructions. In: Paleo, B.W., Delahaye, D. (eds.) All about Proofs, Proofs for All, Studies in Logic (Mathematical logic and foundations), vol. 55. College Publications, London (2015)"},{"issue":"6","key":"8_CR30","doi-asserted-by":"publisher","first-page":"1753","DOI":"10.1093\/logcom\/exu079","volume":"27","author":"F Rabe","year":"2017","unstructured":"Rabe, F.: How to identify, translate and combine logics? J. Log. Comput. 27(6), 1753\u20131798 (2017)","journal-title":"J. Log. Comput."},{"key":"8_CR31","doi-asserted-by":"publisher","unstructured":"Scott, D.: Advice on Modal Logic, pp. 143\u2013173. Springer Netherlands, Dordrecht (1970).https:\/\/doi.org\/10.1007\/978-94-010-3272-8_7","DOI":"10.1007\/978-94-010-3272-8_7"},{"key":"8_CR32","unstructured":"Team, T.C.D.: The Coq Reference Manual. France (2022)"},{"key":"8_CR33","doi-asserted-by":"publisher","unstructured":"Thomason, R.H.: Combinations of tense and modality. In: Handbook of Philosophical Logic, pp. 135\u2013165. Springer, Dordrecht (1984). https:\/\/doi.org\/10.1007\/978-94-009-6259-0_3","DOI":"10.1007\/978-94-009-6259-0_3"},{"issue":"1","key":"8_CR34","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1007\/s11098-005-4052-0","volume":"128","author":"J van Benthem","year":"2006","unstructured":"van Benthem, J.: Epistemic logic and epistemology: the state of their affairs. Philos. Stud. 128(1), 49\u201376 (2006)","journal-title":"Philos. Stud."}],"container-title":["Lecture Notes in Computer Science","Formal Methods: Foundations and Applications"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-78116-2_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,11,28]],"date-time":"2024-11-28T09:04:24Z","timestamp":1732784664000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-78116-2_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,11,29]]},"ISBN":["9783031781155","9783031781162"],"references-count":34,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-78116-2_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2024,11,29]]},"assertion":[{"value":"29 November 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"SBMF","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Brazilian Symposium on Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Vit\u00f3ria","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Brazil","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"3 December 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"5 December 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"sbmf2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}