kananaskis-13-description.pdf (kananaskis-13-description.pdf( 外部リンク: SF.net): 1,644,093 バイト)のダウンロードが開始されます。開始されない場合，左のリンクをクリックしてください。
HOL は高階論理の定理の証明システムです。それは様々 な既存の理論の数学と理論計算機科学のさまざまな部分をほのめかしたが付属しています。
