40 citations · 211 across the 45 of their papers we have counts for
51 papers
Mathematical Proof Assistants for Teaching Logic: The LogiKEy Methodology
Christoph Benzmüller, David Fuenmayor, Luca Pasetto
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…
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…
A Comment on Modal Collapse and Ultrafilters in Gödel's Ontological Argument
Christoph Benzmüller
Gödel's ontological argument is modal by design. Possibility and necessity are among its central concerns, and connected interpretation decisions -- extensions or intensions for th…
First-Order Modal Logic in HOL: Deep and Shallow Embeddings with Automated Faithfulness (Extended Preprint)
Christoph Benzmüller, Daniel Kirchner
We extend, in Isabelle/HOL, the deep-and-shallow embedding methodology of our prior work from propositional to first-order modal logic (FML) with constant-domain Kripke semantics.…
Neuro-Symbolic Verification of LLM Outputs for Data-Sensitive Domains (extended preprint)
Paul Sigloch, Christoph Benzmüller
LLMs deployed in high-stakes domains face fundamental reliability challenges: hallucinations, inconsistencies, and privacy vulnerabilities introduce unacceptable risks where errors…