hol

内容列表

HOL 交互式定理证明器是高阶逻辑的证明助手:可以证明定理并实现证明工具的编程环境。内置的决策程序和定理证明器可以自动建立许多简单的定理(用户可能必须自己证明硬定理!) 预言机机制可以访问外部程序,例如 SMT 和 BDD 引擎。HOL 特别适合作为实现演绎、执行和属性检查相结合的平台。

其他 HOL 在别处进行了描述。

HOL 是免费软件,在修改(3 条款)BSD 许可下发布。

欢迎新的开发者。

历史

在过去的 30 年里,有几个广泛使用的 HOL 系统版本:

  1. HOL88 来自剑桥;
  2. 卡尔加里和贝尔实验室的 HOL90;
  3. HOL98 来自剑桥、格拉斯哥和犹他州。

当前版本以及上述版本的后续版本是 HOL4。它的开发部分得到了PROSPER项目的支持。HOL4 基于 HOL98 并结合了HOL Light的想法和工具。

分类: 默认 标签: 发布于: 2022-06-20 15:23:11, 更新于: 2022-07-07 10:38:39