arXiv cs.AI· Christoph Benzm\"uller, David Fuenmayor, Luca Pasetto·· 10 天前AI 评分17
LogiKEy 方法论：用数学证明助手教逻辑学
Mathematical Proof Assistants for Teaching Logic: The LogiKEy Methodology
AI 导读
LogiKEy 方法论以经典高阶逻辑（HOL）作为通用元逻辑，将经典与非经典对象逻辑通过语义嵌入编码，使 Isabelle/HOL 等单一证明助手成为学生学习、实验和比较多种逻辑的统一环境。该方法已用于课程、暑期学校和教程超过十年，文章给出从命题逻辑、模态逻辑、动态认知逻辑到道义逻辑和 Gödel 本体论论证的递进式课堂示例，并回应了"将一切嵌入经典 HOL 是多元论还是一元论"的质疑。
正文 · AI 翻译
摘要：我们报告一种面向计算机科学、数学和哲学混合学生群体教授逻辑学的方法，其基础是逻辑多元主义的 LogiKEy 方法论，该方法已在课程、暑期学校和教程中使用十余年。LogiKEy 使用经典高阶逻辑（HOL）作为通用元逻辑，在其中通过定义语义来编码对象逻辑，无论是经典的还是非经典的；通过这些语义嵌入，单个证明助手（例如 Isabelle/HOL）及其自动定理证明器和（反）模型查找器，成为一个学生可以学习、实验和比较各种逻辑的环境。在论证了证明助手在逻辑课堂中的教学价值之后，我们呈现了一系列循序渐进的课堂示例，每一次过渡都源于前一表示的局限、对更显式建模资源的需求，或一个新的应用。一个说谎者与说真话者谜题将命题逻辑引向模态逻辑；智者谜题进一步引向动态认知逻辑；Boolos 的奇特推理说明了高阶元逻辑能带来什么，即使对于自动证明搜索也是如此；Chisholm 悖论将这一序列带入道义逻辑，并从标准道义逻辑走向二元道义逻辑；而 Gödel 的本体论论证则将其提升到研究级别的形而上学论证。随后，我们反驳了将所有内容嵌入经典 HOL 是一元论而非多元论的反对意见，反思了三年教授此类课程的经验，并概述了该方法在 Isabelle 之外的可移植性。
| 主题： | 人工智能（cs.AI）；计算机科学中的逻辑（cs.LO） |
| 引用为： | arXiv:2610.08214 [cs.AI] |
| （或 arXiv:2610.08214v1 [cs.AI] 用于此版本） | |
| https://doi.org/10.48550/arXiv.2610.08214 arXiv 颁发的 DOI 通过 DataCite（待注册） |
提交历史
来自：David Fuenmayor [查看电子邮件]
[v1]
2026年10月6日星期二 12:07:39 UTC（120 KB）
来源：arXiv cs.AI · arxiv.org