github.com/cbenzmueller/LogiKEy  ·  ESSLLI 2026 LogiKEy course

LogiKEy

A logic-pluralistic framework and methodology for knowledge representation and reasoning — built on shallow and deep semantical embeddings of object logics in classical higher-order logic (HOL), so that automation and model finding transfer for free to the embedded logics.

What is LogiKEy?

LogiKEy (Logic and Knowledge Engineering) is a framework and methodology for the design, engineering and — importantly — experimentation with special-purpose reasoners, with a particular focus on legal-ethical reasoners, normative theories, and expressive classical and non-classical logics and their combinations. Pursued since 2007, the enterprise is deeply interdisciplinary, connecting computer science and AI with law, ethics, mathematics, philosophy and theology. Its unifying idea is simple and powerful: instead of building a bespoke prover for every object logic, one embeds the object logic semantically into an expressive meta-logic, classical higher-order logic (HOL), and then reasons through existing HOL provers and model finders.

These shallow semantical embeddings — more recently complemented by deep embeddings related to them through mechanised faithfulness proofs — turn HOL into a universal meta-logical workbench. A domain is then modelled across several abstraction layers — the meta-logic, the object logic(s), a domain theory, and concrete examples — each of which can be freely swapped, compared and refined. Because everything lives inside one consistent HOL formalisation, predictions can be stated precisely, tested with rigorous proof and counter-model techniques, and audited. The reference implementation combines interactive and automated reasoning: the Isabelle/HOL proof assistant working hand in hand with automated higher-order provers such as LEO-II and Leo-III, first-order and SMT provers, and (counter-)model finders.

Core Publications
Read first [1][3][15][5][4][2]

The framework paper [1] defines LogiKEy and its multi-layer methodology; the survey [3] traces the broader programme of universal (meta-)logical reasoning; the value-oriented legal reasoning study [15] demonstrates the full LogiKEy methodology at work in AI & law; the recipe paper [5] unifies deep and shallow embeddings with mechanised faithfulness proofs; the position paper [4] argues the underlying vision of logical pluralism; and the [2] Isabelle/HOL dataset makes the whole workbench reproducible.

Interdisciplinary Use of LogiKEy
Logic[9][10][11][12][13][14][21][31][39][45][46][48][49][50]
Computer Science[2][3][5][8][26][28][36][38][39][46]
AI, Law & Ethics[1][2][14][15][22][25][33][34][35][45][48][49]
AI & Health[41][42]
Mathematics[6][18][20][23][24][26][47]
Philosophy[4][17][19][20][32][37][43][44][46][47]
Theology[16][17][18][19][32][40]
Origins & History
2007–08
Roots. Shallow embeddings of (multi)modal logics in Church's simple type theory (STT) — building on Peter B. Andrews's foundational work on STT and higher-order theorem proving — developed with Lawrence C. Paulson and inspired by Chad Brown. The first such paper [31] appeared in Andrews's Festschrift: the technical seed of the whole line of work.
2009–13
Consolidation. Access-control, intuitionistic and quantified multimodal logics [9][11] are embedded in HOL, and the general recipe for combining and automating classical and non-classical logics inside classical HOL is set out [10]; faithfulness and automation are studied systematically.
2014–16
Computational metaphysics. Higher-order provers — with Bruno Woltzenlogel Paleo — verify [16] and expose a hidden inconsistency [17] in Kurt Gödel's modal ontological argument, a widely-noticed success story for AI in metaphysics. In parallel, an award-winning Freie Universität Berlin course by Alexander Steen, Max Wisniewski and Benzmüller pioneers teaching logic with interactive proof assistants [30].
2017–20
The name and the framework. Together with Xavier Parent and Leon van der Torre, the approach is consolidated into the LogiKEy framework and methodology for normative and legal-ethical reasoning — with David Fuenmayor a central contributor, Ali Farjami developing the deontic-logic and Input/Output-logic side [48], and Alexander Steen additionally advancing the Leo-III prover; the broader programme of universal (meta-)logical reasoning is surveyed in [3], and the flagship account appears in Artificial Intelligence (2020) [1]. In parallel, the computational hermeneutics programme with David Fuenmayor [43][44] — an early methodological contribution in this direction — applies the embedding approach to the iterative, human-in-the-loop logical analysis of natural-language arguments.
2021–
Expansion. Deontic, epistemic and dynamic logics [21][22] and further metaphysical case studies [20]; value-oriented legal reasoning [15]; algebraic Input/Output logic and normative reasoning under uncertainty [45]; a "deep & shallow" recipe with mechanised faithfulness proofs [5]; an explicit case for logical pluralism [4]; and symbolic approaches to trustworthy AI in healthcare and theology [40][41][42] — advanced with David Fuenmayor, Daniel Kirchner, Ali Farjami, Andrea Vestrucci and many collaborators. Much of the current momentum is carried by Luca Pasetto, whose ongoing work spans multi-agent argumentation with the Fatio protocol [37], visualizing Kripke models from Nitpick counter-models [38], epistemic rights and the right to know [24], mental privacy [36], and the case for logical pluralism [4].
Vision
Many logics, one methodology. [4] LogiKEy pursues logical pluralism rather than logical imperialism: no single foundational logic is imposed a priori. Instead, object logics — classical or non-classical, modal, deontic, epistemic, free, paraconsistent — are made flexible and negotiable inside one HOL workbench, so that researchers and, ultimately, autonomous systems can select, combine and reflect on the logic a problem actually needs. The long-term goal is trustworthy, explainable reasoning for responsible AI — machine ethics, computational law and beyond — grounded in rigorous formal methods and reproducible experiments.
Application Domains
Normative
Deontic Logics & Normative Reasoning

