QED
QED (Quite Easy Deduction) 是一个用 MoonBit 编写的高阶逻辑定理证明器。它遵循 LCF 方法：一个小型可信内核实现 HOL 的原始推理规则，并且是唯一能创建定理的代码；其余一切，从解析器 (parser) 到命令行工具，都构建在它之上而无需被信任。证明写成带面向目标步骤的简短定理脚本；脚本要么产生内核定理，要么以结构化诊断失败，要么报告未完成证明。一份形式化规范定义了内核，formal_verification/ 中的 Lean 4 包检查该规范的符合性声明。
已发布的证明语言涵盖带等词的命题逻辑、定理头部绑定子和目标级 forall；确切的支持矩阵见用户手册。
形式规范
形式规范是内核唯一的规范性来源。
包
这些包是分层的：每个包只依赖其左侧的包，即 kernel → logic/elab → parser → tactics → prover → cmd，且只有 kernel 受信任。
| 包 | 职责 | 页面 |
|---|---|---|
kernel | 可信内核：类型、项、抽象定理类型、原始规则、带作用域的签名、扩展闸门 | API · 设计 · 教程 |
logic | 作为定义的命题联结词、派生规则、重放辅助函数、定理目录 | API · 设计 · 教程 |
elab | 带冻结常量标识的名称解析、核心类型检查、降级 (lowering) 为内核项 | API · 设计 · 教程 |
parser | 文本前端：规范化、项、目标、定理脚本、源码位置 | API · 设计 · 教程 |
tactics | 反向证明状态与步骤，向前重放为内核定理 | API · 设计 · 教程 |
prover | 带结构化结果的定理脚本驱动器，以及回归语料 (corpus) | API · 设计 · 教程 |
cmd | 命令行工具 qed-cmd（可执行包） | API · 设计 · 教程 |
research_rewrite | 仅用于研究的重写原型，不随发行版提供 | API · 设计 · 教程 |
黑盒测试文件（*_test.mbt）以及别名文件 alias.mbt 和 alias_test.mbt 属于各自的包；其规则由代码治理定义。examples/ 和 prelude/ 中的定理文件是命令行工具的输入，不是包。
从哪里开始
初次接触证明助手。 阅读用户手册中的“面向 HOL 新读者”和快速入门，然后借助 cmd 教程运行示例。语法指南回答“这一步该怎么写”。
在 MoonBit 中使用 QED。 先读 prover 教程，学习运行脚本并读取结果。再深入 tactics 教程，逐步驱动证明；并通过 logic 和 kernel 教程向前构造定理。
检查它为何可靠。 阅读 kernel 设计，其中推导了各条规则，并解释了为何可靠性归结为内核；再读 logic 和 tactics 设计，它们说明上层并未增加任何权限。上述形式化规范具有规范性。
参与贡献。 先读代码治理和文档治理，再读规范符合性，了解代码与测试的对应关系以及示例的规则。工作区审计列出未解决的风险；规范变更日志记录规范的修订。
指南
- 用户手册：用户指南兼实现契约，包含支持矩阵和稳定示例。
- 语法指南：定理脚本语法。
- 规范符合性：代码与测试如何对齐规范，以及贡献者的义务。
- 文档治理与代码治理：仓库关于文档、包分层和 alias 入口的规则。
- 形式规范变更日志：规范的修订记录。
- 工作区审计（2026-04-18）：对风险与缺口的阶段性记录。
安装与构建
QED 需要带 moonc 0.10 或更高版本的 MoonBit 工具链，命令行工具依赖 moonbitlang/x 进行文件访问。要在其他模块中使用该库：
moon add Luna-Flow/QED@0.1.0要在仓库中工作：
moon check --target all
moon test
moon run src/cmd examples/truth_file.qedLean 形式化在 formal_verification/ 中通过 lake build 单独构建。