軟件截圖:
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運營商方面的簡化是更好的。
- 在包包操作改進的支持。
- 在語法更新之類的全集。
- 在其他小的改進和錯誤修正。
評論沒有發現