Obligation, permission, and the logic of norms

Standard, dyadic and preference-based deontic logics, Input/Output logic and conditional normative reasoning — embedded in HOL to handle contrary-to-duty scenarios, detachment, exceptions and non-monotonicity.

References[1][2][12][13][14][45][48][49]
Law & Ethics
Value-Oriented Legal & Ethical Reasoning

AI & Law and machine ethics

Encoding ethico-legal value ontologies and complex ethical theories, so that normative decisions can be modelled, explained and contested — a foundation for ethical governors of intelligent systems.

References[1][15][22][25][33][34][41][42]
Metaphysics
Computational Metaphysics

Gödel's ontological argument & beyond

Formal reconstruction and automated analysis of modal ontological arguments in higher-order modal logic: verifying consistency, revealing hidden assumptions and modal collapse, and comparing Gödel's, Scott's and further variants.

References[16][17][18][19][20][32][40][47]
Epistemic
Epistemic & Dynamic Logics

Knowledge, announcements, and rights

Public announcement logic with relativised common knowledge, and dynamic logics of epistemic rights and duties — including a formal logic of the right to know and reasoning about mental privacy.

References[21][22][34]
Mathematics
Foundations of Mathematics

Free logic, category theory & abstract objects

Automating free logic in HOL and using it to axiomatise category theory, and mechanising Zalta's abstract object theory (Principia Logico-Metaphysica) — LogiKEy as a tool for meta-logical and foundational investigation.

References[23][24][20]
Method
Meta-Logical Foundations & the HOL Workbench

Embeddings, faithfulness, and tools

The methodological core: classical higher-order logic as meta-logic; deep vs. shallow embeddings; mechanised faithfulness proofs between them; and the automated-reasoning toolchain (Isabelle/HOL, Sledgehammer, Nitpick, Leo-III).

References[3][5][6][7][8][9][10][11][27][28][36][38][39][46]
Logic
Reasoning Curiosities & Case Studies

From Boolos' curious inference to ethical theories

Sharp case studies that stress-test the methodology — such as the dramatic proof-length speed-up in Boolos' curious inference — alongside reconstructions of philosophical and legal arguments.

