Paper deep dive

Mathematical Proof Assistants for Teaching Logic: The LogiKEy Methodology

Christoph Benzmüller, David Fuenmayor, Luca Pasetto

Year: 2026Venue: arXiv preprintArea: cs.AIType: PreprintEmbeddings: 99

Intelligence

Status: not_run | Model: - | Prompt: - | Confidence: 0%

Entities (0)

No extracted entities yet.

Relation Signals (0)

No relation signals yet.

Cypher Suggestions (0)

No Cypher suggestions yet.

Abstract

Abstract:We report on an approach to teaching logic to mixed groups of computer science, mathematics, and philosophy students, based on the logico-pluralistic LogiKEy methodology, used for more than a decade in courses, summer schools, and tutorials. LogiKEy uses classical higher-order logic (HOL) as a universal metalogic in which object logics, classical and non-classical alike, are encoded by defining their semantics; through these semantical embeddings a single proof assistant (e.g. Isabelle/HOL), with its automated theorem provers and (counter-)model finders, becomes one environment in which students learn, experiment with, and compare logics. After making the pedagogical case for proof assistants in the logic classroom, we present a graded sequence of classroom examples, each transition motivated by a limitation of the preceding representation, by a need for more explicit modelling resources, or by a new application. A liars-and-truth-tellers puzzle leads from propositional to modal logic; the Wise Men puzzle leads on to dynamic epistemic logic; Boolos's curious inference illustrates what a higher-order meta-logic buys, even for automated proof search; Chisholm's paradox takes the sequence into deontic logic, and from standard to dyadic deontic logic; and Gödel's ontological argument brings it to a research-level metaphysical argument. We then rebut the objection that embedding everything in classical HOL is monism rather than pluralism, reflect on three years of teaching such a course, and sketch the portability of the approach beyond Isabelle.

PDF

Open source PDF →Open local PDF →

Trouble viewing inline? Open PDF directly →

Full Text

95,672 characters extracted from source content.

Expand or collapse full text

