{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,2]],"date-time":"2025-08-02T19:10:46Z","timestamp":1754161846958,"version":"3.41.2"},"publisher-location":"Cham","reference-count":64,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031999833","type":"print"},{"value":"9783031999840","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,7,30]],"date-time":"2025-07-30T00:00:00Z","timestamp":1753833600000},"content-version":"vor","delay-in-days":210,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>Deep and shallow embeddings of non-classical logics in classical higher-order logic have been explored, implemented, and used in various reasoning tools in recent years. This paper presents a method for the simultaneous deployment of deep and shallow embeddings of various degrees in classical higher-order logic. This enables flexible, interactive and automated theorem proving and counterexample finding at meta and object level, as well as automated faithfulness proofs between these logic embeddings. The method is beneficial for logic education, research and application and is illustrated here using a simple propositional modal logic. However, this approach is conceptual in nature and not limited to this simple logic context.<\/jats:p>","DOI":"10.1007\/978-3-031-99984-0_16","type":"book-chapter","created":{"date-parts":[[2025,7,29]],"date-time":"2025-07-29T11:47:44Z","timestamp":1753789664000},"page":"280-301","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Faithful Logic Embeddings in\u00a0HOL\u2014 Deep and\u00a0Shallow"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-3392-3093","authenticated-orcid":false,"given":"Christoph","family":"Benzm\u00fcller","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,7,30]]},"reference":[{"key":"16_CR1","doi-asserted-by":"publisher","unstructured":"Abrahamsson, O., Myreen, M.O., Kumar, R., Sewell, T.: Candle: a verified implementation of HOL light. In: Andronick, J., de\u00a0Moura, L. (eds.) 13th International Conference on Interactive Theorem Proving, ITP 2022, 7\u201310 August 2022, Haifa, Israel. LIPIcs, vol.\u00a0237, pp. 3:1\u20133:17. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2022). https:\/\/doi.org\/10.4230\/LIPICS.ITP.2022.3","DOI":"10.4230\/LIPICS.ITP.2022.3"},{"issue":"2","key":"16_CR2","doi-asserted-by":"publisher","first-page":"395","DOI":"10.2307\/2272982","volume":"37","author":"PB Andrews","year":"1972","unstructured":"Andrews, P.B.: General models and extensionality. J. Symb. Log. 37(2), 395\u2013397 (1972). https:\/\/doi.org\/10.2307\/2272982","journal-title":"J. Symb. Log."},{"key":"16_CR3","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1007\/978-3-642-17172-7_7","volume-title":"Verification, Induction, Termination Analysis","author":"C Benzm\u00fcller","year":"2010","unstructured":"Benzm\u00fcller, C.: Verifying the modal logic cube is an easy task (for higher-order automated reasoners). In: Siegler, S., Wasser, N. (eds.) Verification, Induction, Termination Analysis. LNCS (LNAI), vol. 6463, pp. 117\u2013128. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-17172-7_7"},{"issue":"3","key":"16_CR4","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1007\/s10992-016-9403-0","volume":"46","author":"C Benzm\u00fcller","year":"2016","unstructured":"Benzm\u00fcller, C.: Cut-elimination for quantified conditional logic. J. Philos. Log. 46(3), 333\u2013353 (2016). https:\/\/doi.org\/10.1007\/s10992-016-9403-0","journal-title":"J. Philos. Log."},{"key":"16_CR5","doi-asserted-by":"publisher","unstructured":"Benzm\u00fcller, C.: Faithful logic embeddings in HOL \u2014 deep and shallow (2025). https:\/\/doi.org\/10.48550\/arXiv.2502.19311","DOI":"10.48550\/arXiv.2502.19311"},{"key":"16_CR6","unstructured":"Benzm\u00fcller, C., Andrews, P.: Church\u2019s type theory. In: Zalta, E.N., Nodelman, U. (eds.) The Stanford Encyclopedia of Philosophy, 2024 edn. Metaphysics Research Lab, Stanford University. Spring (2024). https:\/\/plato.stanford.edu\/archives\/spr2024\/entries\/type-theory-church\/"},{"issue":"4","key":"16_CR7","doi-asserted-by":"publisher","first-page":"1027","DOI":"10.2178\/jsl\/1102022211","volume":"69","author":"C Benzm\u00fcller","year":"2004","unstructured":"Benzm\u00fcller, C., Brown, C., Kohlhase, M.: Higher-order semantics and extensionality. J. Symb. Log. 69(4), 1027\u20131088 (2004). https:\/\/doi.org\/10.2178\/jsl\/1102022211","journal-title":"J. Symb. Log."},{"key":"16_CR8","doi-asserted-by":"publisher","unstructured":"Benzm\u00fcller, C., Claus, M., Sultana, N.: Systematic verification of the modal logic cube in Isabelle\/HOL. In: Kaliszyk, C., Paskevich, A. (eds.) PxTP 2015, vol.\u00a0186, pp. 27\u201341. EPTCS (2015). https:\/\/doi.org\/10.4204\/EPTCS.186.5","DOI":"10.4204\/EPTCS.186.5"},{"key":"16_CR9","doi-asserted-by":"publisher","unstructured":"Benzm\u00fcller, C., Miller, D.: Automation of higher-order logic. In: Gabbay, D.M., Siekmann, J.H., Woods, J. (eds.) Handbook of the History of Logic, Volume 9\u2014Computational Logic, pp. 215\u2013254. Elsevier, North Holland (2014). https:\/\/doi.org\/10.1016\/B978-0-444-51624-4.50005-8","DOI":"10.1016\/B978-0-444-51624-4.50005-8"},{"key":"16_CR10","doi-asserted-by":"publisher","DOI":"10.1016\/j.artint.2020.103348","volume":"287","author":"C Benzm\u00fcller","year":"2020","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","journal-title":"Artif. Intell."},{"issue":"6","key":"16_CR11","doi-asserted-by":"publisher","first-page":"881","DOI":"10.1093\/jigpal\/jzp080","volume":"18","author":"C Benzm\u00fcller","year":"2010","unstructured":"Benzm\u00fcller, C., Paulson, L.C.: Multimodal and intuitionistic logics in simple type theory. Log. J. IGPL 18(6), 881\u2013892 (2010). https:\/\/doi.org\/10.1093\/jigpal\/jzp080","journal-title":"Log. J. IGPL"},{"issue":"1","key":"16_CR12","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1007\/s11787-012-0052-y","volume":"7","author":"C Benzm\u00fcller","year":"2013","unstructured":"Benzm\u00fcller, C., Paulson, L.C.: Quantified multimodal logics in simple type theory. Log. Univers. 7(1), 7\u201320 (2013). https:\/\/doi.org\/10.1007\/s11787-012-0052-y","journal-title":"Log. Univers."},{"issue":"6","key":"16_CR13","doi-asserted-by":"publisher","first-page":"1243","DOI":"10.1093\/logcom\/exac029","volume":"33","author":"C Benzm\u00fcller","year":"2023","unstructured":"Benzm\u00fcller, C., Reiche, S.: Automating public announcement logic with relativized common knowledge as a fragment of HOL in LogiKEy. J. Log. Comput. 33(6), 1243\u20131269 (2023). https:\/\/doi.org\/10.1093\/logcom\/exac029","journal-title":"J. Log. Comput."},{"issue":"1","key":"16_CR14","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1007\/s10817-018-09507-7","volume":"64","author":"C Benzm\u00fcller","year":"2019","unstructured":"Benzm\u00fcller, C., Scott, D.S.: Automating free logic in HOL, with an experimental application in category theory. J. Autom. Reason. 64(1), 53\u201372 (2019). https:\/\/doi.org\/10.1007\/s10817-018-09507-7","journal-title":"J. Autom. Reason."},{"key":"16_CR15","unstructured":"Benzm\u00fcller, C.: Faithful logic embeddings in HOL\u2014deep and shallow (Isabelle\/HOL dataset). Arch. Formal Proofs (2025). https:\/\/isa-afp.org\/entries\/FaithfulPMLinHOL.html"},{"key":"16_CR16","doi-asserted-by":"publisher","first-page":"442","DOI":"10.1093\/jigpal\/jzac082","volume":"32","author":"C Benzm\u00fcller","year":"2024","unstructured":"Benzm\u00fcller, C., Fuenmayor, D., Steen, A., Sutcliffe, G.: Who finds the short proof? Log. J. IGPL 32, 442\u2013464 (2024). https:\/\/doi.org\/10.1093\/jigpal\/jzac082","journal-title":"Log. J. IGPL"},{"key":"16_CR17","doi-asserted-by":"publisher","DOI":"10.1007\/s00605-025-02078-x","author":"C Benzm\u00fcller","year":"2025","unstructured":"Benzm\u00fcller, C., Scott, D.S.: Notes on G\u00f6del\u2019s and Scott\u2019s variants of the ontological argument. Monatshefte f\u00fcr Mathematik (2025). https:\/\/doi.org\/10.1007\/s00605-025-02078-x","journal-title":"Monatshefte f\u00fcr Mathematik"},{"key":"16_CR18","doi-asserted-by":"crossref","unstructured":"Bertot, Y., Casteran, P.: Interactive Theorem Proving and Program Development. Springer (2004)","DOI":"10.1007\/978-3-662-07964-5"},{"key":"16_CR19","doi-asserted-by":"publisher","unstructured":"Blackburn, P., van Benthem, J.: Modal logic: a semantic perspective. In: Blackburn, P., van Benthem, J.F.A.K., Wolter, F. (eds.) Handbook of Modal Logic, Studies in Logic and Practical Reasoning, North-Holland, vol.\u00a03, pp. 1\u201384 (2007). https:\/\/doi.org\/10.1016\/S1570-2464(07)80004-8","DOI":"10.1016\/S1570-2464(07)80004-8"},{"key":"16_CR20","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"116","DOI":"10.1007\/978-3-642-22438-6_11","volume-title":"Automated Deduction \u2013 CADE-23","author":"JC Blanchette","year":"2011","unstructured":"Blanchette, J.C., B\u00f6hme, S., Paulson, L.C.: Extending sledgehammer with SMT solvers. In: Bj\u00f8rner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS (LNAI), vol. 6803, pp. 116\u2013130. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22438-6_11"},{"key":"16_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1007\/978-3-642-14052-5_11","volume-title":"Interactive Theorem Proving","author":"JC Blanchette","year":"2010","unstructured":"Blanchette, J.C., Nipkow, T.: Nitpick: a counterexample generator for higher-order logic based on a relational model finder. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol. 6172, pp. 131\u2013146. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-14052-5_11"},{"issue":"1","key":"16_CR22","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1007\/S10817-016-9391-3","volume":"58","author":"JC Blanchette","year":"2017","unstructured":"Blanchette, J.C., Popescu, A., Traytel, D.: Soundness and completeness proofs by coinductive methods. J. Autom. Reason. 58(1), 149\u2013179 (2017). https:\/\/doi.org\/10.1007\/S10817-016-9391-3","journal-title":"J. Autom. Reason."},{"key":"16_CR23","doi-asserted-by":"publisher","unstructured":"Bohrer, R., Rahli, V., Vukotic, I., V\u00f6lp, M., Platzer, A.: Formally verified differential dynamic logic. In: Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2017, pp. 208\u2013221. Association for Computing Machinery, New York, NY, USA (2017). https:\/\/doi.org\/10.1145\/3018610.3018616","DOI":"10.1145\/3018610.3018616"},{"key":"16_CR24","doi-asserted-by":"crossref","unstructured":"Boolos, G.S.: The Logic of Provability. Cambridge University Press (1994)","DOI":"10.1017\/CBO9780511625183"},{"key":"16_CR25","unstructured":"Boulton, R.J., Gordon, A.D., Gordon, M.J.C., Harrison, J., Herbert, J., Tassel, J.V.: Experience with embedding hardware description languages in HOL. In: Stavridou, V., Melham, T.F., Boute, R.T. (eds.) Theorem Provers in Circuit Design, Proceedings of the IFIP TC10\/WG 10.2 International Conference on Theorem Provers in Circuit Design: Theory, Practice and Experience, Nijmegen, The Netherlands, 22\u201324 June 1992, Proceedings. IFIP Transactions, North-Holland, vol.\u00a0A-10, pp. 129\u2013156 (1992)"},{"key":"16_CR26","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1007\/978-3-030-53518-6_5","volume-title":"Intelligent Computer Mathematics","author":"M Carneiro","year":"2020","unstructured":"Carneiro, M.: Metamath zero: designing a theorem prover prover. In: Benzm\u00fcller, C., Miller, B. (eds.) CICM 2020. LNCS (LNAI), vol. 12236, pp. 71\u201388. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-53518-6_5"},{"key":"16_CR27","doi-asserted-by":"publisher","unstructured":"Carneiro, M.: Lean4Lean: towards a verified typechecker for Lean, in Lean (2024). https:\/\/doi.org\/10.48550\/arXiv.2403.14064","DOI":"10.48550\/arXiv.2403.14064"},{"issue":"2","key":"16_CR28","doi-asserted-by":"publisher","first-page":"56","DOI":"10.2307\/2266170","volume":"5","author":"A Church","year":"1940","unstructured":"Church, A.: A formulation of the simple theory of types. J. Symb. Log. 5(2), 56\u201368 (1940). https:\/\/doi.org\/10.2307\/2266170","journal-title":"J. Symb. Log."},{"key":"16_CR29","doi-asserted-by":"publisher","unstructured":"Cohen, J.M., Johnson-Freyd, P.: A formalization of core Why3 in Coq. Proc. ACM Program. Lang. 8(POPL), 1789\u20131818 (2024). https:\/\/doi.org\/10.1145\/3632902","DOI":"10.1145\/3632902"},{"key":"16_CR30","doi-asserted-by":"publisher","unstructured":"Czajka, L.: A shallow embedding of pure type systems into first-order logic. In: Ghilezan, S., Geuvers, H., Ivetic, J. (eds.) 22nd International Conference on Types for Proofs and Programs (TYPES 2016). Leibniz International Proceedings in Informatics (LIPIcs), vol.\u00a097, pp. 9:1\u20139:39. Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik, Dagstuhl, Germany (2018). https:\/\/doi.org\/10.4230\/LIPIcs.TYPES.2016.9","DOI":"10.4230\/LIPIcs.TYPES.2016.9"},{"key":"16_CR31","doi-asserted-by":"publisher","unstructured":"From, A.H., Jacobsen, F.K.: Verifying a sequent calculus prover for first-order logic with functions in Isabelle\/HOL. In: Andronick, J., de\u00a0Moura, L. (eds.) 13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics (LIPIcs), vol.\u00a0237, pp. 13:1\u201313:22. Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik, Dagstuhl, Germany (2022). https:\/\/doi.org\/10.4230\/LIPIcs.ITP.2022.13","DOI":"10.4230\/LIPIcs.ITP.2022.13"},{"key":"16_CR32","unstructured":"From, A.H.: A Naive prover for first-order logic. Arch. Formal Proofs (2022). https:\/\/isa-afp.org\/entries\/FOL_Seq_Calc3.html"},{"key":"16_CR33","unstructured":"From, A.H., Villadsen, J.: Soundness and completeness of implicational logic. Arch. Formal Proofs (2022). https:\/\/isa-afp.org\/entries\/Implicational_Logic.html"},{"key":"16_CR34","unstructured":"Garson, J.: Modal logic. In: Zalta, E.N., Nodelman, U. (eds.) The Stanford Encyclopedia of Philosophy, 2024 edn. Metaphysics Research Lab, Stanford University. Spring (2024). https:\/\/plato.stanford.edu\/archives\/spr2024\/entries\/logic-modal\/"},{"key":"16_CR35","doi-asserted-by":"publisher","unstructured":"Gibbons, J., Wu, N.: Folding domain-specific languages: deep and shallow embeddings (functional pearl). In: Jeuring, J., Chakravarty, M.M.T. (eds.) Proceedings of the 19th ACM SIGPLAN International Conference on Functional Programming, Gothenburg, Sweden, 1\u20133 September 2014, pp. 339\u2013347. ACM (2014). https:\/\/doi.org\/10.1145\/2628136.2628138","DOI":"10.1145\/2628136.2628138"},{"issue":"1","key":"16_CR36","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1007\/BF01700692","volume":"38","author":"K G\u00f6del","year":"1931","unstructured":"G\u00f6del, K.: \u00dcber formal unentscheidbare S\u00e4tze der Principia Mathematica und verwandter Systeme I. Monatshefte f\u00fcr Mathematik und Physik 38(1), 173\u2013198 (1931). https:\/\/doi.org\/10.1007\/BF01700692","journal-title":"Monatshefte f\u00fcr Mathematik und Physik"},{"key":"16_CR37","doi-asserted-by":"publisher","unstructured":"Guilloud, S., Gambhir, S., Gilot, A., Kuncak, V.: Mechanized HOL reasoning in set theory. In: Bertot, Y., Kutsia, T., Norrish, M. (eds.) 15th International Conference on Interactive Theorem Proving, ITP 2024, 9\u201314 September 2024, Tbilisi, Georgia. LIPIcs, vol.\u00a0309, pp. 18:1\u201318:18. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2024). https:\/\/doi.org\/10.4230\/LIPICS.ITP.2024.18","DOI":"10.4230\/LIPICS.ITP.2024.18"},{"key":"16_CR38","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"177","DOI":"10.1007\/11814771_17","volume-title":"Automated Reasoning","author":"J Harrison","year":"2006","unstructured":"Harrison, J.: Towards self-verification of HOL light. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol. 4130, pp. 177\u2013191. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11814771_17"},{"issue":"2","key":"16_CR39","doi-asserted-by":"publisher","first-page":"81","DOI":"10.2307\/2266967","volume":"15","author":"L Henkin","year":"1950","unstructured":"Henkin, L.: Completeness in the theory of types. J. Symb. Log. 15(2), 81\u201391 (1950). https:\/\/doi.org\/10.2307\/2266967","journal-title":"J. Symb. Log."},{"key":"16_CR40","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"329","DOI":"10.1007\/978-3-030-33636-3_12","volume-title":"Mathematics of Program Construction","author":"A Kaposi","year":"2019","unstructured":"Kaposi, A., Kov\u00e1cs, A., Kraus, N.: Shallow embedding of type theory is morally correct. In: Hutton, G. (ed.) MPC 2019. LNCS, vol. 11825, pp. 329\u2013365. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-33636-3_12"},{"key":"16_CR41","doi-asserted-by":"publisher","unstructured":"Kirchner, D.: Computer-verified foundations of metaphysics and an ontology of natural numbers in Isabelle\/HOL. Ph.D. thesis, Freie Universit\u00e4t, Berlin (2022). https:\/\/doi.org\/10.17169\/refubium-35141","DOI":"10.17169\/refubium-35141"},{"issue":"1","key":"16_CR42","doi-asserted-by":"publisher","first-page":"206","DOI":"10.1017\/S1755020319000297","volume":"13","author":"D Kirchner","year":"2020","unstructured":"Kirchner, D., Benzm\u00fcller, C., Zalta, E.N.: Mechanizing principia Logico-Metaphysica in functional type theory. Rev. Symb. Log. 13(1), 206\u2013218 (2020). https:\/\/doi.org\/10.1017\/S1755020319000297","journal-title":"Rev. Symb. Log."},{"key":"16_CR43","unstructured":"Lachnitt, H.: Systematic verification of the intuitionistic modal logic cube in Isabelle\/HOL. Bachelor thesis, Freie Universit\u00e4t, Berlin (2017)"},{"key":"16_CR44","unstructured":"Lammich, P., Meis, R.: A separation logic framework for imperative HOL. Arch. Formal Proofs 2012 (2012). https:\/\/www.isa-afp.org\/entries\/Separation_Logic_Imperative_HOL.shtml"},{"key":"16_CR45","unstructured":"Lawniczak, L., Benzm\u00fcller, C.: Logical modalities within the European AI act: an analysis. In: Maranh\u00e3o, J. (ed.) Proceedings of the 20th International Conference on Artificial Intelligence and Law. Association for Computing Machinery, New York, NY, USA (2025, in print)"},{"issue":"4","key":"16_CR46","doi-asserted-by":"publisher","first-page":"372","DOI":"10.1080\/11663081.2013.841359","volume":"23","author":"E Lorini","year":"2013","unstructured":"Lorini, E.: Temporal logic and its application to normative reasoning. J. Appl. Non-Class. Log. 23(4), 372\u2013399 (2013). https:\/\/doi.org\/10.1080\/11663081.2013.841359","journal-title":"J. Appl. Non-Class. Log."},{"key":"16_CR47","unstructured":"Meder, P.: Deontic agency and moral luck. Master\u2019s thesis, University of Luxembourg (2018). https:\/\/hdl.handle.net\/10993\/39770"},{"key":"16_CR48","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"378","DOI":"10.1007\/978-3-319-21401-6_26","volume-title":"Automated Deduction - CADE-25","author":"L de Moura","year":"2015","unstructured":"de Moura, L., Kong, S., Avigad, J., van Doorn, F., von Raumer, J.: The Lean theorem prover (system description). In: Felty, A.P., Middeldorp, A. (eds.) CADE 2015. LNCS (LNAI), vol. 9195, pp. 378\u2013388. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-21401-6_26"},{"key":"16_CR49","doi-asserted-by":"publisher","unstructured":"Nipkow, T.: Hoare logics in Isabelle\/HOL. In: Schwichtenberg, H., Steinbr\u00fcggen, R. (eds.) Proof and System-Reliability, pp. 341\u2013367. Springer, Netherlands, Dordrecht (2002). https:\/\/doi.org\/10.1007\/978-94-010-0413-8_11","DOI":"10.1007\/978-94-010-0413-8_11"},{"key":"16_CR50","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL","year":"2002","unstructured":"Nipkow, T., Wenzel, M., Paulson, L.C. (eds.): Isabelle\/HOL. LNCS, vol. 2283. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45949-9"},{"key":"16_CR51","doi-asserted-by":"publisher","first-page":"561","DOI":"10.1080\/11663081.2024.2386917","volume":"34","author":"X Parent","year":"2024","unstructured":"Parent, X., Benzm\u00fcller, C.: Conditional normative reasoning as a fragment of HOL. J. Appl. Non-Class. Log. 34, 561\u2013592 (2024). https:\/\/doi.org\/10.1080\/11663081.2024.2386917","journal-title":"J. Appl. Non-Class. Log."},{"key":"16_CR52","unstructured":"Pasetto, L., Benzm\u00fcller, C.: Implementing the Fatio protocol for multi-agent argumentation in LogiKEy. In: Benzm\u00fcller, C., Otten, J., Ramanayake, R. (eds.) Proceedings of the 5th International Workshop on Automated Reasoning in Quantified Non-Classical Logics (ARQNL 2024), Nancy, France, 1 July 2024, vol. CEUR-3875, pp. 38\u201347. CEUR Workshop Proceedings. CEUR-WS.org, Nancy, France (2024). https:\/\/ceur-ws.org\/Vol-3875\/ARQNL2024_paper4.pdf"},{"key":"16_CR53","doi-asserted-by":"publisher","unstructured":"Prinz, J., Kavvos, G.A., Lampropoulos, L.: Deeper shallow embeddings. In: Andronick, J., de\u00a0Moura, L. (eds.) 13th International Conference on Interactive Theorem Proving, ITP 2022, 7\u201310 August 2022, Haifa, Israel. LIPIcs, vol.\u00a0237, pp. 28:1\u201328:18. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2022). https:\/\/doi.org\/10.4230\/LIPICS.ITP.2022.28","DOI":"10.4230\/LIPICS.ITP.2022.28"},{"key":"16_CR54","unstructured":"Rabe, M.N., Lammich, P., Popescu, A.: A shallow embedding of hyperCTL. Arch. Formal Proofs 2014 (2014). https:\/\/www.isa-afp.org\/entries\/HyperCTL.shtml"},{"key":"16_CR55","doi-asserted-by":"publisher","first-page":"110","DOI":"10.1016\/S0049-237X(08)70728-6","volume":"82","author":"H Sahlqvist","year":"1975","unstructured":"Sahlqvist, H.: Completeness and correspondence in the first and second order semantics for modal logic. Stud. Log. Found. Math. 82, 110\u2013143 (1975). https:\/\/doi.org\/10.1016\/S0049-237X(08)70728-6","journal-title":"Stud. Log. Found. Math."},{"key":"16_CR56","unstructured":"Sider, T.: Logic for Philosophy. Oxford University Press, New York (2009)"},{"key":"16_CR57","unstructured":"Smullyan, R.: A Beginner\u2019s Guide to Mathematical Logic. Dover Books on Mathematics, Dover Publications (2014). https:\/\/books.google.ae\/books?id=n6S-AwAAQBAJ"},{"issue":"5","key":"16_CR58","doi-asserted-by":"publisher","first-page":"947","DOI":"10.1007\/S10817-019-09540-0","volume":"64","author":"M Sozeau","year":"2020","unstructured":"Sozeau, M., et al.: The MetaCoq project. J. Autom. Reason. 64(5), 947\u2013999 (2020). https:\/\/doi.org\/10.1007\/S10817-019-09540-0","journal-title":"J. Autom. Reason."},{"issue":"6","key":"16_CR59","doi-asserted-by":"publisher","first-page":"775","DOI":"10.1007\/s10817-021-09588-x","volume":"65","author":"A Steen","year":"2021","unstructured":"Steen, A., Benzm\u00fcller, C.: Extensional higher-order paramodulation in Leo-III. J. Autom. Reason. 65(6), 775\u2013807 (2021). https:\/\/doi.org\/10.1007\/s10817-021-09588-x","journal-title":"J. Autom. Reason."},{"key":"16_CR60","doi-asserted-by":"publisher","unstructured":"Steen, A., Sutcliffe, G., Benzm\u00fcller, C.: Solving quantified modal logic problems by translation to classical logics. J. Log. Comput., 1\u201323 (2025). https:\/\/doi.org\/10.1093\/logcom\/exaf006","DOI":"10.1093\/logcom\/exaf006"},{"key":"16_CR61","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1007\/978-3-642-40447-4_2","volume-title":"Trends in Functional Programming","author":"J Svenningsson","year":"2013","unstructured":"Svenningsson, J., Axelsson, E.: Combining deep and shallow embedding for EDSL. In: Loidl, H.-W., Pe\u00f1a, R. (eds.) TFP 2012. LNCS, vol. 7829, pp. 21\u201336. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-40447-4_2"},{"key":"16_CR62","doi-asserted-by":"publisher","unstructured":"Wang, Z., Cao, Q., Tao, Y.: Verifying programs with logic and extended proof rules: deep embedding vs. shallow embedding. J. Autom. Reason. 68(3), 18 (2024). https:\/\/doi.org\/10.1007\/S10817-024-09706-5","DOI":"10.1007\/S10817-024-09706-5"},{"key":"16_CR63","unstructured":"Wikipedia contributors: Hilbert system \u2014 Wikipedia, the free encyclopedia (2024). https:\/\/en.wikipedia.org\/w\/index.php?title=Hilbert_system&oldid=1257978821. Accessed 18 Feb 2025"},{"key":"16_CR64","unstructured":"Zalta, E.N.: Principia Logico-Metaphysica (Draft\/Excerpt) (2025). https:\/\/mally.stanford.edu\/principia.pdf. Accessed 27 May 2025"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE 30"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-99984-0_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,29]],"date-time":"2025-07-29T11:47:49Z","timestamp":1753789669000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-99984-0_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031999833","9783031999840"],"references-count":64,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-99984-0_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"30 July 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"The authors have no competing interests to declare that are relevant to the content of this article.","order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Disclosure of Interests"}},{"value":"CADE","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Automated Deduction","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Stuttgart","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Germany","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28 July 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"31 July 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cade2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.dhbw-stuttgart.de\/cade-30\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}