HOL4
の編集
http://www.mathlibre.org/wiki/?HOL4
[
トップ
] [
編集
|
差分
|
バックアップ
|
添付
|
リロード
] [
新規
|
一覧
|
検索
|
最終更新
|
ヘルプ
]
-- 雛形とするページ --
(no template pages)
*HOL4 [#tb60deb7] HOL4 is the latest version of the HOL interactive proof assistant for higher order logic: a programming environment in which theorems can be proved and proof tools implemented. Built-in decision procedures and theorem provers can automatically establish many simple theorems (users may have to prove the hard theorems themselves!) An oracle mechanism gives access to external programs such as SMT and BDD engines. HOL4 is particularly suitable as a platform for implementing combinations of deduction, execution and property checking. HOLファミリーの本家,汎用の対話的証明系です.コンパイルには数時間掛かります. *インストール例 [#he922c7d] export CAS=/usr/local/CAS sudo mkdir $CAS sudo chmod 777 $CAS cd $CAS wget --no-check-certificate https://github.com/Munksgaard/mosml/archive/master.zip unzip -x master cd ./mosml-master/src make world sudo make install cd $CAS wget http://sourceforge.net/projects/hol/files/hol/kananaskis-8/kananaskis-8.tar.gz tar zxvf kananaskis-8.tar.gz cd $CAS/hol-kananaskis-8 mosml < tools/smart-configure.sml ./bin/build sudo ln -s $CAS/hol-kananaskis-8/bin/hol /usr/local/bin/hol4 *使用例 [#aaa58f1b] echo -e "g \`! n. 1 + n <= 2 EXP n\`; e Induct ; e( RW_TAC(arith_ss++ARITH_ss)[] ); e( RW_TAC(arith_ss++ARITH_ss)[arithmeticTheory.EXP,arithmeticTheory.ADD1] );" | hol4 *リンク [#ibfe853b] - http://hol.sourceforge.net/ - http://d.hatena.ne.jp/ehito/20130316/1363425373
タイムスタンプを変更しない
*HOL4 [#tb60deb7] HOL4 is the latest version of the HOL interactive proof assistant for higher order logic: a programming environment in which theorems can be proved and proof tools implemented. Built-in decision procedures and theorem provers can automatically establish many simple theorems (users may have to prove the hard theorems themselves!) An oracle mechanism gives access to external programs such as SMT and BDD engines. HOL4 is particularly suitable as a platform for implementing combinations of deduction, execution and property checking. HOLファミリーの本家,汎用の対話的証明系です.コンパイルには数時間掛かります. *インストール例 [#he922c7d] export CAS=/usr/local/CAS sudo mkdir $CAS sudo chmod 777 $CAS cd $CAS wget --no-check-certificate https://github.com/Munksgaard/mosml/archive/master.zip unzip -x master cd ./mosml-master/src make world sudo make install cd $CAS wget http://sourceforge.net/projects/hol/files/hol/kananaskis-8/kananaskis-8.tar.gz tar zxvf kananaskis-8.tar.gz cd $CAS/hol-kananaskis-8 mosml < tools/smart-configure.sml ./bin/build sudo ln -s $CAS/hol-kananaskis-8/bin/hol /usr/local/bin/hol4 *使用例 [#aaa58f1b] echo -e "g \`! n. 1 + n <= 2 EXP n\`; e Induct ; e( RW_TAC(arith_ss++ARITH_ss)[] ); e( RW_TAC(arith_ss++ARITH_ss)[arithmeticTheory.EXP,arithmeticTheory.ADD1] );" | hol4 *リンク [#ibfe853b] - http://hol.sourceforge.net/ - http://d.hatena.ne.jp/ehito/20130316/1363425373
テキスト整形のルールを表示する