证明助手

在计算机科学和数理逻辑中，证明助手或交互式定理检验器是一种软件工具，通过人机协作来协助开发形式证明。

这涉及到某种交互式证明编辑器，或其他界面，人类可以用它来指导搜索证明，其细节存储在计算机中，并由计算机提供一些步骤。

系统比较ACL2--一种编程语言，一种一阶逻辑理论，以及博耶-摩尔传统的定理验证器（有交互式和自动模式）。Coq--允许表达数学断言，机械地检查这些断言的证明，帮助寻找形式证明，并从其形式规范的构造证明中提取认证程序。HOL定理验证器--最终由LCF定理验证器衍生的工具系列。

在这些系统中，逻辑核心是其编程语言的一个库。定理代表语言的新元素，只能通过保证逻辑正确性的策略引入。策略组合使用户能够在与系统相对较少的互动中产生重要的证明。

这个家族的成员包括：HOL4-主要的后裔，仍在积极开发中。支持MoscowML和Poly/ML。HOLLight-一个蓬勃发展的极简主义分叉，基于OCML。ProofPower-曾经是专有的，然后又回到了开放源码。

基于StandardML。IMPS，一个交互式数学证明系统是一个交互式定理检验器，是HOL的继承者。

主要代码库是BSD许可的，但Isabelle发行版捆绑了许多不同许可的附加工具。Jape-基于Java。LeanLEGOMatita-基于归纳构造微积分的轻型系统。

MINLOG-基于一阶最小逻辑的证明助手。Mizar-基于一阶逻辑的证明助手，采用自然演绎风格，以及塔斯基-格罗滕迪克 (Tarski-Grothendieck) 集合理论。PhoX-基于高阶逻辑的证明助手，是eXtensible。PrototypeVerificationSystem(PVS 样机验证系统)-基于高阶逻辑的证明语言和系统。

TPS和ETPS-同样基于简单类型的λ演算 (lambdacalculus) 的交互式定理证明器，但基于逻辑理论的独立表述和独立实现。

TypelabYarrow 定理证明器博物馆是一个保护定理证明器系统来源的倡议，以备将来分析，因为它们是重要的文化/科学文物。它拥有上面提到的许多系统的来源。

一个流行的证明助手的前端是基于Emacs的一般证明 (ProofGeneral)，由爱丁堡大学开发。Coq包括CoqIDE，它是基于OCaml/Gtk的。Isabelle包括Isabelle/jEdit，它是基于jEdit和Isabelle/Scala基础设施的面向文档的证明处理。