高い順序ロジック （HOL） はどの定理を証明することができますと実装プルーフ ツール プログラミング環境です。組み込みの決定プロシージャおよび定理証明器自動的に多くの単純な定理を確立できます。Oracle メカニズムは BDD エンジンや土などの外部プログラムにアクセスできます。HOL 4 は控除、実行、およびプロパティのチェックの組み合わせを実装するためのプラットフォームとして特に適しています。
