3 papers
cs.LO2026
Monadic Second-Order Logic in HOL: Deep and Shallow with Automated Faithfulness (Extended Preprint)
Christoph Benzmueller, Daniel Kirchner
In Isabelle/HOL, we apply the deep-and-shallow embedding methodology of our prior work to monadic second-order logic (MSO). Three embeddings are developed side by side: a deep embe…
cs.AI2026
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.…
cs.LO2026
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…