40 citations · 211 across the 45 of their papers we have counts for
26 papers · 1 filter
Proofs Without Nominals: Gödel's Ontological Argument, its Shallow Embedding, and the Open Questions of the Monatshefte Notes
Christoph Benzmüller
The shallow embedding of higher-order modal logic in classical higher-order logic, used in Benzmüller and Scott's Notes on Gödel's and Scott's variants of the ontological argument,…
Gödel's and Scott's Variants of the Ontological Argument in Lean 4 and TPTP THF
Christoph Benzmüller
The Isabelle/HOL dataset of Benzmüller and Scott's study of Gödel's ontological argument and Scott's variant (Monatshefte für Mathematik, 2025) is carried to Lean 4 and from there…
Many Logics, One Methodology: A Plea for Logical Pluralism in Formalised Reasoning (preprint)
Christoph Benzmüller, Daniel Kirchner, Luca Pasetto
This position statement looks back on two decades of work on shallow embeddings of non-classical logics in classical higher-order logic (HOL), a line of research that expanded into…
Faithful Logic Embeddings in HOL -- Deep and Shallow
Christoph Benzmüller
Deep and shallow embeddings of non-classical logics in classical higher-order logic have been explored, implemented, and used in various reasoning tools in recent years. This paper…
Normative Conditional Reasoning as a Fragment of HOL
Xavier Parent, Christoph Benzmüller
We report on the mechanization of (preference-based) conditional normative reasoning. Our focus is on Aqvist's system E for conditional obligation, and its extensions. Our mechaniz…
Category Theory in Isabelle/HOL as a Basis for Meta-logical Investigation
Jonas Bayer, Aleksey Gonus, Christoph Benzmüller +1
This paper presents meta-logical investigations based on category theory using the proof assistant Isabelle/HOL. We demonstrate the potential of a free logic based shallow semantic…