References[26][25][35][37][43][44]
Research Projects Using LogiKEy (selection)
LODEX
Logical Methods for Deontic Explanations. WEAVE research grant — a collaboration between TU Wien (PI Agata Ciabattoni), Ruhr University Bochum (PI Christian Straßer) and the University of Luxembourg (PI Leon van der Torre) (running). project page
LuCi
Logics for Utilitarian Conditional Oughts. FWF research grant PAT1007025 (running). International project participants: Christophe Salvat and Pierre Livet (Aix-Marseille Université, France), Christoph Benzmüller (University of Bamberg, Germany) and Leon van der Torre (University of Luxembourg). project page
ZLAIRE
National High-end Foreign Expert Projects. Zhejiang University, Laboratory for AI and Reasoning — Machine Ethics in Cross-Cultural Context (2023–24) and Ethical Issues in Embodied AI (2025–26, running). project page
DELIGHT
Deontic Logic for Epistemic Rights. FNR OPEN research grant O20/14776480, University of Luxembourg. project page
AuReLeE
Automated Reasoning with Legal Entities. FNR CORE research grant C20/IS/14616644, University of Luxembourg (concluded).
2014–18
Effective Higher-Order Automated Theorem Proving. DFG Research Grants Programme. GEPRIS
2012–17
Studies in Computational Metaphysics. DFG Heisenberg Programme (Heisenberg Fellowship). GEPRIS
2009–11
Kooperatives höherstufiges automatisches Beweisen zum Schließen in Ontologien. DFG Postdoctoral Fellowship. GEPRIS
Key Contributors, Users & Friends (incomplete)

LogiKEy has been shaped — and is carried forward — by many hands across the world. Among its contributors, users and friends:

Lawrence C. Paulson (University of Cambridge) · Leon van der Torre (University of Luxembourg) · Xavier Parent (TU Wien) · Dana S. Scott (Carnegie Mellon University, Berkeley) · Edward N. Zalta (Stanford University) · Beishui Liao (Zhejiang University) · Sujala Shetty (BITS Pilani Dubai) · Alexander Steen (University of Greifswald) · Geoff Sutcliffe (University of Miami) · Chad E. Brown (Czech Technical University in Prague) · Michael Kohlhase (FAU Erlangen-Nürnberg) · Florian Rabe (FAU Erlangen-Nürnberg) · Andrea Vestrucci (University of Bamberg) · David Fuenmayor · Daniel Kirchner (FU Berlin) · Luca Pasetto (University of Luxembourg) · Réka Markovich (University of Luxembourg) · Bruno Woltzenlogel Paleo · Max Wisniewski (University of Bamberg) · Bertram Lomfeld (FU Berlin) · Ali Farjami (University of Luxembourg) · Sebastian Reiche · Paul Meder · Valeria Zahoransky · Lara Lawniczak · Xu Li · Nik Sultana · …

LogiKEy in teaching. An award-winning logic course at FU Berlin, co-taught with Alexander Steen and Max Wisniewski, pioneered the classroom use of interactive and automated theorem provers — with computational metaphysics as a case study [30]; the LogiKEy teaching methodology is described by Benzmüller & Fuenmayor [29]. LogiKEy is now used in logic courses at several universities. At the University of Bamberg it underpins several courses of the AISE group — Logische Wissensrepräsentation und Schließen (David Fuenmayor & Max Wisniewski), the project course Universal Reasoning in Philosophy, Mathematics and Computer Science, and the modules AISE-UL: Universelle Logik & Universelles Schließen and AISE-PLM-V: Computational Metaphysics — Mechanizing Principia Logico-Metaphysica [20] — and Andrea Vestrucci also builds on it in his teaching (e.g., computational philosophy) and in the supervision of student projects.

