First-Order Modal Logic in HOL : Deep and Shallow Embeddings with Automated Faithfulness (Extended Preprint)

Benzmüller, ChristophChristophBenzmüller0000-0002-3392-3093Kirchner, DanielDanielKirchner0000-0001-9229-11482026-09-102026-09-102026https://fis.uni-bamberg.de/handle/uniba/117136engFirst-Order Modal Logic in HOL : Deep and Shallow Embeddings with Automated Faithfulness (Extended Preprint)preprint10.48550/arxiv.2607.108802607.10880