The HOL Light theorem prover

HOL Light is a computer program to help users prove interesting mathematical theorems completely formally in higher order logic. It sets a very exacting standard of correctness, but provides a number of automated tools and pre-proved mathematical theorems (e.g. about arithmetic, basic set theory and real analysis) to save the user work. It is also fully programmable, so users can extend it with new theorems and inference rules without compromising its soundness.

名称は HOL のライト版のようであり,実際,Isabelle2013 のような強力な検索ツールも(デフォルトでは)付属せず,ProofPower のような大掛かりなインターフェイスも持ちませんが,本家 HOL の先駆的な数学ライブラリの作者が独立させた,Cambridge HOL ファミリー中,数学の公理論的構成という定理証明システム本来の目的に最も適したシステム,それが HOL Light です.

インストール例

MathLibre (20130831) ではインストール済みです.それ以前のバージョンでは次を実行してください.

sudo apt-get install hol-light

(*最新版を用いる場合は,適当なディレクトリで

svn co http://hol-light.googlecode.com/svn/trunk/ hol-light
cd ./hol-light
make

*)

使用例

起動(初期ファイルのロードに1〜2分掛かります)

cd /usr/share/hol-light 
hol-light

(*最新版を用いる場合は,make を実行したディレクトリに移動して

rlwrap ocaml -init ./hol.ml

*)

数学的帰納法(まとめてコピペしても通りますが,1行ずつの方が過程が見易いです)

g `!n. ?x. x * x <= n /\ n < SUC x * SUC x`;;
e INDUCT_TAC;;
e(EXISTS_TAC`0` THEN ARITH_TAC);;
e(POP_ASSUM MP_TAC THEN STRIP_TAC);;
e(ASM_CASES_TAC`SUC n = SUC x * SUC x`);;
e(EXISTS_TAC`SUC x` THEN ASM_ARITH_TAC);;
e(EXISTS_TAC`x:num` THEN ASM_ARITH_TAC);;
top_thm();;

余弦関数の3倍角公式

needs "Library/transc.ml";;
g `!x. cos (&3 * x) = &4 * cos x pow 3 - &3 * cos x`;;
e(GEN_TAC THEN SIMP_TAC[REAL_ARITH`&3 * x = x + x + x`;COS_ADD;SIN_ADD]);;
e(MP_TAC(SPEC_ALL SIN_CIRCLE));;
e(CONV_TAC REAL_RING);;
top_thm();;

終了

#quit;;

リンク


トップ   編集 凍結 差分 バックアップ 添付 複製 名前変更 リロード   新規 一覧 単語検索 最終更新   ヘルプ   最終更新のRSS
Last-modified: 2015-01-09 (金) 18:44:24 (2041d)