TY  - RPRT
TI  - First-Order Modal Logic in HOL: Deep and Shallow Embeddings with Automated Faithfulness (Extended Preprint)
AU  - Christoph Benzmüller
AU  - Daniel Kirchner
PY  - 2026
UR  - https://arxiv.org/abs/2607.10880
ID  - 2607.10880
ER  -