软件截图:
HOL从短高阶逻辑是其中的定理可以证明和防爆工具实现的编程环境。
内置的决策程序和定理证明能自动建立很多简单的定理。一个oracle的机制可以访问外部程序，如SAT和BDD引擎。
HOL 4特别适合作为实现的扣除，执行和检查物业组合的平台
什么在此版本中是新的：
- 在HolSmtLib现在还支持Z3证明重建目标涉及固定宽度的文字和翻译HOL进入SMT-LIB 2格式。
- 在HolQbfLib支持检查既有效性和证书Squolem 2.02的无效。 wordsSyntax.mk_word_replicate计算所得字的宽度时施加到标号和一个固定宽度字。
- 在该系统支持语法小数。
- 在此语法映射到窗体的分工条件N /10米。
- 在核心系统，这个语法是启用了真正的，理性的，复杂的理论。
什么在6个版本是新的：
- 在该HolSmtLib库现在支持重建的证明了SMT求解器Z3 。
- 在许多类型的变量，现在可以解析并打印成小写希腊字母。
- 在有界的重写工作得更好。
- 在涉及EL运营商方面的简化是更好的。
- 在包包操作改进的支持。
- 在语法更新之类的全集。
- 在其他小的改进和错误修正。
评论没有发现