ESSLLI 2026  ·  Course Programme  ·  logikey.org

Experimenting with the LogiKEy Framework & Methodology

Normative Reasoning, Computational Metaphysics, and More — an introductory course in the Logic and Computation track of the 37th European Summer School in Logic, Language and Information.

Week 2: 10–14 August 2026• Mon–Fri, 17:00–18:30• Room C-221• Faculty of Civil Engineering, Czech Technical University, Prague
Christoph Benzmüller
University of Bamberg — Chair for AI Systems Engineering
FU Berlin — Dep. of Mathematics and Computer Science
christoph-benzmueller.de
Luca Pasetto
University of Luxembourg — Department of Computer Science, Computational Law and Machine Ethics group
lucapasetto.github.io
Abstract

The course provides an introduction to the LogiKEy framework and methodology for Logic and Knowledge Engineering. LogiKEy’s unifying approach is based on semantical embeddings of object logics in expressive classical higher-order logic (HOL). We begin with the methodology, introduce HOL, and give a guided practical tour of the Isabelle/HOL proof assistant. Next, we explain the technique of semantical embeddings of object logics in the meta-logic HOL, which enables the automation and model finding available in HOL provers to reason with the embedded logics.

We then apply the framework in three steps. First, we encode deontic logics and corresponding ethical or legal theories to support computational tools for normative reasoning. Second, we turn to knowledge representation within LogiKEy: combining logics, and encoding agents, actions, obligations, and knowledge; as a case study, we discuss the formalization of epistemic rights and present the embedding of a dynamic logic of the right to know in HOL. We conclude with an application in computational metaphysics: the analysis of a version of the modal ontological argument from Kurt Gödel’s papers.

Programme — Five Lectures
Lecture 1Monday
Foundations — HOL & Isabelle/HOL

General Introduction to LogiKEy

  • The LogiKEy framework and methodology
    Overview of the course. History and interdisciplinary methodology; experimentation in formal studies: representing examples, domain theories, logics, and logic combinations within a computational system.
  • HOL and Church’s type theory
    Classical higher-order logic based on Church’s type theory as an expressive meta-logical language; higher-order interactive theorem proving.
  • The Isabelle/HOL proof assistant
    Guided tour: basic warm-up; proof automation with Sledgehammer and (counter-)model finding with Nitpick; Cantor theorem and Boolos’ curious inference.
MaterialsLogiKEy Intro (PDF)HOL (PDF)Isabelle/HOL Warm-Up (PDF)LLM Demo (.thy)Liars Street (.thy)Surjective Cantor (.thy)Boolos’ Curious Inference (.thy)
Further LinksIsabelle proof assistant (TUM)HOL course notes, ESSLLI 2006 (PDF)
Further Reading[1][2][9][3][20]
Lecture 2Tuesday
Semantical Embeddings

Shallow and Deep Embeddings in HOL

  • Deep vs. shallow embeddings of logics
    Shallow Semantical Embeddings (SSE) of object logics in the meta-logic HOL; propositional logic embedding demo.
  • Embedding of propositional modal logic
    The modal logic cube in Isabelle/HOL; frame conditions such as reflexivity and transitivity; testing axioms; propositional modal logics via SSE.
  • Embedding of QBF / first-order modal logic tentative
    Quantified Boolean formulas and first-order multimodal logics via SSE; automation of faithfulness proofs; converting formulas across embeddings.
MaterialsDeep & Shallow, part 1: PML & QBF (PDF)Deep & Shallow, part 2: FML (PDF)Minimal Shallow Embedding Primer (.thy)PML sources (.zip)QBF sources (.zip)FML sources (.zip)
Further Reading[6][7][8][22][23][24]
Lecture 3Wednesday
Normative Reasoning

Normative Reasoning and Deontic Logics in HOL

  • Normative reasoning and deontic logics
    Philosophical challenges and foundations; obligation, permission, and prohibition; deontic paradoxes.
  • Deontic logics in HOL
    Embedding of Standard Deontic Logic as the modal logic KD, its semantics and limitations; preference-based and dyadic deontic logics (Åqvist’s System E) for contrary-to-duty scenarios; Input/Output logic for detachment, exceptions, and non-monotonicity; explaining normative decisions and reasoning with values.
MaterialsNormative Reasoning (PDF)Contrary-to-Duty: Preference & Dyadic Deontic Logics (PDF)
Further Reading[11][26][14]
Extra Reading[12][13]
Lecture 4Thursday
Logic Combinations

Logic Combinations in HOL: Agency, Knowledge, and Rights

  • Combining logics in the meta-logic HOL
    Knowledge representation in LogiKEy: encoding agents, actions, knowledge, and practical reasoning; epistemic–deontic combinations; maximal shallow embeddings to capture evaluation domains that vary in the evaluation of a formula.
  • Public announcement logic (PAL) tentative
    Embedding dynamic epistemic reasoning: announcements and knowledge update in HOL.
  • Epistemic rights and mental privacy tentative
    Legal relations and the problem of formalizing rights; formalizing epistemic rights and duties.
  • Case study: a dynamic logic of the Right to Know (LRK)
    Embedding of a dynamic logic of the Right to Know in HOL, illustrating how epistemic rights can be formalized and analyzed in LogiKEy.
