The LogiKEy methodology: applications, domain-specific languages and object logics are embedded in classical higher-order logic (HOL)

The LogiKEy methodology (figure: Benzmüller et al., Artificial Intelligence 2020)

LogiKEy Course at ESSLLI 2026 in Prague

Christoph Benzmüller and Luca Pasetto (University of Luxembourg) taught the course “Experimenting with the LogiKEy Framework & Methodology” at the 37th European Summer School in Logic, Language and Information (ESSLLI 2026). All course materials are freely available.

From 10 to 14 August 2026, the 37th European Summer School in Logic, Language and Information (ESSLLI 2026) took place at Charles University in Prague. Christoph Benzmüller and Luca Pasetto (University of Luxembourg) offered the one-week introductory course “Experimenting with the LogiKEy Framework & Methodology” in the Logic and Computation track.

The course introduced the LogiKEy methodology – the semantical embedding of object logics in classical higher-order logic (HOL) – and hands-on work with the proof assistant Isabelle/HOL. Applications were demonstrated in three areas: normative reasoning (deontic logics), knowledge representation (agents, actions, rights) and computational metaphysics (Gödel’s ontological argument).

All course materials (slides and Isabelle/HOL source files) are freely available at logikey.org/CoursesAndTutorials/2026-ESSLLI. Further information on the summer school: 2026.esslli.eu.