HOL（证明助手）

HOL（高阶逻辑）表示一个使用类似（高阶）逻辑和实现策略的交互式定理证明系统家族。这个系列的系统遵循LCF的方法，因为它们被实现为一个库，该库定义了一个被证明的定理的抽象数据类型，这样，这种类型的新对象只能使用库中对应于高阶逻辑推理规则的函数来创建。

只要这些函数被正确实现，系统中所有被证明的定理都必须是有效的。因此，一个大的系统可以建立在一个小的可信内核之上。HOL家族中的系统使用ML或其继承者。ML最初是和LCF一起开发的，作为定理证明系统的元语言；事实上，这个名字代表了元语言。

HOL系统使用经典高阶逻辑的变体，它有简单的公理基础，公理很少，语义很好理解。HOL证明器中使用的逻辑与Isabelle/HOL密切相关，后者是Isabelle中使用最广泛的逻辑。HOL的实现尽管HOL是Isabelle的前身，但各种HOL的衍生物仍在活跃使用。这就是目前的四个HOL系统（共享本质上相同的逻辑）。

HOL4--目前唯 一被维护和开发的系统，源于HOL88系统，它是由MikeGordon领导的原始HOL实现工作的高潮。HOL88包括它自己的ML实现，它又是在CommonLisp的基础上实现的。

HOL88之后的系统（HOL90、HOL98和HOL4）都是用标准ML实现的；而HOL98是与MoscowML耦合的，HOL4可以用MoscowML或Poly/ML构建。所有这些都带有大量的定理证明代码库，在非常简单的核心代码之上实现额外的自动化。

HOL4是BSD授权的。HOLLight-HOL的一个实验性极简版本，后来发展成为另一个主流的HOL变体；其逻辑基础仍然异常简单。HOLLight最初用CamlLight实现，现在使用OCaml。

HOLLight在新的BSD许可下可用。ProofPower-一组工具，旨在为使用形式化规范的Z符号工作提供特殊支持。

6个工具中有5个是GNUGPLv2许可的。第六个(PPDaz)有一个专有许可证。HOLZero-一个专注于可信度的最小化实现。HOLZero是GNUGPL3+许可的。形式证明的发展CakeML项目为ML开发了一个形式证明的编译器。