40 citations · 211 across the 45 of their papers we have counts for
21 papers · 1 filter
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…
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…
Automated Reasoning in Non-classical Logics in the TPTP World
Alexander Steen, David Fuenmayor, Tobias Gleißner +2
Non-classical logics are used in a wide spectrum of disciplines, including artificial intelligence, computer science, mathematics, and philosophy. The de-facto standard infrastruct…
Automating Public Announcement Logic with Relativized Common Knowledge as a Fragment of HOL in LogiKEy
Christoph Benzmüller, Sebastian Reiche
A shallow semantical embedding for public announcement logic with relativized common knowledge is presented. This embedding enables the first-time automation of this logic with off…
Public Announcement Logic in HOL
Sebastian Reiche, Christoph Benzmüller
A shallow semantical embedding for public announcement logic with relativized common knowledge is presented. This embedding enables the first-time automation of this logic with off…