Email Gateway (Jun 04 2025 at 14:11): Email Gateway (Jun 04 2025 at 14:11):From: Lawrence Paulson <lp15@cam.ac.uk>
I'm happy to announce yet another contribution (from our sadly considerable backlog):
Faithful Logic Embeddings in HOL — Deep and Shallow
by Christoph Benzmüller
A recipe for the simultaneous deployment of different forms of deep and shallow embeddings of non-classical logics in classical higher-order logic is presented, which enables interactive or even automated faithfulness proofs between the logic embeddings. The approach, which is particularly fruitful for logic education, is explained in detail in an associated CADE conference paper. This paper presents the corresponding Isabelle/HOL dataset (which is only slightly modified to meet AFP requirements).
https://www.isa-afp.org/entries/FaithfulPMLinHOL.html
Larry Paulson
Last updated: Jun 20 2025 at 12:44 UTC