同时支持深嵌入与浅嵌入，实现逻辑推理与验证的灵活统一
Faithful Logic Embeddings in HOL -- Deep and Shallow
- 在经典高阶逻辑中融合深嵌入与浅嵌入方法
- 可自动证明嵌入间的保真性并支持元层与对象层推理
- 适合逻辑教学、研究及形式化工具开发
近年来，非经典逻辑在经典高阶逻辑中的深嵌入与浅嵌入已被广泛探索、实现并应用于各类推理工具。本文提出一种在经典高阶逻辑中同时部署不同层次深嵌入与浅嵌入的方法，实现了元层与对象层的交互式与自动化定理证明、反例生成，以及这些逻辑嵌入间保真性的自动证明。该方法概念性强，虽以简单的命题模态逻辑为例说明，但不局限于特定逻辑体系，对逻辑教育、研究与应用均有裨益。
原文摘要 · Abstract (English)
Deep and shallow embeddings of non-classical logics in classical higher-order logic have been explored, implemented, and used in various reasoning tools in recent years. This paper presents a method for the simultaneous deployment of deep and shallow embeddings of various degrees in classical higher-order logic. This enables flexible, interactive and automated theorem proving and counterexample finding at meta and object level, as well as automated faithfulness proofs between these logic embeddings. The method is beneficial for logic education, research and application and is illustrated here using a simple propositional modal logic. However, this approach is conceptual in nature and not limited to this simple logic context.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。