Selected Talks
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: Universal (Meta-)Logical Reasoning: Recent Successes. Science of Computer Programming 172 (2019), 48–62. doi.org/10.1016/j.scico.2018.10.008
  4. C. Benzmüller, D. Kirchner, L. Pasetto: Many Logics, One Methodology: A Plea for Logical Pluralism in Formalised Reasoning. Preprint, 2026. arXiv:2605.27246
  5. C. Benzmüller: Faithful Logic Embeddings in HOL — Deep and Shallow. In: CADE-30, LNCS 15943, 280–302, Springer, 2025. doi.org/10.1007/978-3-031-99984-0_16 · arXiv:2502.19311 · AFP: FaithfulPMLinHOL · LogiKEy: 2025-CADE-DeepShallow
  6. C. Benzmüller, C. Brown, M. Kohlhase: Higher-Order Semantics and Extensionality. Journal of Symbolic Logic 69(4) (2004), 1027–1088. doi.org/10.2178/jsl/1102022211
  7. C. Benzmüller, P. Andrews: Church's Type Theory. The Stanford Encyclopedia of Philosophy, Spring 2024 edition. plato.stanford.edu/archives/spr2024/entries/type-theory-church/
  8. C. Benzmüller, D. Miller: Automation of Higher-Order Logic. In: Handbook of the History of Logic, vol. 9 — Computational Logic, 215–254, Elsevier, 2014. doi.org/10.1016/B978-0-444-51624-4.50005-8
  9. C. Benzmüller, L. C. Paulson: Multimodal and Intuitionistic Logics in Simple Type Theory. Logic Journal of the IGPL 18(6) (2010), 881–892. doi.org/10.1093/jigpal/jzp080
  10. 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) (2011), 103–128. doi.org/10.1007/s10472-011-9249-7
  11. C. Benzmüller, L. C. Paulson: Quantified Multimodal Logics in Simple Type Theory. Logica Universalis 7(1) (2013), 7–20. doi.org/10.1007/s11787-012-0052-y
  12. C. Benzmüller, A. Farjami, X. Parent: Åqvist's Dyadic Deontic Logic E in HOL. Journal of Applied Logics — IfCoLoG Journal 6(5) (2019), 733–755. collegepublications.co.uk/ifcolog/?00034
  13. C. Benzmüller, A. Farjami, P. Meder, X. Parent: I/O Logic in HOL. Journal of Applied Logics — IfCoLoG Journal 6(5) (2019), 715–732. collegepublications.co.uk/ifcolog/?00034
  14. X. Parent, C. Benzmüller: Conditional Normative Reasoning as a Fragment of HOL. Journal of Applied Non-Classical Logics 34(4) (2024). doi.org/10.1080/11663081.2024.2386917 · arXiv:2308.10686 · AFP: CondNormReasHOL · LogiKEy sources
  15. C. Benzmüller, D. Fuenmayor, B. Lomfeld: Modelling Value-oriented Legal Reasoning in LogiKEy. Logics 2(1) (2024), 31–78. doi.org/10.3390/logics2010003 · arXiv:2006.12789 · LogiKEy: EncodingLegalBalancing
  16. C. Benzmüller, B. Woltzenlogel Paleo: Automating Gödel's Ontological Proof of God's Existence with Higher-order Automated Theorem Provers. ECAI 2014, 93–98, IOS Press. doi.org/10.3233/978-1-61499-419-0-93
  17. C. Benzmüller, B. Woltzenlogel Paleo: The Inconsistency in Gödel's Ontological Argument: A Success Story for AI in Metaphysics. IJCAI 2016, 936–942. ijcai.org/Proceedings/16/Papers/137.pdf · LogiKEy: 2016-IJCAI
  18. C. Benzmüller, D. Fuenmayor: Computer-Supported Analysis of Positive Properties, Ultrafilters and Modal Collapse in Variants of Gödel's Ontological Argument. Bulletin of the Section of Logic 49(2) (2020), 127–148. doi.org/10.18778/0138-0680.2020.08 · arXiv:1910.08955 · LogiKEy: 2020-BSL
  19. 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
  20. D. Kirchner, C. Benzmüller, E. N. Zalta: Mechanizing Principia Logico-Metaphysica in Functional Type Theory. Review of Symbolic Logic 13(1) (2020), 206–218. doi.org/10.1017/S1755020319000297 · AFP: PLM
  21. 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) (2023), 1243–1269. doi.org/10.1093/logcom/exac029 · arXiv:2111.01654 · AFP: PAL · LogiKEy: Public-Announcement-Logic
  22. 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, 1623–1630, IOS Press. doi.org/10.3233/FAIA250988 · LogiKEy: LRK
  23. C. Benzmüller, D. Scott: Automating Free Logic in HOL, with an Experimental Application in Category Theory. Journal of Automated Reasoning 64(1) (2020), 53–72. doi.org/10.1007/s10817-018-09507-7 · AFP: AxiomaticCategoryTheory · LogiKEy: 2020-JAR
  24. J. Bayer, A. Gonus, C. Benzmüller, D. Scott: Category Theory in Isabelle/HOL as a Basis for Meta-logical Investigation. CICM 2023, LNCS 14101, 69–83, Springer. doi.org/10.1007/978-3-031-42753-4_5 · arXiv:2306.09074
  25. D. Fuenmayor, C. Benzmüller: Harnessing Higher-Order (Meta-)Logic to Represent and Reason with Complex Ethical Theories. PRICAI 2019, LNAI 11670, 418–432, Springer. doi.org/10.1007/978-3-030-29908-8_34 · arXiv:1903.09818 · AFP: GewirthPGCProof · LogiKEy: Gewirth
  26. 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) (2024), 442–459. doi.org/10.1093/jigpal/jzac082 · arXiv:2208.06879 · AFP: Boolos_Curious_Inference_Automated
  27. T. Nipkow, L. C. Paulson, M. Wenzel: Isabelle/HOL — A Proof Assistant for Higher-Order Logic. LNCS 2283, Springer, 2002. doi.org/10.1007/3-540-45949-9
  28. A. Steen, C. Benzmüller: Extensional Higher-Order Paramodulation in Leo-III. Journal of Automated Reasoning 65(6) (2021), 775–807. doi.org/10.1007/s10817-021-09588-x · arXiv:1907.11501
  29. C. Benzmüller, D. Fuenmayor: Mathematical Proof Assistants for Teaching Logic: The LogiKEy Methodology. Book of Abstracts — V Congress Tools for Teaching Logic, 2023. doi.org/10.13140/RG.2.2.24708.74888
  30. A. Steen, M. Wisniewski, C. Benzmüller: Einsatz von Theorembeweisern in der Lehre. Commentarii informaticae didacticae (CID) 10 (2016), 81–92, Universitätsverlag Potsdam. publishup.uni-potsdam.de/…/docId/9485
  31. C. Benzmüller, L. C. Paulson: Exploring Properties of Normal Multimodal Logics in Simple Type Theory with LEO-II. In C. Benzmüller, C. Brown, J. Siekmann, R. Statman (eds.), Reasoning in Simple Type Theory — Festschrift in Honor of Peter B. Andrews on His 70th Birthday, Studies in Logic 17, 386–406, College Publications, 2008. PDF (superseded by the 2013 Logica Universalis paper [11])
  32. C. Benzmüller: A (Simplified) Supreme Being Necessarily Exists, says the Computer: Computationally Explored Variants of Gödel's Ontological Argument. KR 2020, 779–789. doi.org/10.24963/kr.2020/80 · arXiv:2001.04701 · AFP: SimplifiedOntologicalArgument · LogiKEy: 2020-KR
  33. L. Lawniczak, C. Benzmüller: Logical Modalities within the European AI Act: An Analysis. ICAIL 2025, 348–353, ACM. doi.org/10.1145/3769126.3769202 · arXiv:2501.19112 · LogiKEy: 2025-ICAIL-Data
  34. L. Pasetto, C. Benzmüller, R. Markovich: Formalizing Mental Privacy in LogiKEy. AAMAS 2026, 3643–3645, IFAAMAS. doi.org/10.65109/PTSF2244 · LogiKEy: 2026-AAMAS-Data
  35. L. Pasetto, C. Benzmüller: Implementing the Fatio Protocol for Multi-Agent Argumentation in LogiKEy. ARQNL 2024, CEUR Vol. 3875, 38–47. ceur-ws.org/Vol-3875/ARQNL2024_paper4.pdf · LogiKEy: Fatio/v1
  36. L. Pasetto, C. Benzmüller: Visualizing Kripke Models in LogiKEy: the Case of SDL. Joint Proceedings of the ICLP 2025 Workshops, CEUR Vol. 4117, 1–9. ceur-ws.org/Vol-4117/LPLR2025_short_1.pdf · LogiKEy: Nitpick2TikZ
  37. D. Fuenmayor, C. Benzmüller: Higher-order Logic as a Lingua Franca for Logico-Pluralist Argumentation. In: Logics for New-Generation AI, 83–94, College Publications, 2022. collegepublications.co.uk/downloads/LNGAI00002.pdf · LogiKEy sources
  38. C. Rothgang, F. Rabe, C. Benzmüller: Theorem Proving in Dependently-Typed Higher-Order Logic. CADE-29, LNAI 14132, 438–455, Springer, 2023. doi.org/10.1007/978-3-031-38499-8_25 · arXiv:2305.15382 · LogiKEy: EncodingLegalBalancing
  39. 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
  40. A. Vestrucci, C. Benzmüller: Kurt Gödel and the Logical Existence of God. In: Divined Explanations: The Theological and Philosophical Context for the Development of the Sciences (1600–2000), 255–285, Brill, 2024. doi.org/10.1163/9789004701908_013
  41. A. Vestrucci, C. Benzmüller, N. Evangelatos: Symbolic Approach to Trustworthy AI: Exploration and Healthcare Case Study. ISDIA 2025, LNNS 1537, 367–379, Springer, 2025. doi.org/10.1007/978-981-96-9242-2_27
  42. A. Tenne, A. Vestrucci, C. Benzmüller: XAI in Healthcare: Analysis and Evaluation of XAI Tools and Legal Liability for Neural Networks — A Case Study on Tumor Image Classification. ISDIA 2025, LNNS 1537, 423–434, Springer, 2025. doi.org/10.1007/978-981-96-9242-2_31
  43. D. Fuenmayor, C. Benzmüller: Computational Hermeneutics: An Integrated Approach for the Logical Analysis of Natural-Language Arguments. In: Dynamics, Uncertainty and Reasoning — CLAR 2018, Logic in Asia: Studia Logica Library, 187–207, Springer, 2019. doi.org/10.1007/978-981-13-7791-4_9
  44. D. Fuenmayor, C. Benzmüller: A Computational-Hermeneutic Approach for Conceptual Explicitation. In: Model-Based Reasoning in Science and Technology, SAPERE 49, 441–469, Springer, 2019. doi.org/10.1007/978-3-030-32722-4_25 · arXiv:1906.06582
  45. A. Farjami: Normative Reasoning under Uncertainty: Algebraic Extensions of Input/Output Logic with Preferences. Annals of Mathematics and Artificial Intelligence, 2026. doi.org/10.1007/s10472-026-10010-8
  46. D. Fuenmayor: A Universal Mathematical Language for Argumentative Reasoning Agents. PhD thesis, Freie Universität Berlin, 2025. doi.org/10.17169/refubium-48234
  47. D. Kirchner: Computer-Verified Foundations of Metaphysics and an Ontology of Natural Numbers in Isabelle/HOL. PhD thesis, Freie Universität Berlin, 2022. doi.org/10.17169/refubium-35141
  48. A. Farjami: Discursive Input/Output Logic: Deontic Modals, and Computation. PhD thesis, University of Luxembourg, 2020. orbilu.uni.lu/handle/10993/44768
  49. A. Vestrucci, P. Wälde: Formalizing Value Ontologies for Smart-City Governance in Isabelle/HOL: Fixed and Context-Sensitive Preference Reasoning with Ceteris Paribus. VPR 2026 — Values & Preferences in Reasoning Symposium, AISB 2026 Convention (in press).
  50. 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

This is a curated selection. Complete, up-to-date publication lists are maintained at christoph-benzmueller.de/publications and lucapasetto.github.io. Many LogiKEy source theories and datasets are available in this repository; others are hosted elsewhere, for example in the Archive of Formal Proofs.