Mathematical Proof Assistants for Teaching Logic: The LogiKEy Methodology Christoph Benzmüller Affiliation: Otto-Friedrich-Universität Bamberg, Germany, and Freie Universität Berlin, Germany, E-mail: christoph.benzmueller@uni-bamberg.de David Fuenmayor Affiliation: Otto-Friedrich-Universität Bamberg, Germany, E-mail: david.fuenmayor@uni-bamberg.de and Luca Pasetto Affiliation: University of Luxembourg, Luxembourg, E-mail: luca.pasetto@uni.lu Abstract We report on an approach to teaching logic to mixed groups of computer science, mathematics, and philosophy students, based on the logico-pluralistic LogiKEy methodology, used for more than a decade in courses, summer schools, and tutorials. LogiKEy uses classical higher-order logic (HOL) as a universal meta-logic in which object logics, classical and non-classical alike, are encoded by defining their semantics; through these semantical embeddings a single proof assistant (e.g. Isabelle/HOL), with its automated theorem provers and (counter-)model finders, becomes one environment in which students learn, experiment with, and compare logics. After making the pedagogical case for proof assistants in the logic classroom, we present a graded sequence of classroom examples, each transition motivated by a limitation of the preceding representation, by a need for more explicit modelling resources, or by a new application. A liars-and-truth-tellers puzzle leads from propositional to modal logic; the Wise Men puzzle leads on to dynamic epistemic logic; Boolos’s curious inference illustrates what a higher-order meta-logic buys, even for automated proof search; Chisholm’s paradox takes the sequence into deontic logic, and from standard to dyadic deontic logic; and Gödel’s ontological argument brings it to a research-level metaphysical argument. We then rebut the objection that embedding everything in classical HOL is monism rather than pluralism, reflect on three years of teaching such a course, and sketch the portability of the approach beyond Isabelle. 1 The Logic Pluralism Challenge in Logic Education Logic is a mandatory, and notoriously demanding, subject in the curricula of several disciplines at once. In computer science it underpins verification, knowledge representation, and the theory of computation; in mathematics it supplies the language of proof; in linguistics it underpins the formal semantics of natural language; and in philosophy it is at once a tool and an object of study. Yet these audiences arrive with very different backgrounds, motivations, and tolerances for formalism. Teaching logic well is therefore, first of all, an interdisciplinary challenge: the same room may hold a student who programs fluently but has never written a proof, one who writes rigorous proofs but has never seen them checked by a machine, and one who argues subtly in natural language but freezes at a quantifier Wisniewski et al., 2016; Benzmüller and Fuenmayor, 2023. A second challenge concerns content. The applications that make logic attractive today (artificial intelligence, natural-language semantics, the formal analysis of law and ethics) routinely require reasoning beyond classical first-order logic: modal, deontic, epistemic, temporal, and many further non-classical logics, often in combination. The traditional response is to teach each such logic with its own syntax, its own proof calculus, and, where tool support exists at all, its own software. For a mixed and time-limited student audience this fragmentation is costly: every new logic looks like a fresh start, and the conceptual thread (what all these logics have in common, and how they differ) is easily lost. This chapter reports on an approach that addresses both challenges together. Its guiding idea is to fix a single, sufficiently expressive meta-logic, classical higher-order logic (HOL), and to obtain the many object logics of interest inside it, by means of semantical embeddings: encodings that define, within HOL, the semantics of each object logic.11 1 “Semantical embedding” is the term established in the LogiKEy literature; what is embedded into HOL is the semantics of the object logic. Despite the surface similarity, the term is unrelated to the vector “embeddings” of machine learning. Sect. 2.2 explains the technique by example. A single proof assistant, in our courses Isabelle/HOL, then provides one uniform working environment, complete with automated theorem provers and (counter-)model finders, in which a heterogeneous student group can learn, experiment with, and, crucially, compare logics. This is the pedagogical face of the LogiKEy methodology for logic and knowledge engineering Benzmüller et al., 2020b; Benzmüller et al., 2024a; Benzmüller, 2019; Benzmüller and Fuenmayor, 2023. Our thesis is that such a platform lets a mixed cohort learn many logics uniformly, with immediate machine-checked feedback, along a single path that runs from elementary logic puzzles up to research-grade arguments in ethics and metaphysics. In the vocabulary of this volume, the approach answers its three organising questions at once. How to teach logic: by machine-supported, exploratory practice. What tools to use: a general-purpose proof assistant repurposed for teaching. What to teach: a plurality of logics, presented uniformly rather than in isolation. The last point connects our proposal to the broader case, made elsewhere in this volume, for teaching logic in a pluralistic and application-aware spirit;22 2 See, in the “Philosophy” part of this volume, the contributions on teaching logic as formal philosophy and on teaching non-classical logics through the Liar paradox, with which our computational proposal is in close sympathy. what we add is a concrete, executable way to realise it in the classroom. In sum, this chapter contributes (i) a pedagogical case for teaching many logics uniformly within a proof assistant; (i) a graded sequence of classroom examples, from a liars-and-truth-tellers puzzle to Gödel’s ontological argument, in which each transition is motivated by a limitation exposed in the preceding representation, by a need for more explicit modelling resources, or by a new application, so that students examine different reasons for changing a logic or its formalisation. It further contributes (i) an account of the supporting tools, including automated assessment and a Kripke-model visualiser, and (iv) a reflection on three years of teaching such a course to a mixed audience. A word on what is, and is not, new. LogiKEy itself is an established research programme, and a two-page abstract under the same title Benzmüller and Fuenmayor, 2023 already sketched the idea of teaching with it. What is new here is the worked course and its rationale (Sect. 4), the tools that make it usable by non-specialists (Sect. 5), the positioning of the meta-logical stance against the charge of monism (Sect. 2.4), and a sketch of portability to other proof assistants (Sect. 7). Underlying all of these is one thread we ask the reader to follow: what is gained is not simply that a proof assistant is used, but that a single expressive meta-logic is. Its expressiveness buys an economy of formalisation, since each further object logic is a set of definitions rather than a new system; that economy in turn buys automation, since every embedded logic inherits the same provers and model finders; and only on top of these does the teaching application rest. Boolos’s inference (Sect. 4) shows that the first of these steps can pay off even where one would least expect it. The chapter belongs to the Programmes part of this volume: it describes a methodological infrastructure and a concrete teaching application, not an empirical study of learning. We write for logic educators and for readers from philosophy, mathematics, and computer science who have not necessarily used a proof assistant. A basic acquaintance with propositional and modal logic suffices. The Isabelle/HOL listings are illustrative and can be read as annotated pseudo-code; no knowledge of Isabelle, type theory, or programming is assumed, and the same holds for the students in the course described below. Adopting the infrastructure is a different matter: instructors will find the complete, machine-checked sources openly available (Sect. 7), but putting them to work does require an initial investment in the tools. 2 The LogiKEy Idea in One Picture The whole approach rests on one central idea, which we now explain once so that the later sections can take it for granted. The idea has three ingredients: a meta-logic, an embedding technique, and a layered architecture. We keep the treatment deliberately light, introducing only what the classroom examples of Sect. 4 require: enough to follow the proofs and countermodels that follow. 2.1 Higher-order logic as a universal meta-logic Classical higher-order logic, Church’s simple type theory Benzmüller and Andrews, 2024, is ordinary classical logic with two decisive additions. One may quantify not only over individuals but also over functions and predicates, which makes HOL expressive enough to talk about other logics: their formulas, their notions of truth, their models. And one may form functions on the fly by λ-abstraction, which makes encodings compositional and elegant and gives them the flavour of elementary functional programming: a modal connective, for instance, simply becomes a function on world-dependent propositions (Sect. 2.2). LogiKEy exploits both, using HOL as a universal meta-logic Benzmüller, 2019. Students need no prior acquaintance with type theory to use it; in practice they meet HOL simply as the language of the proof assistant, and its higher-order features appear exactly when, and only when, a particular object logic calls for them. 2.2 Semantical embeddings, by example The technique by which LogiKEy turns HOL into a host for other logics is shallow semantical embedding (SSE) Benzmüller, 2019; Benzmüller, 2025; a deep alternative is discussed in Sect. 2.4. The idea is best seen on propositional modal logic. Read a modal formula not as an opaque symbol but as a predicate on possible worlds: “φ holds” becomes “φ holds at a world w”. Necessity is then nothing but truth at all accessible worlds. Writing σ for the type of such world-predicates (the listings use the same name) and R for the accessibility relation, the modal connectives are defined in HOL by ¬φ :=λw.¬(φw), \;:=\;λ w.\; \,( \,w), φ→ψ →ψ :=λw.φw⟶ψw, \;:=\;λ w.\; \,w ψ\,w, □φ :=λw.∀v.Rwv⟶φv, \;:=\;λ w.\;∀ v.\;R\,w\,v \,v, ⌊φ⌋ :=∀w.φw, \;:=\;∀ w.\; \,w, (1) where ⌊φ⌋ (“φ is valid”) abbreviates truth at every world. Wherever the two levels meet in one formula, as they do here, we set the object-level connectives in bold: the ¬ and □ on the left are being defined, the ¬ , ⟶ and ∀ on the right are HOL’s own. The notation λw.…λ w.\,… denotes the function that assigns to each world w the truth value described after the dot; so ¬φ , for instance, is the proposition that is true at exactly those worlds at which φ is false. That is the entire definition of the modal logic K: everything else (the axiom K, the necessitation rule, and all theorems) is a consequence of these definitions, obtained by ordinary reasoning in HOL rather than stipulated. In Isabelle/HOL the definitions of (1) are a handful of lines, after which one can already state and prove modal facts (Fig. 1).33 3 Throughout, the Isabelle/HOL code is shown as Isabelle displays it, with the usual logical symbols, and occasionally deliberately simplified for a non-specialist reader. The faithful, machine-checked sources are openly available (cf. Sect. 7). Because the embedding is so direct, an off-the-shelf HOL prover reasons in the modal logic for free; just as importantly, a HOL (counter-)model finder produces modal countermodels when a conjecture fails. (What such a countermodel looks like, first as the model finder prints it and then as a picture, is shown in Figs. 9 and 7 below.) ⬇ (* axiom K holds in every frame (a consequence of the definitions): *) lemma K: "⌊□⁡(p→q)→(□p→□q)⌋ (p →q) →( p → q) " by simp (* correspondence: the ’T’ schema holds exactly on reflexive frames: *) lemma Tc: "(∀ p. ⌊□p→p⌋ p →p ) = (∀ x. R x x)" by metis (* without reflexivity, Nitpick refutes the schema: *) lemma "⌊□p→p⌋ p →p " nitpick Figure 1: Working with the embedding (1). Axiom K is proved in every frame. The schema □φ→φ → is shown to correspond exactly to reflexivity of the accessibility relation, and without reflexivity Nitpick returns a countermodel: proof and refutation are the same one-line gesture. (The plain ∀ and R are meta-level; the bold □ and → → are the embedded object connectives. simp and metis are automatic proof methods; they do construct proofs, which Isabelle checks but does not normally display, and any of them can be replaced by a step-by-step proof in Isabelle’s Isar language.) The pedagogical dividend appears the moment one varies the frame. Imposing a condition on R selects a stronger logic: reflexivity yields KT, seriality yields KD (the base of deontic logic, of which more in Sect. 4), transitivity yields K4, and so on up to S5. Students do not take these correspondences on faith: they test them, and watch the same machinery deliver a different logic each time. One meta-logic, many object logics: this refrain returns throughout the chapter. 2.3 A layered architecture—and why it helps LogiKEy organises this idea into four layers (Fig. 2). At the base (L0) sits the meta-logic, HOL. On top of it one encodes object logics and their combinations (L1). Using those logics one formulates domain-specific languages, theories, and ontologies (L2). With these in hand one models and assesses concrete application scenarios (L3) Benzmüller et al., 2020b; Pasetto and Benzmüller, 2025.44 4 In the framework paper Benzmüller et al., 2020b the three engineered layers L1–L3 rest on the meta-logic HOL as a substrate; we simply number that substrate L0. For teaching, the layering has a pleasant consequence. Students can enter at the layer that suits their background, a philosopher at L2/L3 with an ethical scenario, a computer scientist at L0/L1 with the embedding machinery, and still meet on the same platform and speak the same underlying language. The architecture thus doubles as a map of an interdisciplinary division of labour. L3 — ApplicationsL2 — Domain-Specific Languages, Theories, OntologiesL1 — Object Logic(s) and their CombinationsL0 — Meta-Logic (HOL)LogiKEy Figure 2: The four layers of the LogiKEy methodology. Object logics are embedded in HOL (L0→ 1), used to build domain theories (L2), and applied to concrete scenarios (L3). Students may enter at the layer matching their discipline. The tools the student actually touches are few. Isabelle/HOL Nipkow et al., 2002 is the surface: a mature, well-documented proof assistant with a modern editor. Behind a single command, Sledgehammer Blanchette et al., 2016 invokes external automated theorem provers to find proofs, while Nitpick Blanchette and Nipkow, 2010 searches for (counter-)models. For the learner these are a proof-finding and a refutation companion (Sect. 5). For interactive proof, Isabelle offers, among various other proof languages, Isar: a declarative language modelled on the way mathematicians argue, in which a machine-checked proof reads like a structured argument. 2.4 Semantical embeddings and logical pluralism The embedding technique is not new. Shallow semantical embeddings grew out of the automation of multimodal and quantified multimodal logics in simple type theory Benzmüller and Paulson, 2008; Benzmüller and Paulson, 2013; for an overview see Benzmüller, 2019. A companion deep style, in which the object syntax is represented as a datatype with an explicit interpretation function, has been worked out alongside it. For simple logics such as propositional modal logic it has been proved by machine that the two styles are faithful: they prove exactly the same formulas, so the object logic is captured correctly Benzmüller, 2025. (That paper was itself written with logic education in mind.) For teaching, the shallow style is the natural default: it is short, readable, and lets the prover work directly on object-level formulas (Fig. 3 shows the difference on the box). A further dividend of embedding a logic, rather than hard-coding it, is that one reasons at two levels at once. The same machinery that proves object-level theorems also establishes facts about the logic, such as the frame correspondences of Sect. 2.2, and finds countermodels when either fails. ⬇ (* shallow: the box is a HOL definition on world-predicates (type σ = i ⇒ bool) *) definition box :: "σ ⇒ σ" ("□ ") where "□ p = (%w. ∀ v. R w v ⟶ p v)" (* deep: formulas are a datatype, evaluated by an explicit interpretation function *) datatype form = Atom nat | Neg form | Imp form form | Box form consts val :: "nat ⇒ i ⇒ bool" (* valuation of the atoms, a constant like R *) fun eval :: "form ⇒ i ⇒ bool" where "eval (Atom n) w = val n w" | "eval (Box f) w = (∀ v. R w v ⟶ eval f v)" | ... Figure 3: The two styles of embedding, on the box (schematic; the deep evaluation function is shown for the atom and box cases only). In the shallow style the object connective simply is a HOL function on world-predicates, so the prover works on object formulas directly. In the deep style object formulas are data, and a separate evaluation function assigns them a meaning; this makes the syntax itself an object of study, at the price of one more level of indirection. Faithfulness means that both styles validate exactly the same formulas Benzmüller, 2025. Conceptually, the method turns logical pluralism from a slogan into a practice. Instead of treating each logic as a self-contained system with its own calculus, one exhibits many logics as definitional variants within a single framework, and can compare them, combine them, and move between them without changing tools. This computational pluralism sits naturally beside the philosophical case, made elsewhere in this volume, for teaching logic as formal philosophy and for taking a plurality of logics seriously in the curriculum; it offers a concrete, executable counterpart to those arguments. A philosopher will rightly press the obvious objection: if every object logic is interpreted in classical HOL, is this not in truth a classical monism in disguise, and the “pluralism” merely cosmetic? The reply we and others give Benzmüller et al., 2026 distinguishes a methodology from a foundation. LogiKEy does not enthrone HOL as the one true logic in which all reasoning must be conducted: the choice of HOL rests on pragmatic grounds (its expressiveness and its mature automation) and is not constitutive of the method. What is constitutive is that the object logic, and to some extent even the meta-logic, are kept negotiable and made objects of study. A single rich foundation, by contrast, silently embeds commitments, such as excluded middle, the axiom of choice, existential import, or extensionality, that remain opaque to the user and against which any dissenter must work: a foundation forecloses, whereas a methodology explores Benzmüller et al., 2026. This exploration pays off in practice: when Zalta’s object theory was encoded as an object logic in HOL, the interaction with Isabelle/HOL brought to light a paradox that had been inadvertently reintroduced and had previously gone undetected Kirchner et al., 2020; Benzmüller et al., 2026. A smaller example, taken from Rung 4 below, shows how such a commitment enters a formalisation. Do the quantifiers of the object logic range over all possible individuals, or only over those that actually exist at a world? This choice between a possibilist and an actualist reading is invisible in the informal text of Gödel’s ontological argument. In the encoding it is a single definitional decision, and which results remain provable, and under which frame conditions, depends on it Fuenmayor and Benzmüller, 2017; Benzmüller and Scott, 2025. Making the choice explicit is what allows it to be varied and discussed in class. The stance is thus pluralism set deliberately against a logical imperialism (the term is from Benzmüller et al., 2026) that would impose one logic on every problem. In the classroom it has a welcome corollary: no student’s “home” logic is crowned the winner, and the differences between logics, not one orthodoxy, become the subject matter. 3 Why a Proof Assistant in the Logic Classroom Before turning to concrete classroom material, we set out the pedagogical case for using an interactive proof assistant to teach logic. Our experience builds on an earlier line of work on theorem provers in teaching Wisniewski et al., 2016, and our courses follow the Humboldtian ideal of a unity of research and teaching: they aim at a research-oriented education that can culminate in students reproducing current research results Wisniewski et al., 2016. A word on the status of the claims that follow. Three kinds of claim run through this chapter. Formal results (that a given formula is provable or refutable) are machine-checked and reported as such in Sect. 4. Methodological claims (that one framework can carry all of these logics uniformly) are borne out by the worked examples. The pedagogical claims of this section, and the classroom observations of Sect. 6, rest on our own teaching experience: three runs of one course with small, self-selected cohorts, and earlier courses in the same line. We offer them as considered impressions and as hypotheses worth testing, not as findings of a controlled study. Immediate, machine-checked feedback—no hidden gaps. On paper, the reasoning steps a student finds “obvious” are often the ones that hide errors, and feedback arrives days later, if at all. In a proof assistant every step is checked as it is made; a gap cannot be waved away, because the system will not accept it. The effect, in our experience, is not punitive but clarifying: students learn where an inference’s real content lies. Logic as an experimental subject. With proof search and model finding one command away, students can try things: Does this formula hold on this class of frames? What happens if I drop seriality? Which axioms separate modal logic S4 from S5? The proof assistant turns questions that would otherwise be rhetorical into experiments with immediate answers, encouraging a habit of conjecture-and-test that is closer to mathematical practice than to rote calculation Benzmüller and Fuenmayor, 2023. What students actually do. Sessions begin with small, complete, runnable theories that students execute and modify rather than read passively: change an axiom and watch a theorem turn into a countermodel; strengthen a frame condition and watch the countermodel turn back into a proof. The core task is formalisation: rendering an informal statement (a puzzle, a philosophical principle, a legal rule) in a chosen object logic and asking the machine whether the intended conclusions follow. This targets the skill a mixed audience most needs and most lacks, namely moving carefully between natural language and formal notation, now with an oracle to catch mistakes (and, more recently, with language models to draft a first attempt; see Sect. 5). Assignments are correspondingly open-ended (“model this scenario and decide whether…”, “find a countermodel showing that…”) rather than narrow calculations, because automatic checking makes such tasks tractable both to set and to assess. This iterative loop of formalising, testing, and revising has a philosophical side as well: it is a form of computational hermeneutics, in which the meaning of an informal concept is made explicit precisely by the succession of formalisations the machine accepts and rejects Fuenmayor and Benzmüller, 2019. A dialogical style of learning. Used this way, the system becomes a partner in a dialogue between the learner and the material: pose a claim, attempt a proof, inspect a countermodel, revise. This fits the model of dialogical learning of Ruf and Gallin, in which a core idea, an open-ended commission, a learning journal, and feedback chain production and reception into an iterative loop Wisniewski et al., 2016. A proof assistant is unusually well suited to play the machine side of this dialogue. An Isabelle theory accumulated over a term is a formally verified learning journal: a record of a student’s reasoning in which every accepted step is guaranteed correct, and in which even unsuccessful attempts can be preserved and annotated for later reflection. Exemplary passages from such journals can be curated into a shared collection and fed back to the class as new learning material Wisniewski et al., 2016, and since Isabelle typesets a theory into a PDF, a journal doubles as a publishable, machine-checked document. The division of labour in this dialogue is worth stating plainly: the assistant supplies reliable formal feedback, and interpreting that feedback, connecting it to the logical or philosophical question behind it, remains the student’s work. Lowering the barrier—and the affective payoff. A recurring worry about formal methods in teaching is that the tooling itself becomes the obstacle. Two features mitigate this. First, one starts from very small, self-contained examples and grows them; nothing must be built from scratch. Second, the machine’s willingness to refute a plausible conjecture, and to reward a second or third attempt at a proof, seems to us to encourage the dispositions that a virtue-oriented view of logic education prizes: open-mindedness, humility, persistence. It may also help defuse the ‘logic anxiety’ that formal notation provokes in humanities-trained students. Both are impressions from our courses rather than measured effects.55 5 Both themes are taken up elsewhere in this volume, in the contributions on the epistemology of virtues and on logic anxiety, respectively. 4 A Course Walkthrough: The Graded Ladder We now show the methodology in action, as a graded progression of classroom examples that students climb like the rungs of a ladder: each rung is a new logic, reached from the one below it. The concrete setting is a lecture course with tutorial, Universal Logic and Universal Reasoning (AISE-UL), taught by two of us at the University of Bamberg in three successive winter terms (2022/23, 2023/24, 2024/25). It is a 2+22+2 SWS, 66 ECTS course for computer-science students, offered to philosophy students as a 33 ECTS seminar variant Benzmüller and Fuenmayor, 2023. It continues a line of teaching that runs through the first author’s Universal Logical Reasoning course at the Freie Universität Berlin (from winter 2018/19) back to the Computational Metaphysics course, which won the university’s central teaching prize for 2015 and ran in the summer of 2016 Benzmüller et al., 2015c.66 6 The prize, awarded to teaching concepts to be realised in the following academic year, was announced on 1 February 2016; see the FU Berlin press release No. 022/2016, https://w.fu-berlin.de/presse/informationen/fup/2016/fup_16_022-lehrpreis-benzmueller-logik-gottesbeweis/index.html. That course was designed and taught together with Max Wisniewski and Alexander Steen Benzmüller et al., 2015c; Wisniewski et al., 2016; Steen went on to become a contributor to and developer of LogiKEy, and he now pursues the same line, with a stronger emphasis on proof automation, as junior professor at the University of Greifswald. The course has also yielded what this chapter hopes for: two of its participants went on to write their theses, up to the doctoral level, in the same line. One began with a master’s thesis mechanising Zalta’s Principia Logico-Metaphysica, the work in which the paradox recounted in Sect. 2.4 came to light Kirchner, 2017; Kirchner et al., 2020, and completed a doctorate on computer-verified foundations of metaphysics Kirchner, 2022. The other is the second author of this chapter. He began with a bachelor’s thesis that applied the method to Lowe’s modal ontological argument Fuenmayor, 2018; Fuenmayor and Benzmüller, 2018. A series of publications followed, on the ontological argument, on computational hermeneutics, and on the normative applications and the Boolos example on which this chapter draws Fuenmayor and Benzmüller, 2017; Fuenmayor and Benzmüller, 2019; Fuenmayor and Benzmüller, 2020; Benzmüller et al., 2024a; Benzmüller et al., 2024b, before a doctorate on a universal formal language for argumentative reasoning agents Fuenmayor, 2025. The name LogiKEy, and the methodology’s international spread, date from the first author’s years at the University of Luxembourg, where Xavier Parent and Leendert van der Torre became convinced of its virtues and joined its development Benzmüller et al., 2020b. The methodology reaches well beyond this one course: it has been used in graduate courses on computational metaphysics and on intelligent agents (the latter at the University of Luxembourg), in invited courses and an ongoing research collaboration at Zhejiang University in China,77 7 The invited lecture course Universal Logical Reasoning (2020, part of a course on Logic in AI; https://w.xixilogic.org/events/2020/08/course-logic-in-ai/) and the foreign-expert projects at ZLAIRE (https://w.zlaire.net/foreignexperts/). at summer schools (from a first tutorial on higher-order modal logics, given with Bruno Woltzenlogel Paleo at the Reasoning Web Summer School and the ANU Logic Summer School in 2015, to the ESSLLI 2026 course Experimenting with the LogiKEy Framework & Methodology in Prague88 8 See https://logikey.org/CoursesAndTutorials/2026-ESSLLI/.), and in numerous invited tutorials and lecture courses over the past decade, among them at the Berkeley--Stanford Circle in Logic and Philosophy, at the CIMI thematic trimester in Toulouse, and in Brazil.99 9 See https://christoph-benzmueller.de/teaching.html for the full record of LogiKEy-based courses and tutorials. Enrolments in such advanced courses are naturally small, and the audience is genuinely mixed: in Bamberg a handful of computer-science and philosophy students, in the earlier Berlin courses also mathematics students, working side by side on the same platform. A semester follows the ladder. The first weeks establish HOL and the proof assistant and settle the propositional warm-up, alongside small exercises (such as a compact HOL proof of Cantor’s theorem Benzmüller and Fuenmayor, 2021) that build fluency with the tool. The middle of the course introduces the embedding technique and works through modal, then epistemic and deontic logics. The final weeks are given to the capstone and to student projects. Prerequisites are deliberately light: a basic acquaintance with propositional and a little modal logic, and no programming experience. This is what makes a genuinely mixed enrolment possible. Each transition is motivated by a limitation exposed in the preceding representation, by a need for more explicit modelling resources, or by a new application: the student moves to a new logic not because the syllabus prescribes it, but because an experiment, or a new question, shows what the old one cannot do. The sequence thus lets students examine different reasons for changing a logic or its formalisation, and each example exposes a different facet of the methodology. Table 1 lays the path out at a glance. It is the actual backbone of the Bamberg course, but we present it as an exemplary path rather than a prescribed curriculum: the steps differ in kind, and an instructor may enter, leave, or branch at any rung. Throughout, the refrain “one meta-logic, many object logics, always machine-checked” becomes a matter of necessity rather than of sightseeing. Table 1: The graded ladder at a glance: for each example, the object logic, the problem that motivates it, the ingredient it adds, and the kind of step it represents: a limitation exposed in the preceding representation, a need for more explicit modelling resources, or a new application. Example Object logic Motivating problem New ingredient Kind of step Rung 1: Liars Street propositional (HOL itself) who lives where?; then: “knows” as a truth-function collapses machine-checked reasoning; the layers L1–L3 first contact Rung 2: modal cube modal K to S5 the extensional collapse possible worlds, accessibility, frame conditions limitation exposed Sequel: Wise Men multi-agent S5 + PAL announcements change what is known announcement as model restriction new modelling resources Interlude: Boolos HOL vs. FOL (meta-level) what does higher-order buy? comprehension as a cut illustrates the meta-logic’s virtues Rung 3: Chisholm SDL (KD), then dyadic DL contrary-to-duty obligations deontic reading; countermodels as pictures; preference relations new application; then limitation exposed Rung 4: Gödel higher-order modal logic necessary existence quantification over properties; frame conditions per theorem extension to a research argument 4.1 Rung 1—A logic puzzle, and its limits The course opens with a puzzle of the “liars and truth-tellers” kind. Two children, Nilda and Carla, each live either in Liars Street (whose inhabitants always lie) or on Truth-tellers’ Road (whose inhabitants always tell the truth); from what they say about one another, the student asks the machine which worlds fit the story. The scenario is encoded directly in HOL, and the first aim is purely experiential: to feel what it is like to reason with a partner that checks every step. The partner answers either “yes, and here is why” (Sledgehammer finds a proof) or “no, and here is a counter-scenario” (Nitpick exhibits a model or a countermodel). The encoding (Fig. 4) is instructive in a second way, too: it is laid out in exactly the LogiKEy layers of Sect. 2.3. The object logic is just HOL’s own propositional connectives (L1); the vocabulary “_ says _” and “_ lives_in _”, together with the two bridge axioms, forms a small domain-specific language (L2); and the concrete question about Nilda and Carla is the application (L3). The puzzle is thus also a first, painless glimpse of the architecture. ⬇ consts says :: "person ⇒ bool ⇒ bool" ("_ says _") (* what an inhabitant asserts *) axiomatization where Liars: "p lives_in Liars ⟹ (p says X) = (¬ )" (* liars invert the truth *) Truth: "p lives_in Road ⟹ (p says X) = X " (* truth-tellers preserve it *) (* Nilda and Carla each vouch that the other tells the truth. Which worlds fit? *) lemma assumes "Nilda says (Carla lives_in Road)" and "Carla says (Nilda lives_in Road)" shows "Nilda lives_in s1 & Carla lives_in s2" nitpick [satisfy] (* Nitpick returns the models consistent with the story *) Figure 4: The warm-up “liars and truth-tellers” puzzle, in outline (the declarations of the types and of lives_in are omitted). Rather than work the knight-and-knave cases by hand, the student has nitpick[satisfy] find the configurations consistent with what Nilda and Carla say: the “answer models”, read off the free variables s1 and s2. Here two survive (both tell the truth, or both lie); enumerating that solution space is exactly the machine’s job. So far, so propositional. The turn comes when we ask what “_ says _” and “_ knows _” actually mean. In the first encoding they are ordinary truth-functions: “X says φ ” is simply a truth value that depends only on the truth value of φ . That suffices for the basic puzzle, but it conceals a trap, and the course springs it deliberately (Fig. 5, upper listing). Because such an operator sees only the truth value of its argument, any two propositions that merely happen to be true become interchangeable inside it: the moment Carla “knows” one truth, the machine proves that she “knows” every other truth as well. This extensional collapse (the crudest member of the family of hyperintensionality problems, of which the well-known logical-omniscience problem is a subtler relative) is not a caveat to be issued in a lecture but a theorem the students derive from their own encoding. The lesson is inescapable: a truth-functional, propositional reading of “says”, “knows”, and “believes” is untenable, and something more expressive is required. ⬇ consts knows :: "person ⇒ bool ⇒ bool" ("_ knows _") (* a plain truth-function *) (* P and Q are both true, and Carla knows P; then she ’knows’ Q as well: *) lemma "[[[\![ P; Q; Carla knows P ]]]\!] ⟹ Carla knows Q" by simp ⬇ typedecl i (* the type of possible worlds *) type_synonym σ = "i ⇒ bool" (* a proposition now depends on worlds *) consts R :: "person ⇒ i ⇒ i ⇒ bool" (* each agent’s accessibility relation *) definition Knows :: "person ⇒ σ ⇒ σ" ("_ knows _") where "a knows p = (%w. ∀ v. R a w v ⟶ p v)" (* box, per agent *) (* the same premises as above, now at a world w: the entailment fails *) lemma "[[[\![ P w; Q w; (Carla knows P) w ]]]\!] ⟹ (Carla knows Q) w" nitpick Figure 5: The extensional collapse, and its modal repair. Above: because “knows” sees only the truth value of its argument, and P and Q are both true, Isabelle proves that knowing P forces knowing Q; any two truths become interchangeable, a reductio the students derive for themselves. Below: a proposition becomes world-dependent, and “knows” becomes a box over the worlds the agent considers possible (frame conditions, such as those of S5, are added afterwards). The collapse is gone: for the very same premises Nitpick now finds a world w at which P and Q both hold and P is known, yet Q is not, because Q fails at some other world Carla considers possible. Logical omniscience proper, knowledge closed under consequence, survives and motivates finer logics. 4.2 Rung 2—Modal logic, and the modal-logic cube The repair is modal logic. A proposition ceases to be a bare truth value and becomes a function from possible worlds to truth values; its type changes from bool to σ (which abbreviates i ⇒ bool, for i the type of possible worlds). “X knows φ ” is then read as “φ holds at every world X considers possible”: the box operator of Sect. 2.2, now indexed by the agent (Fig. 5, lower listing). Two propositions that happen to agree in truth value at the current world need no longer be interchangeable inside a modality, since they may differ at other worlds; the extensional collapse is undone, and Nitpick confirms that the very same entailment now fails. Here modal logic is not introduced, it is needed: the limitation that ended Rung 1 is what motivates the move. Honesty compels a caveat, and the caveat itself makes the pluralist point. The modal reading removes the crude, extensional collapse, but not the finer logical-omniscience problem: according to modal logic S5 a knower still knows every logical consequence of what they know, and every valid formula. Faithfully modelling resource-bounded, non-omniscient agents calls for yet further logics (hyperintensional, awareness-based, or impossible-worlds accounts), each of which the same meta-logical framework can host in turn. Every repair exposes the next question, and none of them forces us to leave the platform: that, in a sentence, is the pedagogical case for logical pluralism. With one modality in hand, the natural next question is which principles it obeys, and here the framework pays a further dividend. Using the embedding of Sect. 2.2, students explore the “modal-logic cube” Benzmüller et al., 2015a: they impose conditions on the accessibility relation one at a time and watch the logic change under their hands. Reflexivity validates □φ→φ → (axiom TT: what is known is true). Seriality validates □φ→◇φ → (axiom DD), and transitivity □φ→□□φ → (axiom 44: positive introspection). Reflexivity together with the Euclidean condition (any two worlds accessible from a given world are accessible from each other) yields S5, a familiar logic of idealised knowledge.1010 10 The systematic verification Benzmüller et al., 2015a labels the TT- and 44-axioms M and IVIV; we use the conventional names. Each correspondence is proved when it holds and refuted by an explicit countermodel when it does not—the same button, opposite verdicts. (The systematic development behind the cube machine-verifies all 15 of its logics and the 25 inclusions among them Benzmüller et al., 2015a.) The refrain is now concrete: the object logic is selected by adding a single line, and the meta-logic never changes. The frame condition behind axiom DD is seriality, which is characteristic of the deontic logic taken up in Rung 3. Even this, the course is careful to add, is not the last word. Reading “says” as a static box still mishandles the dynamics of announcement (what changes when something is publicly said), and nested announcements soon outrun plain modal K. That is the doorway to dynamic epistemic logic, which we take up in the worked example that follows. 4.3 An epistemic sequel: the Wise Men The gap left open by Rung 1 was the dynamics of communication, and the classic vehicle for it is the Wise Men puzzle (equivalently, the “muddy children”). A king marks each of three wise men with a spot on the forehead, white or black—in fact all three white; each sees the others’ spots but not his own. The king announces publicly that at least one spot is white, and then asks, in turn, whether each wise man knows the colour of his own. The first two answer “no”; on hearing them, the third answers “yes”—correctly. The puzzle is a staple precisely because the decisive information is carried not by what is said about the spots but by the announcements themselves: each “I do not know” is a public event that changes what everyone knows. Static modal logic has no direct way to capture this: a fixed accessibility relation cannot represent the update an announcement performs, so each announcement would have to be handled by re-encoding the model by hand. Public-announcement logic (PAL) supplies an operator for exactly this.1111 11 In sheer expressive power PAL without common knowledge adds nothing to static multi-agent epistemic logic, since its reduction axioms eliminate every announcement operator. What it adds is a natural and succinct way of stating updates, and in the classroom that is what counts. On top of multi-agent epistemic logic (one knowledge operator per agent, whose accessible worlds are those the agent cannot tell apart from the actual one), PAL adds an operator [!φ]ψ[! ]ψ, read “after φ is truthfully announced, ψ holds”. Its meaning is simple: after the announcement, only the worlds in which φ was true remain in play. In LogiKEy this is once more a shallow embedding: knowledge is the box of Sect. 2.2, and an announcement restricts all subsequent evaluation to the surviving worlds. Technically this changes the type of a proposition once more: where a modal proposition was a function from worlds to truth values, σ=i⇒σ=i , a dynamic proposition takes one further argument, the set of worlds currently in play, τ=(i⇒)⇒i⇒τ=(i ) i ; it is this extra argument that lets the same formula be evaluated before and after an announcement. The treatment extends to common knowledge, and the embedding has been proven sound in HOL Benzmüller and Reiche, 2023 (Fig. 6). ⬇ type_synonym τ = "(i ⇒ bool) ⇒ i ⇒ bool" (* dynamic proposition: worlds in play, world *) consts K :: "agent ⇒ τ ⇒ τ" ("K_ _") (* K_a p : agent a knows p (S5) *) consts C :: "τ ⇒ τ" (* common knowledge among a, b, c *) consts ann :: "τ ⇒ τ ⇒ τ" ("[!_]_") (* [!phi]psi : after announcing phi, psi *) consts ws :: "agent ⇒ τ" (* ws x : x has a white spot *) axiomatization where WM1: "⌊C⁡(wsa∨wsb∨wsc)⌋ C\ (ws\ a ws\ b ws\ c) " (* at least one white *) (* WM2: if x has no white spot, the other two know it (common knowledge; six axioms) *) theorem "⌊[!¬Ka(wsa)][!¬Kb(wsb)](Kc(wsc))⌋ [! K_a\ (ws\ a)]\ [! K_b\ (ws\ b)]\ (K_c\ (ws\ c)) " Figure 6: Public-announcement logic in LogiKEy, in outline (the encoding of Benzmüller and Reiche, 2023, entered into the Archive of Formal Proofs). The operator K is an S5 box and stands for individual knowledge, while C stands for common knowledge in a group; the announcement [!φ ] restricts the model to the worlds where φ held. The king’s statement is common knowledge (WM1), as is that each wise man sees the others’ spots (WM2). The puzzle is then the single theorem shown: after a announces that he does not know his colour, and b, having heard him, announces the same, c knows that he has a white spot. With the embedding in place, the puzzle becomes a single theorem: given the common knowledge that at least one hat is white, after the first wise man announces that he does not know his colour and the second, having heard him, announces the same, the third knows his spot is white. The automated provers discharge it, and, just as instructive for students, Nitpick can display the intermediate epistemic states, showing how each announcement prunes possibilities until only one survives. The same machinery settles variants (two wise men, black spots, a false announcement) by proof or by countermodel. This closes the loop opened in Rung 1. The single escalation propositional → modal → dynamic epistemic (each step motivated by a demonstrated limitation of the previous logic in modelling “says” and “knows”) is, in miniature, the whole argument of the chapter: many logics, one meta-logic, each one earned rather than presented. Interlude—The virtues of higher-order logic: Boolos’s inference By now a sharp student will be asking what is gained by taking the meta-logic to be higher-order rather than ordinary first-order logic. One example illustrates it memorably, and does so in a domain where one might least expect expressiveness to help: automated proof search Benzmüller et al., 2024b. Boolos’s “curious inference” Boolos, 1987 is a small, valid argument (five axioms in all: three characterising a fast-growing, Ackermann-style function, plus a base case and an induction-like step for a predicate) whose conclusion, that this predicate holds of a particular term, genuinely follows. Three claims should be kept apart here. First, a theorem about proof length: Boolos showed that in a cut-free first-order calculus the shortest derivation has on the order of f⁡(5,5)f(5,5) steps, for f the Ackermann function, so that no such proof could be found, or even written down, in this universe Boolos, 1987. The restriction to cut-free calculi is not an idealisation but the practically relevant case, since the resolution, superposition and tableau calculi on which automated provers are built are analytic. Nor would admitting cuts rescue the first-order case: the cut formula one would need is an instance of second-order comprehension, which quantifies over properties and is therefore not expressible in first-order logic at all. Second, a theorem about expressiveness: Boolos also gave a short proof in second-order logic, using particular instances of the comprehension schema Boolos, 1987. Third, an observation about today’s provers: they are built around cut elimination and do (generally) not introduce the comprehension instances that would be needed. Higher-order provers are not quite in the first-order predicament here, since λ-abstraction together with primitive substitution addresses cut introduction in part, but in general this remains far too weak. Once a single higher-order definition is supplied by hand (the notion of a property being “inductive”, which quantifies over predicates), the provers synthesise the remaining lemmas and dispatch the theorem in milliseconds Benzmüller et al., 2024b. The moral cuts against the grain of what a theoretical-computer-science course tends to instil. Complexity results teach that greater expressiveness must be paid for, with undecidability or higher complexity; yet here the more expressive logic affords an incomparably shorter proof. Expressive power is not merely a luxury; for some problems it is what brings a proof within reach at all. This proof-theoretic bonus is, however, only the most dramatic reason for choosing HOL as the base layer, not the primary one. The primary reason is that higher-order logic is the natural home for the semantical embeddings approach. The λ-abstraction of (1) lifts each connective to a world-dependent function, and quantification over predicates lets one speak directly about properties and accessibility relations. HOL’s mature provers and model finders then serve every embedded logic for free. 4.4 Rung 3—Reasoning about norms: Chisholm’s paradox With one modality in hand, we reinterpret it deontically (□ as “it ought to be that”) and arrive at so-called “standard deontic logic” (SDL), the modal logic KD. The vehicle is Chisholm’s contrary-to-duty paradox Chisholm, 1963, a small set of intuitively consistent obligations that classical SDL formalisations render inconsistent or redundant Gabbay et al., 2013. Two things make this rung pedagogically decisive. First, it shows non-classical logic doing genuine work on a problem philosophers care about. Second, it is where countermodels become pictures: a raw Nitpick countermodel, all but unreadable as text, is rendered automatically as a labelled Kripke graph by a lightweight visualiser developed within LogiKEy Pasetto and Benzmüller, 2025 (Sect. 5). The student does not merely read “not valid”; she gets a visual explanation of why the formula fails. In ordinary language the four sentences are: (1) it ought to be that Jones goes to assist his neighbours; (2) it ought to be that if he goes, he tells them he is coming; (3) if he does not go, he ought not to tell them he is coming; (4) he does not go. The four textbook SDL renderings of these sentences differ only in whether each obligation takes wide (W) or narrow (N) scope over the conditional; we take the four Isabelle/HOL encodings from the LogiKEy Workbench Benzmüller et al., 2020a; Pasetto and Benzmüller, 2025: WN W N NW F1 gOg gOg gOg gOg F2 ⁡(g→t)O(g→ t) ⁡(g→t)O(g→ t) g→tg g→tg F3 ¬g→¬t g t ⁡(¬g→¬t)O( g→ t) ¬g→¬t g t ⁡(¬g→¬t)O( g→ t) F4 ¬g g ¬g g ¬g g ¬g g where g reads “Jones goes to help” and t “Jones tells them he is coming”. None of these renderings captures the intended meaning (each either makes the four sentences jointly inconsistent or makes one a consequence of the others), and students probe them by experiment. One such check asks whether the fact F4F_4 (that Jones does not go) already follows from the three obligations F1F_1–F3F_3: it does not, and Nitpick returns a model in which F1F_1, F2F_2, F3F_3 all hold yet Jones in fact goes. That model, rendered by the LogiKEy visualiser Pasetto and Benzmüller, 2025, is Fig. 7; because g and t hold at every world, each node carries the label “go,tellgo,tell”, and the world marked start is where the conjectured entailment F1∧F2∧F3→F4F_1 F_2 F_3→ F_4 fails. w1w_1w0w_0w2w_2startgo,tellgo,tellgo,tellgo,tellgo,tellgo,tell Figure 7: The Nitpick countermodel of the text, rendered automatically as a labelled Kripke graph by the LogiKEy visualiser Pasetto and Benzmüller, 2025: every world satisfies g and t (“go,tellgo,tell”), the arrows are the deontic accessibility relation, and start marks the world of evaluation. Reading the picture beats reading Nitpick’s raw text—that is the point of the visualiser. The machine’s verdicts diagnose the four renderings precisely: at the designated world, WN is inconsistent; W makes F3F_3 follow from F1F_1; N makes F2F_2 follow from F4F_4; and NW exhibits both redundancies. This systematic failure of SDL on Chisholm’s scenario is, moreover, precisely what motivates the move to more expressive deontic logics. Dyadic deontic logics use a conditional obligation ⁡(t∣g)O(t g), “t is obligatory given g”. In Åqvist’s systems Åqvist, 2002 it is interpreted over a preference (betterness) relation on worlds rather than a mere accessibility relation; in the system of Carmo and Jones Carmo and Jones, 2002, over a semantics designed expressly for contrary-to-duty scenarios. In LogiKEy this upgrade is one further embedding, not a new tool: the LogiKEy Workbench provides ready encodings of both traditions Benzmüller et al., 2019; Benzmüller et al., 2022; Benzmüller et al., 2020a, and the visualiser of Sect. 5 displays preference relations just as it does accessibility relations Pasetto and Benzmüller, 2025. The failed formalisations thus do double duty in class: they diagnose SDL, and they justify its successors. Chisholm’s puzzle is a doorway, not a destination. The same deontic machinery scales to substantial applications in AI and law, and the course points to them. LogiKEy has been used to model value-oriented legal reasoning, where competing legal values are weighed to justify a decision Benzmüller et al., 2024a. Closer to this chapter’s authors, it has served to formalise epistemic rights, such as the “power-right to know” Lawniczak et al., 2025, or mental privacy Pasetto et al., 2026a; Pasetto et al., 2026b, whose formalisation combines the logics used for the right to privacy and freedom of thought. The very contrary-to-duty pattern of Chisholm’s puzzle even recurs in real regulation: one such structure in the GDPR is singled out, in the LogiKEy literature, as instructive “also from an educational viewpoint” Benzmüller et al., 2020b. In the classroom these connect a small paradox to live questions in machine ethics and AI & law, and let a project-minded student move from a textbook example to a fragment of a genuine normative theory. 4.5 Rung 4—Gödel’s ontological argument The capstone lifts everything to higher-order modal logic and applies it to a famous philosophical argument with roots in Leibniz and Anselm: Gödel’s modal ontological proof. The encoding is remarkably compact: a single primitive, “positive property”, and three definitions (God-like, essence, necessary existence) on top of the higher-order modal embedding, followed by five axioms (Fig. 8). ⬇ consts posProp :: "(e ⇒ σ) ⇒ σ" ("P") (* ’P A’: A is positive *) definition God :: "e ⇒ σ" ("G") (* God-like: has every positive property *) where "G x = (∀A.PA→Ax)( ∀A.\ P\ A →A\ x)" (* also Ess (essence), NE (necessary existence), and Scott’s axioms A1..A5 *) Figure 8: The core of Scott’s variant of Gödel’s argument: one primitive (the positive-property operator P) and the definition of God-likeness (the bold ∀,→ ∀, → are the embedded object connectives). From this base—three definitions and five axioms—the provers derive ⌊□∃x.Godx⌋ \, ∃x.\ God\,x , “a God-like being necessarily exists”, while Nitpick confirms the axioms are consistent by exhibiting a model. Encoded this way, the argument becomes an object of experiment. Automated provers reconstruct Scott’s chain of results (positive properties are possibly instantiated, hence a God-like being is possible; being God-like is an essential property; and hence a God-like being necessarily exists), while Nitpick confirms at each stage that the axioms remain consistent by exhibiting a model Benzmüller and Scott, 2025. Turned instead on Gödel’s original axioms, the very same tools expose a hidden inconsistency, from which everything would follow: a discovery first made by the first author’s higher-order prover LEO-I Benzmüller et al., 2015b, and repaired in Scott’s variant Benzmüller and Woltzenlogel Paleo, 2016. The machine refutation even admits a human-readable reconstruction: an “empty essence” lemma from which a contradiction follows in a few steps, an issue that had gone unnoticed before Benzmüller and Woltzenlogel Paleo, 2016. The encoding likewise makes the modal frame conditions explicit per result: the final theorem needs a symmetric accessibility relation, whereas the inconsistency already bites in the base logic K Benzmüller and Scott, 2025. We show only the headers and report the machine’s verdicts; the point is not to grind through a proof but to witness the same platform that ran the hour-one puzzle now adjudicating a twentieth-century metaphysical argument. For students this capstone does real pedagogical work beyond spectacle. It shows that the tools they first met on a logic puzzle are the very ones now used in research; the automated analysis of Gödel’s argument was itself a noted episode of “AI in metaphysics” Benzmüller and Woltzenlogel Paleo, 2016. And it makes vivid that formalisation can clarify a famous argument, exposing assumptions and errors that centuries of informal scrutiny had passed over. That a mixed group of undergraduates can, by the end of a term, replay and interrogate such a result is, in our experience, the course’s most persuasive advertisement for logic itself. Taken as a whole, the ladder is itself the argument for pluralism-in-teaching: one environment, a family of logics of increasing expressiveness, continuous machine checking, and students from different disciplines meeting on one platform. The ladder is, moreover, not a fixed track, and student projects can reach genuine research material, because the same platform carries the teaching examples and the research encodings. A few examples from this line of courses show how far that can go. A project on public-announcement logic grew, by way of a thesis, into the embedding with common knowledge used in Sect. 4.3, published in the Journal of Logic and Computation Benzmüller and Reiche, 2023 and entered into the Archive of Formal Proofs Benzmüller and Reiche, 2021. A project on epistemic rights became the dynamic logic of the “right to know” mentioned in Rung 3 Lawniczak et al., 2025 and an analysis of the logical modalities in the European AI Act Lawniczak and Benzmüller, 2025. Doctoral work at the University of Luxembourg produced the embeddings of dyadic deontic logics Benzmüller et al., 2019; Benzmüller et al., 2022 that form much of the LogiKEy Workbench Benzmüller et al., 2020a on which Rung 3 draws. A mathematics-leaning branch is open as well: one project embedded positive free higher-order logic in HOL Makarenko and Benzmüller, 2020, and another built on such a free logic to develop category theory in Isabelle/HOL with Dana Scott Benzmüller and Scott, 2020; Bayer et al., 2023. The rungs shown here are one instructive path through a much larger space of examples. 5 Tool Support That Lowers the Barrier Several of the tools have already appeared in passing; together they are what makes the approach usable by students who are not, and need not become, specialists in interactive theorem proving. Proof and refutation companions. Sledgehammer Blanchette et al., 2016 and Nitpick Blanchette and Nipkow, 2010 address the beginner’s “blank page” problem from both sides: one looks for a proof, the other for a counterexample (Isabelle’s try command even invokes both at once). A student who does not yet know whether a statement is true can simply ask and, whatever the answer, receive something to inspect and learn from. From countermodel text to a picture. Nitpick reports its (counter-)models as textual assignments (Fig. 9). These are readable enough once one is used to them, but they become inconvenient when large, and they use a function-update notation that newcomers rarely know. The LogiKEy Kripke-model visualiser Pasetto and Benzmüller, 2025 closes this gap: it parses a Nitpick model and emits a labelled graph of worlds, valuations, and accessibility or preference edges, ready for slides or papers. It lets students of law and philosophy see where obligations clash, and it is freely available.1212 12 See https://logikey.org and the tool sources referenced in Pasetto and Benzmüller, 2025. Related infrastructure is emerging in the TPTP world, independent of any one prover: a standard format for interpretations that covers Kripke models Sutcliffe et al., 2024, tools that verify and visualise such interpretations Steen et al., 2023, and finite model finding for first-order modal logics Sariyanto et al., 2026. ⬇ Nitpick found a counterexample for card i = 3: Skolem constant: w = i1 (* the world marked ’start’ *) Constants: go = (%x. _)(i1 := True, i2 := True, i3 := True) tell = (%x. _)(i1 := True, i2 := True, i3 := True) (R) = (%x. _)((i1,i3):=True, (i2,i1):=True, (i3,i3):=True, ...) Figure 9: The raw Nitpick text (abridged) of the very model that Fig. 7 displays: Nitpick’s worlds i1,i2,i3 become w0,w1,w2w_0,w_1,w_2, the Skolem constant w=i1 is the world marked start, the (R) pairs become the arrows, and go/tell (i.e. g and t) hold at every world. What the visualiser adds is legibility: the same content, but readable by a student of law or philosophy. Automated assessment. Because an Isabelle proof either checks or does not, submissions can be graded by machine. In larger deployments this has been realised by coupling Isabelle with the DOMjudge online judge, software originally written for programming contests Wisniewski et al., 2016. A student uploads a proof document, it is checked against the lecturer’s specification, and a verdict is returned within minutes; unsuccessful attempts are retained and annotated inside the verified document. This matters most where hand-marking runs out. In a large course a student might otherwise receive only a single, final comment, whereas the machine’s verdict arrives before submission and can steer the work rather than merely grade it. Even in the small cohorts of our own courses, where grading is done by hand, the same automatic checking sustains a rapid conjecture–attempt–feedback loop during class. Autoformalisation with language models. A more recent aid addresses the hardest step for most students, the passage from an informal statement to a formal one. Large language models now produce serviceable first drafts of a formalisation from a natural-language description, and we already include a small in-class demonstration. What makes this usable rather than hazardous is the setting: a draft is not accepted on trust but handed to the proof assistant, and Sledgehammer and Nitpick report whether it proves what was intended or admits an unintended countermodel. Students must still judge whether the definitions and assumptions capture the intended meaning. The formalise–test–revise loop of Sect. 3 thus absorbs the language model as one more, fallible, participant, and connects the course to current questions about neuro-symbolic AI. The same technology also lets students outsource assignments, a difficulty shared with computer science and mathematics at large. In our setting, this shifts assessment towards students’ own understanding, assessed through discussion: explaining why a formalisation admits a given countermodel, comparing two formalisations of the same text, and defending a modelling choice. At Bamberg this connection is now taught deliberately: the undergraduate logic course Logical Knowledge Representation and Reasoning (AISE-LKR-B) is paired with a course on DevOps for AI systems (AISE-DO-B) that introduces agentic infrastructure and builds bridges between theorem provers, wrapped as agents, and generative AI tools. Together the two courses have become a starting point for ambitious student projects and thesis topics. One honest caveat. Using a general-purpose research proof assistant, rather than a purpose-built teaching applet, buys power and continuity with research practice (students work with the very tools used in current research), at the price of a steeper initial interface. Section 6 weighs this trade-off against the alternatives. 6 Experience, and Related Approaches What we observed. Of the three kinds of claim distinguished in Sect. 3, the classroom observations are the softest. Over the three Bamberg runs a few things stood out. Exploration engaged students across disciplines. Being able to ask the machine (does this hold, and what breaks it?) and to receive an immediate proof or an explicit countermodel turned otherwise abstract questions into something students could probe. The mixed groups often taught one another: the computer-science students were typically quicker with the tool, the philosophy students quicker to see what was at stake in an example. The capstone motivated the climb. Announcing at the outset that the course would end by having the computer scrutinise Gödel’s argument gave the earlier, drier material a visible purpose. The main friction was the tool itself. Isabelle’s syntax, the gap between finding a proof with Sledgehammer and understanding it, and installation across heterogeneous laptops were recurring hurdles, especially for students without a programming background; starting from very small, editable examples was the most effective remedy. Automation reshaped what we could ask. Because the system checks every step, assignments could be genuinely open-ended (“find a model in which…”, “decide whether…and justify your answer formally”) rather than restricted to what is convenient to mark by hand. Students became reviewers. We have discussed research-level, work-in-progress Isabelle theories in class, and more than once a student’s difficulty or question uncovered a genuine issue, leading to a corrected definition or a missing premise being added. Relation to other tool-based approaches. Tool support for teaching logic is by now a lively area with a survey of its own Tran Minh et al., 2025, and this volume itself gathers several complementary tool-based proposals; we leave their comparison to the editors’ introduction and confine ourselves here to a selection of work published elsewhere, with no claim to completeness. Interactive proof assistants are increasingly used in the teaching of mathematics and of program verification: Coq in the Software Foundations series Pierce et al., 2024 and, for many years, in Smolka’s Introduction to Computational Logic at Saarland University Smolka, 2026, Lean in Avigad, Lewis and van Doorn’s Logic and Proof Avigad et al., 2024, and Isabelle in dedicated logic and automated-reasoning courses Villadsen and Jacobsen, 2021. A range of browser-based tutors, such as Carnap Leach-Krouse, 2018 and ProofWeb Hendriks et al., 2010, supports the learning of natural deduction through a gentle, purpose-built interface. Philosophy departments in particular have a long tradition of such software for classical logic, from Barwise and Etchemendy’s Language, Proof and Logic with its Tarski’s World and Fitch programs Barwise and Etchemendy, 1999 and Allen and Hand’s Logic Primer with the Logic Daemon Allen and Hand, 2001 to the Jape proof calculator Bornat and Sufrin, 1999; at the largest scale, Sieg’s Logic & Proofs course at Carnegie Mellon, built on the AProS proof-search engine and its Proof Lab, has taught natural deduction to many thousands of students over two decades Sieg, 2007; Sieg, 2004. Closer to the boundary between informal and formal that our language-model aid addresses (Sect. 5), the Naproche system developed at Bonn checks proofs written in a controlled natural language, and its didactic variant Diproche has been used in introduction-to-proof classes Lon et al., 2021; Carl et al., 2022. ProofBuddy takes a middle road, placing a simplified web front end with restricted syntax in front of Isabelle itself Karsten et al., 2023; Karsten et al., 2025. A further strand gamifies the assistant outright: Buzzard’s Natural Number Game walks students into Lean through a sequence of levels, and a dedicated game server now hosts a growing family of such games Buzzard and Pedramfar, 2021, a format that ties this chapter to the games discussed elsewhere in the present volume. Ontology tools in the style of Protégé introduce logic through applications; even that terrain is not foreign to our course, since the basic description logic ALC is, by Schild’s classic observation Schild, 1991, propositional multimodal logic in another notation. In their semantical embedding this correspondence becomes a one-line exercise, and the soundness of the usual ALC tableau rules a small verification task, as we showed in an earlier tutorial Benzmüller and Woltzenlogel Paleo, 2015; its concepts thus fall out of the modal embedding of Rung 2, a connection we make explicit in the lecture when time permits. LogiKEy’s place in this landscape is characterised by two choices. First, where most such tools fix a single logic or calculus, LogiKEy is semantics-based and logic-pluralistic: many, mostly non-classical, object logics are obtained by embedding their semantics, so that each of them comes with both proof search and countermodel search. Second, it deliberately repurposes a general-purpose research proof assistant, accepting a steeper learning curve in exchange for greater reach: the same environment carries a first logic puzzle and a research-grade metaphysical argument, and it does so for a mixed audience of computer science, mathematics, and philosophy students. The trade-off is better described as an exchange than as a loss: the aim is not to eliminate formal overhead, but to exchange the repeated, ad-hoc formalisation costs of teaching one logic at a time for a single reusable infrastructure. A purpose-built tutor is an excellent first encounter with formal proof, and a LogiKEy-style course is a natural follow-up for students who want to go further. 7 Conclusion and Outlook We have argued that a single expressive meta-logic, hosted in a modern proof assistant, lets a mixed student cohort learn many logics uniformly and experimentally: one meta-logic, many object logics, always machine-checked. We have illustrated the claim with a graded ladder of classroom examples and with the tools that make it workable. It is worth being precise about what the chapter establishes and what it proposes. Established, in the sense of machine-checked and reproducible from the openly available sources, are the formal results of the ladder and the methodological claim that one meta-logic carries all of them. Documented, but only by our own experience, is that a course built this way can be run with a mixed cohort and that students engage with it in the ways described in Sect. 6. Open are the questions a pedagogical study would have to settle: whether the approach improves particular skills, whether it lowers or raises barriers for particular groups, how it compares with purpose-built tutors on a common task, and how learning is best assessed now that large language models can draft formalisations. We regard the chapter as an invitation to such studies, not as a substitute for them. Several directions look promising. Language-model assistance with formalisation (Sect. 5) suggests a future in which students move still more fluently between informal argument and machine-checked proof. Richer interactive and visual tooling, in particular interactive exploration of Kripke models extending the visualiser of Pasetto and Benzmüller, 2025, promises to make non-classical semantics more tangible yet. A further direction concerns portability across proof assistants. Because LogiKEy is defined at the level of a meta-logic rather than of a particular tool Benzmüller, 2019; Benzmüller and Fuenmayor, 2023, the approach is not wedded to Isabelle: any proof assistant whose logic extends higher-order logic can host the same semantical embeddings. We have explored this by porting the ontological-argument material of Rung 4 to the Lean 4 proof assistant Benzmüller, 2026. The translation is structure-preserving, reproducing the same embeddings, definitions, and theorems (down to the inconsistency of Gödel’s original axioms and the individual frame conditions on which each result depends), and the complete Lean sources are available with the preprint. Such portability matters pedagogically: it lets a course meet students on whichever proof assistant their programme already uses. The ceiling, moreover, is high. Recent work carries the embedding technique, with machine-checked faithfulness, to monadic second-order logic Benzmüller and Kirchner, 2026b and even to a deep embedding of HOL within HOL whose soundness, completeness, and consistency are themselves verified Benzmüller and Kirchner, 2026a, so that a graduate course can treat metatheory itself formally. A growing library of openly available, verified developments offers instructors ready-made, machine-checked material at whatever level they teach.1313 13 See the authors’ entries in the Archive of Formal Proofs, https://isa-afp.org/authors/benzmueller/. Finally, the same platform that carries our teaching also carries current research on normative and epistemic reasoning, which points towards a natural extension of the approach to the teaching of AI ethics. All of the course materials are openly available,1414 14 Via https://logikey.org and the associated Isabelle/HOL datasets. in the hope that others may adapt them, in keeping with the mission of the Commission on Logic Education from which this volume grows. Acknowledgements. We are grateful to the LogiKEy contributors mentioned in this chapter and listed at https://logikey.org, and to the students of the courses reported here, whose questions shaped much of the material. The work of Luca Pasetto was supported by the Luxembourg National Research Fund (FNR) through the project Logical methods for Deontic Explanations (INTER/DFG/23/17415164/LODEX). References Allen and Hand (2001) C. Allen and M. Hand Logic primer. 2 edition, MIT Press, Cambridge, MA. Cited by: §6. Åqvist (2002) L. Åqvist Deontic logic. In Handbook of Philosophical Logic, D. M. Gabbay and F. Guenthner (Eds.), Vol. 8, p. 147–264. External Links: Document Cited by: §4.4. Avigad et al. (2024) J. Avigad, R. Y. Lewis, and F. van Doorn Logic and proof. Note: Electronic textbook (Lean) External Links: Link Cited by: §6. Barwise and Etchemendy (1999) J. Barwise and J. Etchemendy Language, proof and logic. CSLI Publications, Stanford. Note: 2nd ed. 2011; with the programs Tarski’s World, Fitch and Boole Cited by: §6. Bayer et al. (2023) J. Bayer, A. Gonus, C. Benzmüller, and D. S. Scott Category theory in Isabelle/HOL as a basis for meta-logical investigation. In Intelligent Computer Mathematics - International Conference, CICM 2023, September 4–8, 2023, Cambridge, UK, Proceedings, C. Dubois and M. Kerber (Eds.), Lecture Notes in Computer Science, Vol. 14101, p. 69–83. External Links: Document Cited by: §4.5. Benzmüller and Andrews (2024) C. Benzmüller and P. Andrews Church’s Type Theory. In The Stanford Encyclopedia of Philosophy, E. N. Zalta and U. Nodelman (Eds.), External Links: Link Cited by: §2.1. Benzmüller et al. (2015a) C. Benzmüller, M. Claus, and N. Sultana Systematic verification of the modal logic cube in Isabelle/HOL. In PxTP 2015, C. Kaliszyk and A. Paskevich (Eds.), Vol. 186, Berlin, Germany, p. 27–41. External Links: Document, ISSN 2075-2180, Link Cited by: §4.2, footnote 10. Benzmüller et al. (2020a) C. Benzmüller, A. Farjami, D. Fuenmayor, P. Meder, X. Parent, A. Steen, L. van der Torre, and V. Zahoransky LogiKEy workbench: deontic logics, logic combinations and expressive ethical and legal reasoning (Isabelle/HOL dataset). Data in Brief (data publication) 33 (106409), p. 1–10. External Links: Link, Document Cited by: §4.4, §4.4, §4.5. Benzmüller et al. (2019) C. Benzmüller, A. Farjami, and X. Parent Åqvist’s dyadic deontic logic E in HOL. Journal of Applied Logics – IfCoLoG Journal of Logics and their Applications (Special Issue: Reasoning for Legal AI) 6 (5), p. 733–755. Cited by: §4.4, §4.5. Benzmüller et al. (2022) C. Benzmüller, A. Farjami, and X. Parent Dyadic deontic logic in HOL: faithful embedding and meta-theoretical experiments. In New Developments in Legal Reasoning and Logic: From Ancient Law to Modern Legal Systems, S. Rahman, M. Armgardt, N. Kvernenes, and H. Christian (Eds.), Logic, Argumentation & Reasoning, Vol. 23, p. 353–377. External Links: Document, Link, ISBN 978-3-030-70083-6, ISSN 2214-9120 Cited by: §4.4, §4.5. Benzmüller et al. (2024a) C. Benzmüller, D. Fuenmayor, and B. Lomfeld Modelling value-oriented legal reasoning in LogiKEy. Logics 2 (1), p. 31–78. External Links: Document Cited by: §1, §4.4, §4. Benzmüller et al. (2024b) C. Benzmüller, D. Fuenmayor, A. Steen, and G. Sutcliffe Who finds the short proof?. Logic Journal of the IGPL 32 (3), p. 442–464. Note: (preprint: arXiv.2208.06879) External Links: Document Cited by: §4, §4. Benzmüller and Fuenmayor (2021) C. Benzmüller and D. Fuenmayor Cantor’s theorem without reductio ad absurdum. Technical report University of Bamberg. External Links: Document, Link Cited by: §4. Benzmüller and Fuenmayor (2023) C. Benzmüller and D. Fuenmayor Mathematical proof assistants for teaching logic: the LogiKEy methodology. In Book of Abstracts — V Congress Tools for Teaching Logic, Madrid, Spain, March 23-24 2023. External Links: Document Cited by: §1, §1, §1, §3, §4, §7. Benzmüller et al. (2026) C. Benzmüller, D. Kirchner, and L. Pasetto Many logics, one methodology: a plea for logical pluralism in formalised reasoning. p. . Note: forthcoming (preprint arXiv:2605.27246) Cited by: §2.4. Benzmüller and Kirchner (2026a) C. Benzmüller and D. Kirchner A deep embedding of HOL in HOL: soundness, completeness, consistency (Isabelle/HOL dataset). Archive of Formal Proofs (data publication), p. 1–96. External Links: Link Cited by: §7. Benzmüller and Kirchner (2026b) C. Benzmüller and D. Kirchner Monadic second-order logic in hol: deep and shallow with automated faithfulness. p. 1–19. Note: forthcoming (extended preprint arXiv:2609.07345) Cited by: §7. Benzmüller et al. (2020b) C. Benzmüller, X. Parent, and L. van der Torre Designing normative theories for ethical and legal reasoning: LogiKEy framework, methodology, and tool support. Artificial Intelligence 287, p. 103348. External Links: ISSN 0004-3702, Document Cited by: §1, §2.3, §4.4, §4, footnote 4. Benzmüller and Paulson (2008) C. Benzmüller and L. C. Paulson Exploring properties of normal multimodal logics in simple type theory with LEO-I. In Reasoning in Simple Type Theory — Festschrift in Honor of Peter B. Andrews on His 70th Birthday, C. Benzmüller, C. Brown, J. Siekmann, and R. Statman (Eds.), Studies in Logic, Mathematical Logic and Foundations, p. 386–406. Note: (Superseded by 2013 paper in Logica Universalis) External Links: ISBN 978-1-904987-70-3, Link Cited by: §2.4. Benzmüller and Paulson (2013) C. Benzmüller and L. C. Paulson Quantified multimodal logics in simple type theory. Logica Universalis (Special Issue on Multimodal Logics) 7 (1), p. 7–20. External Links: Document Cited by: §2.4. Benzmüller and Reiche (2021) C. Benzmüller and S. Reiche Automating public announcement logic and the wise men puzzle in Isabelle/HOL. Archive of Formal Proofs (data publication), p. 1–5. External Links: Link Cited by: §4.5. Benzmüller and Reiche (2023) C. Benzmüller and S. Reiche Automating public announcement logic with relativized common knowledge as a fragment of HOL in LogiKEy. Journal of Logic and Computation 33 (6), p. 1243–1269. External Links: Document Cited by: Figure 6, §4.3, §4.5. Benzmüller and Scott (2020) C. Benzmüller and D. S. Scott Automating free logic in HOL, with an experimental application in category theory. Journal of Automated Reasoning 64 (1), p. 53–72. External Links: Document, Link Cited by: §4.5. Benzmüller and Scott (2025) C. Benzmüller and D. S. Scott Notes on Gödel’s and Scott’s variants of the ontological argument. Monatshefte für Mathematik 208, p. 569–611. External Links: Document Cited by: §2.4, §4.5. Benzmüller et al. (2015b) C. Benzmüller, N. Sultana, L. C. Paulson, and F. Theiss The higher-order prover LEO-I. Journal of Automated Reasoning 55 (4), p. 389–404. External Links: Document Cited by: §4.5. Benzmüller et al. (2015c) C. Benzmüller, M. Wisniewski, and A. Steen Computational Metaphysics. Technical report Freie Universität Berlin. Note: This lecture course proposal received the 2015 central teaching award of FU Berlin External Links: Link, Document Cited by: §4. Benzmüller and Woltzenlogel Paleo (2015) C. Benzmüller and B. Woltzenlogel Paleo Higher-order modal logics: automation and applications. In Reasoning Web 2015, A. Paschke and W. Faber (Eds.), LNCS, Berlin, Germany, p. 32–74. Note: (Invited paper) External Links: Document Cited by: §6. Benzmüller and Woltzenlogel Paleo (2016) C. Benzmüller and B. Woltzenlogel Paleo The inconsistency in Gödel’s ontological argument: a success story for AI in metaphysics. In IJCAI 2016, S. Kambhampati (Ed.), Vol. 1-3, p. 936–942. External Links: ISBN 978-1-57735-770-4 Cited by: §4.5, §4.5. Benzmüller (2019) C. Benzmüller Universal (meta-)logical reasoning: recent successes. Science of Computer Programming 172, p. 48–62. External Links: Link, Document Cited by: §1, §2.1, §2.2, §2.4, §7. Benzmüller (2025) C. Benzmüller Faithful logic embeddings in HOL — deep and shallow. In Automated Deduction – CADE-30 – 30th International Conference on Automated Deduction, Stuttgart, Germany, July 28-31, 2025, Proceedings, C. Barrett and U. Waldmann (Eds.), Lecture Notes in Computer Science, Vol. 15943, p. 280–302. Note: (preprint: arXiv:2502.19311) External Links: Document, Link Cited by: Figure 3, §2.2, §2.4. Benzmüller (2026) C. Benzmüller Gödel’s and Scott’s variants of the ontological argument in Lean 4 and TPTP THF. Note: arXiv:2609.26806 External Links: Document Cited by: §7. Blanchette et al. (2016) J. C. Blanchette, C. Kaliszyk, L. C. Paulson, and J. Urban Hammering towards QED. Journal of Formalized Reasoning 9 (1), p. 101–148. External Links: Document Cited by: §2.3, §5. Blanchette and Nipkow (2010) J. C. Blanchette and T. Nipkow Nitpick: a counterexample generator for higher-order logic based on a relational model finder. In Interactive Theorem Proving (ITP 2010), M. Kaufmann and L. C. Paulson (Eds.), Lecture Notes in Computer Science, Vol. 6172, p. 131–146. External Links: Document Cited by: §2.3, §5. Boolos (1987) G. Boolos A curious inference. Journal of Philosophical Logic 16 (1), p. 1–12. External Links: Document Cited by: §4. Bornat and Sufrin (1999) R. Bornat and B. Sufrin Animating formal proof at the surface: the Jape proof calculator. The Computer Journal 42 (3), p. 177–192. External Links: Document Cited by: §6. Buzzard and Pedramfar (2021) K. Buzzard and M. Pedramfar The natural number game. Note: Interactive Lean tutorial, hosted on the Lean game server, https://adam.math.hhu.de/ Cited by: §6. Carl et al. (2022) M. Carl, H. Lorenzen, and M. Schmitz Natural language proof checking in introduction to proof classes – first experiences with Diproche. In Proceedings of the 10th International Workshop on Theorem Proving Components for Educational Software (ThEdu’21), EPTCS, Vol. 354, p. 59–70. External Links: Document Cited by: §6. Carmo and Jones (2002) J. Carmo and A. J. I. Jones Deontic logic and contrary-to-duties. In Handbook of Philosophical Logic, D. M. Gabbay and F. Guenthner (Eds.), Vol. 8, p. 265–343. External Links: Document Cited by: §4.4. Chisholm (1963) R. M. Chisholm Contrary-to-duty imperatives and deontic logic. Analysis 24 (2), p. 33–36. External Links: Document Cited by: §4.4. Fuenmayor and Benzmüller (2017) D. Fuenmayor and C. Benzmüller Automating emendations of the ontological argument in intensional higher-order modal logic. In KI 2017: Advances in Artificial Intelligence, 40th Annual German Conference on AI, Dortmund, Germany, September 25-29, 2017, Proceedings, LNAI, Vol. 10505, p. 114–127. External Links: ISBN 978-3-319-67189-5, Document, Link Cited by: §2.4, §4. Fuenmayor and Benzmüller (2018) D. Fuenmayor and C. Benzmüller A case study on computational hermeneutics: E. J. Lowe’s modal ontological argument. Journal of Applied Logic - IfCoLoG Journal of Logics and their Applications (special issue on Formal Approaches to the Ontological Argument) 5 (7), p. 1567–1603. Note: Published also as chapter in the book ’Beyond Faith and Rationality: Essays on Logic, Religion and Philosophy’ printed in the Springer book series ’Sophia Studies in Cross-cultural Philosophy of Traditions and Cultures’ Cited by: §4. Fuenmayor and Benzmüller (2019) D. Fuenmayor and C. Benzmüller A computational-hermeneutic approach for conceptual explicitation. In Model-Based Reasoning in Science and Technology. Inferential Models for Logic, Language, Cognition and Computation, A. Nepomuceno, L. Magnani, F. Salguero, C. Bares, and M. Fontaine (Eds.), SAPERE, Vol. 49, p. 441–469. External Links: Document, Link Cited by: §3, §4. Fuenmayor and Benzmüller (2020) D. Fuenmayor and C. Benzmüller Normative reasoning with expressive logic combinations. In ECAI 2020 – 24th European Conference on Artificial Intelligence, June 8-12, Santiago de Compostela, Spain, G. De Giacomo, A. Catala, B. Dilkina, M. Milano, S. Barro, A. Bugarín, and J. Lang (Eds.), Frontiers in Artificial Intelligence and Applications, Vol. 325, p. 2903–2904. External Links: Document Cited by: §4. Fuenmayor (2018) D. Fuenmayor Computational hermeneutics: using computers to understand philosophical arguments. Bachelor’s thesis, Institut für Philosophie, Freie Universität Berlin. Note: Winter term 2017/18 Cited by: §4. Fuenmayor (2025) D. Fuenmayor A universal mathematical language for argumentative reasoning agents. Ph.D. Thesis, Fachbereich Mathematik und Informatik, Freie Universität Berlin. Cited by: §4. D. Gabbay, J. Horty, X. Parent, R. van der Meyden, and L. van der Torre (Eds.) (2013) D. Gabbay, J. Horty, X. Parent, R. van der Meyden, and L. van der Torre (Eds.) Handbook of deontic logic and normative systems, volume 1. College Publications, London. Cited by: §4.4. Hendriks et al. (2010) M. Hendriks, C. Kaliszyk, F. van Raamsdonk, and F. Wiedijk Teaching logic using a state-of-the-art proof assistant. Acta Didactica Napocensia 3 (2), p. 35–48. Cited by: §6. Karsten et al. (2025) N. Karsten, K. J. Eiken, and U. Nestmann ProofBuddy: how it started, how it’s going. In Proceedings of the 13th International Workshop on Theorem Proving Components for Educational Software (ThEdu’24), EPTCS, Vol. 419, p. 90–111. External Links: Document Cited by: §6. Karsten et al. (2023) N. Karsten, F. K. Jacobsen, K. J. Eiken, U. Nestmann, and J. Villadsen ProofBuddy: a proof assistant for learning and monitoring. In Proceedings of the 12th International Workshop on Theorem Proving Components for Educational Software (ThEdu’23), EPTCS, Vol. 382, p. 1–21. External Links: Document Cited by: §6. Kirchner et al. (2020) D. Kirchner, C. Benzmüller, and E. N. Zalta Mechanizing principia logico-metaphysica in functional type theory. Review of Symbolic Logic 13 (1), p. 206–218. External Links: Document Cited by: §2.4, §4. Kirchner (2017) D. Kirchner Representation and partial automation of the Principia Logico-Metaphysica in Isabelle/HOL. Master’s thesis, Institut für Mathematik, Freie Universität Berlin. Cited by: §4. Kirchner (2022) D. Kirchner Computer-verified foundations of metaphysics and an ontology of natural numbers in Isabelle/HOL. Ph.D. Thesis, Freie Universität Berlin. External Links: Document Cited by: §4. Lawniczak and Benzmüller (2025) L. Lawniczak and C. Benzmüller Logical modalities within the european ai act: an analysis. In ICAIL ’25: Proceedings of the Twentieth International Conference on Artificial Intelligence and Law, J. Maranhão (Ed.), p. 348–353. Note: (preprint: arXiv:2501.19112) External Links: Document Cited by: §4.5. Lawniczak et al. (2025) L. Lawniczak, L. Pasetto, C. Benzmüller, X. Li, and R. Markovich Reasoning with epistemic rights and duties: automating a dynamic logic of the right to know in logikey. In ECAI 2025 - 28th European Conference on Artificial Intelligence, I. Lynce, N. Murano, M. Vallati, S. Villata, F. Chesani, M. Milano, A. Omicini, and M. Dastani (Eds.), Vol. 413, p. 1623–1630. External Links: Document, Link Cited by: §4.4, §4.5. Leach-Krouse (2018) G. Leach-Krouse Carnap: an open framework for formal reasoning in the browser. In Proceedings of the 6th International Workshop on Theorem Proving Components for Educational Software (ThEdu 2017), EPTCS, Vol. 267, p. 70–88. External Links: Document Cited by: §6. Lon et al. (2021) A. D. Lon, P. Koepke, A. Lorenzen, A. Marti, M. Schütz, and M. Wenzel The Isabelle/Naproche natural language proof assistant. In Automated Deduction – CADE 28, LNCS, p. 614–624. External Links: Document Cited by: §6. Makarenko and Benzmüller (2020) I. Makarenko and C. Benzmüller Positive free higher-order logic and its automation via a semantical embedding. In KI 2020: Advances in Artificial Intelligence – 43rd German Conference on Artificial Intelligence, Bamberg, Germany, September 21–25, 2020, Proceedings, U. Schmid, F. Klügl, and D. Wolter (Eds.), Lecture Notes in Artificial Intelligence, Vol. 12352, p. 116–131. Note: EasyChair Preprint no. 3621, EasyChair External Links: Link, Document, ISBN 978-3-030-58284-5 Cited by: §4.5. Nipkow et al. (2002) T. Nipkow, L. C. Paulson, and M. Wenzel Isabelle/hol: a proof assistant for higher-order logic. Lecture Notes in Computer Science, Vol. 2283, Springer. External Links: Document Cited by: §2.3. Pasetto et al. (2026a) L. Pasetto, C. Benzmüller, and R. Markovich Formalizing mental privacy in logikey. In Proceedings of the 25th International Conference on Autonomous Agents and Multiagent Systems (AAMAS 2026), May 25 – 29, 2026, Paphos, Cyprus, C. Amato, L. Dennis, V. Mascardi, and J. Thangarajah (Eds.), , p. 3643–3645. External Links: Document Cited by: §4.4. Pasetto et al. (2026b) L. Pasetto, C. Benzmüller, and R. Markovich Right on thought, left private: reasoning about mental privacy in logikey. In Proceedings of the 10th International Joint Conference on Rules and Reasoning (RuleML+R 2026), D. Lanti and A. Paschke (Eds.), LNCS. Cited by: §4.4. Pasetto and Benzmüller (2025) L. Pasetto and C. Benzmüller Visualizing kripke models in logikey: the case of sdl. In Joint Proceedings of the Workshops and Doctoral Consortium of the 41st International Conference on Logic Programming, September 9–13, 2025, Rende, Italy, D. Azzolini, S. Batsakis, M. A. B. Santana, P. Bruno, L. A. Cecchi, J. Fandinno, M. Hecher, M. Maratea, J. F. Morales, B. Muñiz, E. Papadakis, L. Robaldo, L. Serafini, F. Lo Scudo, I. Tachmazidis, A. Tarzariol, M. Vallati, and A. Wyner (Eds.), Vol. 4117, p. 1–9. External Links: Link Cited by: Figure 7, §2.3, §4.4, §4.4, §4.4, §4.4, §5, §7, footnote 12. Pierce et al. (2024) B. C. Pierce, A. A. de Amorim, C. Casinghino, M. Gaboardi, M. Greenberg, C. Hriţcu, V. Sjöberg, and B. Yorgey Software foundations. Note: Electronic textbook (Coq) External Links: Link Cited by: §6. Sariyanto et al. (2026) H. K. Sariyanto, A. Steen, and G. Sutcliffe Finite model finding in first-order modal logics. In Automated Reasoning – 13th International Joint Conference, IJCAR 2026, A. Biere, C. Lutz, and S. Negri (Eds.), LNCS, p. 317–335. External Links: Document Cited by: §5. Schild (1991) K. Schild A correspondence theory for terminological logics: preliminary report. In Proceedings of the 12th International Joint Conference on Artificial Intelligence (IJCAI-91), p. 466–471. Cited by: §6. Sieg (2004) W. Sieg Logic & proofs. Note: Online course, Open Learning Initiative, Carnegie Mellon University, taught since 2004, https://oli.cmu.edu/courses/logic-proofs/ Cited by: §6. Sieg (2007) W. Sieg The AProS project: strategic thinking & computational logic. Logic Journal of the IGPL 15 (4), p. 359–368. External Links: Document Cited by: §6. Smolka (2026) G. Smolka Modeling and proving in computational type theory using the Rocq prover. Note: Textbook draft accompanying the course Introduction to Computational Logic, Saarland University, https://w.ps.uni-saarland.de/~smolka/drafts/mpctt.pdf Cited by: §6. Steen et al. (2023) A. Steen, G. Sutcliffe, P. Fontaine, and J. McKeown Representation, verification, and visualization of Tarskian interpretations for typed first-order logic. In LPAR 2023: 24th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, EPiC Series in Computing, Vol. 94, p. 351–369. External Links: Document Cited by: §5. Sutcliffe et al. (2024) G. Sutcliffe, A. Steen, P. Fontaine, and L. Kondylidou The TPTP format for interpretations. Note: arXiv:2406.06108 Cited by: §5. Tran Minh et al. (2025) F. Tran Minh, L. Gonnord, and J. Narboux Proof assistants for teaching: a survey. Note: PreprintarXiv:2505.13472 External Links: Document Cited by: §6. Villadsen and Jacobsen (2021) J. Villadsen and F. K. Jacobsen Using isabelle in two courses on logic and automated reasoning. In Formal Methods Teaching (FMTea 2021), Lecture Notes in Computer Science, Vol. 13122, p. 117–132. External Links: Document Cited by: §6. Wisniewski et al. (2016) M. Wisniewski, A. Steen, and C. Benzmüller Einsatz von Theorembeweisern in der Lehre. In Hochschuldidaktik der Informatik: 7. Fachtagung des GI-Fachbereichs Informatik und Ausbildung/Didaktik der Informatik; 13.-14. September 2016 an der Universität Potsdam, A. Schwill and U. Lucke (Eds.), Commentarii informaticae didacticae (CID), Potsdam, Germany, p. 81–92. External Links: ISBN 978-3-86956-376-3, ISSN 1868-0844, Link Cited by: §1, §3, §3, §4, §5.

Instant research discovery