MaterialsAgents and Rights (PDF)
Further Reading[27][19][28]
Lecture 5Friday
Computational Metaphysics — Wrapping Up

Gödel’s Ontological Argument in HOL

  • Higher-order multimodal logic (HOML)
    SSE of HOML in HOL as the formal setting for metaphysical experiments.
  • Gödel’s modal ontological argument
    The argument as presented in Gödel’s 1970 manuscript; Isabelle/HOL encoding; how automated theorem provers verify consistency and identify hidden assumptions — and how they revealed a previously unnoticed inconsistency in Gödel’s original argument.
  • Positive properties and Scott’s variant
    Gödel’s notion of positive properties and how it constitutes a (modal) ultrafilter; Dana Scott’s variant of the argument and its Isabelle/HOL encoding.
  • Wrap-up and outlook
    Comments on open problems, unification, and future directions.
MaterialsGödel — God & the Devil (PDF)
Further Reading[16][17][18][21]
Expected Level & Prerequisites

Introductory course (Logic and Computation track). In order to benefit from this course, participants are expected to have a basic understanding of discrete mathematics, propositional logic, and modal logic. The course is highly interdisciplinary and will also appeal to students from machine ethics, legal theory, AI & Law, and philosophy.

Selected References
  1. C. Benzmüller, X. Parent, L. van der Torre: Designing Normative Theories for Ethical and Legal Reasoning: LogiKEy Framework, Methodology, and Tool Support. Artificial Intelligence 287 (2020). doi.org/10.1016/j.artint.2020.103348 · arXiv:1903.10187 · LogiKEy sources
  2. C. Benzmüller, A. Farjami, D. Fuenmayor, P. Meder, X. Parent, A. Steen, L. van der Torre, V. Zahoransky: LogiKEy Workbench: Deontic Logics, Logic Combinations and Expressive Ethical and Legal Reasoning (Isabelle/HOL dataset). Data in Brief 33 (2020). doi.org/10.1016/j.dib.2020.106409 · LogiKEy: 2020-DataInBrief-Data
  3. C. Benzmüller, P. Andrews: Church’s Type Theory. In: The Stanford Encyclopedia of Philosophy, Spring 2024 edition. plato.stanford.edu/archives/spr2024/entries/type-theory-church/
  4. C. Benzmüller, D. Fuenmayor, A. Steen, G. Sutcliffe: Who Finds the Short Proof? An Exploration of Variants of Boolos’ Curious Inference using Higher-order Automated Theorem Provers. Logic Journal of the IGPL 32(3): 442–459, 2024. doi.org/10.1093/jigpal/jzac082 · arXiv:2208.06879 · AFP: Boolos_Curious_Inference_Automated
  5. C. Benzmüller, D. Fuenmayor, A. Steen, G. Sutcliffe: Automation of Boolos’ Curious Inference in Isabelle/HOL. Archive of Formal Proofs, 2022. isa-afp.org/entries/Boolos_Curious_Inference_Automated.html
  6. C. Benzmüller: Faithful Logic Embeddings in HOL — Deep and Shallow. In: CADE-30, LNCS 15943, pp. 280–302, Springer, 2025. doi.org/10.1007/978-3-031-99984-0_16 · arXiv:2502.19311 · AFP: FaithfulPMLinHOL · LogiKEy: 2025-CADE-DeepShallow
  7. C. Benzmüller: Faithful Logic Embeddings in HOL — Deep and Shallow (Isabelle/HOL dataset). Archive of Formal Proofs, 2025. isa-afp.org/entries/FaithfulPMLinHOL.html
  8. C. Benzmüller, D. Kirchner: First-Order Modal Logic in HOL: Deep and Shallow Embeddings with Automated Faithfulness. ARQNL 2026. Extended preprint with source-code appendix: arXiv:2607.10880
  9. C. Benzmüller, D. Kirchner, L. Pasetto: Many Logics, One Methodology: A Plea for Logical Pluralism in Formalised Reasoning. To appear. Preprint: arXiv:2605.27246
  10. C. Benzmüller, M. Claus, N. Sultana: Systematic Verification of the Modal Logic Cube in Isabelle/HOL. PxTP 2015, EPTCS 186, pp. 27–41. doi.org/10.4204/EPTCS.186.5
  11. X. Parent, L. van der Torre: Introduction to Deontic Logic and Normative Systems. College Publications, 2018. collegepublications.co.uk/TLR/?00001
  12. D. Gabbay, J. Horty, X. Parent, R. van der Meyden, L. van der Torre (eds.): Handbook of Deontic Logic and Normative Systems, vol. 1. College Publications, 2013. collegepublications.co.uk/handbooks/?00001
  13. D. Gabbay, J. Horty, X. Parent, R. van der Meyden, L. van der Torre (eds.): Handbook of Deontic Logic and Normative Systems, vol. 2. College Publications, 2021. collegepublications.co.uk/handbooks/?00005
  14. C. Benzmüller, A. Farjami, X. Parent: Åqvist’s Dyadic Deontic Logic E in HOL. Journal of Applied Logics — IfCoLoG Journal 6(5): 733–755, 2019. collegepublications.co.uk/ifcolog/?00034
  15. C. Benzmüller, D. Fuenmayor, B. Lomfeld: Modelling Value-oriented Legal Reasoning in LogiKEy. Logics 2(1): 31–78, 2024. doi.org/10.3390/logics2010003 · arXiv:2006.12789 · LogiKEy: EncodingLegalBalancing
  16. C. Benzmüller, D. Scott: Notes on Gödel’s and Scott’s Variants of the Ontological Argument. Monatshefte für Mathematik, 2025. doi.org/10.1007/s00605-025-02078-x · AFP: Notes_On_Goedels_Ontological_Argument
  17. C. Benzmüller, D. Scott: Notes on Gödel’s and Scott’s Variants of the Ontological Argument (Isabelle/HOL dataset). Archive of Formal Proofs, 2025. isa-afp.org/entries/Notes_On_Goedels_Ontological_Argument.html
  18. C. Benzmüller, B. Woltzenlogel Paleo: Automating Gödel’s Ontological Proof of God’s Existence with Higher-order Automated Theorem Provers. ECAI 2014, IOS Press, pp. 93–98. doi.org/10.3233/978-1-61499-419-0-93
  19. L. Lawniczak, L. Pasetto, C. Benzmüller, X. Li, R. Markovich: Reasoning with Epistemic Rights and Duties: Automating a Dynamic Logic of the Right to Know in LogiKEy. ECAI 2025, pp. 1623–1630, IOS Press. doi.org/10.3233/FAIA250988 · LogiKEy: LRK
  20. C. Benzmüller, C. Brown, M. Kohlhase: Higher-Order Semantics and Extensionality. Journal of Symbolic Logic 69(4): 1027–1088, 2004. doi.org/10.2178/jsl/1102022211
  21. C. Benzmüller, B. Woltzenlogel Paleo: The Inconsistency in Gödel’s Ontological Argument: A Success Story for AI in Metaphysics. IJCAI 2016, pp. 936–942. ijcai.org/Proceedings/16/Papers/137.pdf · LogiKEy: 2016-IJCAI
  22. C. Benzmüller, L. C. Paulson: Multimodal and Intuitionistic Logics in Simple Type Theory. Logic Journal of the IGPL 18(6): 881–892, 2010. doi.org/10.1093/jigpal/jzp080
  23. C. Benzmüller, L. C. Paulson: Quantified Multimodal Logics in Simple Type Theory. Logica Universalis 7(1): 7–20, 2013. doi.org/10.1007/s11787-012-0052-y
  24. C. Benzmüller: Combining and Automating Classical and Non-classical Logics in Classical Higher-Order Logic. Annals of Mathematics and Artificial Intelligence 62(1–2): 103–128, 2011. doi.org/10.1007/s10472-011-9249-7
  25. C. Benzmüller, D. Kirchner: Monadic Second-Order Logic in HOL: Deep and Shallow Embeddings with Automated Faithfulness (Isabelle/HOL dataset). Archive of Formal Proofs, 2026. AFP: MSOinHOL
  26. X. Parent, C. Benzmüller: Conditional Normative Reasoning as a Fragment of HOL. Journal of Applied Non-Classical Logics 34(4): 561–592, 2024. doi.org/10.1080/11663081.2024.2386917 · arXiv:2308.10686 · AFP: CondNormReasHOL · LogiKEy sources
  27. C. Benzmüller, S. Reiche: Automating Public Announcement Logic with Relativized Common Knowledge as a Fragment of HOL in LogiKEy. Journal of Logic and Computation 33(6): 1243–1269, 2023. doi.org/10.1093/logcom/exac029 · arXiv:2111.01654 · AFP: PAL · LogiKEy: Public-Announcement-Logic
  28. L. Pasetto, C. Benzmüller, R. Markovich: Formalizing Mental Privacy in LogiKEy. AAMAS 2026, pp. 3643–3645, IFAAMAS. doi.org/10.65109/PTSF2244 · LogiKEy: 2026-AAMAS-Data
  29. C. Benzmüller, D. Kirchner: A Deep Embedding of HOL in HOL: Soundness, Completeness, Consistency (Isabelle/HOL dataset). Archive of Formal Proofs, 2026. AFP: HOL_in_HOL_Deep