主要证据
- The PLTP ArchiveS1 · 主要研究来源 · 代码仓库
Edinburgh Pure Lisp Theorem Prover 将自动归纳推理用于程序性质证明
PLTP 面向基于归结的一阶证明器难以处理的递归程序性质，采用以化简与归纳为核心的专门证明过程。
发生了什么？
Boyer 与 Moore 在 IJCAI-73 发表“Proving Theorems about LISP Functions”，公开记录 1972–1973 年开发的 Edinburgh Pure Lisp Theorem Prover 及其自动归纳、重写与符号求值方法。
为什么重要？
它建立了长期发展的自动归纳定理证明与程序验证架构，并演化为多个重要后续系统。
重要性说明：Boyer 与 Moore 的 PLTP 建立了面向递归 Lisp 函数的自动归纳推理谱系，并成为后来的 Boyer–Moore prover、NQTHM 与 ACL2 的前史。
历史脉络
更早进展
—
后续进展
—
相关里程碑
—
证据与状态一览
- 重要性
- H2 · 领域里程碑
- 验证状态
- 论文已发布
- 证据等级
- E3 · 可检查工件
- AI 角色
- AI 自主主导
- 形式保障
- 有形式化工件
贡献与验证
- 数学新颖性
- 工具性进展
- 接口
- 形式化, 符号
- AI 贡献
- 证明器自动化简公式、选择归纳方案并搜索递归函数性质的证明。
- 人类贡献
- Robert Boyer 与 J Strother Moore 设计并实现逻辑、启发式与证明过程。
- 验证状态
- 论文已发布 · E3 · 可检查工件 · 有形式化工件
- 最后审阅
- 2026-09-15
技术细节
- 系统
- pltp
- 机构
- university-of-edinburgh
- 数学问题
- inductive-theorem-proving, program-verification
- 方法
- mathematical-induction, rewriting, symbolic-evaluation
全部来源与工件
- The PLTP ArchiveS1 · 主要研究来源 · 代码仓库 · 访问于 2026-09-15
验证历史
- 1973-08-20 · 论文已发布 · E2 · 研究记录
IJCAI-73 论文记录了 PLTP 及其定理证明方法。
- 2026-09-15 · 论文已发布 · E3 · 可检查工件
UT Austin 的 PLTP 档案保存 1973 年原始源代码清单以及现代转录与重建版本。
更正
当前没有记录的更正。