Faithful Logic Embeddings in HOL -- A recipe to have it all: deep and shallow, automated and interactive, heavy and light, proofs and counterexamples, meta and object level
作者: Christoph Benzmüller
发布时间: 2025-02-27
来源: arxiv
研究方向: 逻辑嵌入与自动推理
主要内容
本文研究了在经典高阶逻辑（HOL）中实现不同形式的深层次和浅层次逻辑嵌入，并展示了如何通过这些嵌入实现灵活的交互式和自动化定理证明、反例查找，以及元层次和对象层次上的忠实性证明。
主要贡献
1. 提出了一种将深层次和浅层次逻辑嵌入在HOL中链接起来的技术，使得在这些嵌入之间进行忠实性证明成为可能。
2. 讨论了不同形式的浅层次嵌入，这些嵌入在显式编码和维持的语义依赖程度上有所不同。
3. 探讨了逻辑教育以及使用现代证明辅助工具和定理证明器进行逻辑嵌入研究和应用的不同可能性。
4. 通过简单的命题模态逻辑（PML）示例说明了所提出的技术。
5. 提出了最小浅层次嵌入可能比最大或深层次嵌入更适合某些推理任务的假设，并提供了证据。
6. 使用可证明性逻辑的Löb公理，简要说明了如何使用所提出的技术支持语义对应关系的检测研究。
研究方法
1. 高阶逻辑（HOL）
2. 逻辑嵌入
3. 忠实性证明
4. 自动化推理
5. 反例查找
6. 交互式证明
7. 模型查找
8. sledgehammer工具
9. nitpick工具
实验结果
实验结果表明，最小浅层次嵌入在证明自动化和反例查找方面表现最佳。
未来工作
未来工作可能包括开发无限模型查找工具、将浅层次嵌入与更复杂的逻辑相结合、以及为用户提供直观的反例图。