Satallax
の編集
http://ftp.mathlibre.org/wiki/?Satallax
[
トップ
] [
編集
|
差分
|
バックアップ
|
添付
|
リロード
] [
新規
|
一覧
|
検索
|
最終更新
|
ヘルプ
]
-- 雛形とするページ --
(no template pages)
*Satallax [#ye7fa280] Satallax is an automated theorem prover for higher-order logic. The particular form of higher-order logic supported by Satallax is Church's simple type theory with extensionality and choice operators. Satallax は古典高階論理の高性能プルーバーです.原理は命題論理に変換後,SAT ソルバー MiniSat にタブロー法で解かせるものです. *インストール例 [#q39293b5] export CAS=/usr/local/CAS export MROOT=/usr/local/CAS/satallax-2.7/minisat sudo mkdir $CAS sudo chmod 777 $CAS cd $CAS wget http://www.ps.uni-saarland.de/~cebrown/satallax/downloads/satallax-2.7.tar.gz tar zxvf ./satallax-2.7.tar.gz cd ./satallax-2.7/minisat/core make Solver.o cd ../simp make SimpSolver.o cd ../../picosat-936 ./configure make cd .. ./configure make sudo ln -s /usr/local/CAS/satallax-2.7/bin/satallax.opt /usr/local/bin/satallax echo 'Add LoadPath "/usr/local/CAS/satallax-2.7/coq".' >> ~/.coqrc coqc ./coq/stt.v coqc ./coq/stttab.v *使用例 [#hd20376f] 入力の書式は TPTP の高階論理のコア言語 THF0 です. - 右逆写像の存在 echo 'thf(x,type,x : $tType). thf(y,type,y : $tType). thf(f,type,f : x > y). thf(gl,conjecture, ((! [Y : y] : ? [X : x] : ( (f @ X) = Y )) <=> (? [G : y > x] : ! [Y : y] : ((f @ (G @ Y)) = Y ) ))).'> demo1.p これが定理であることを示し,その証明スクリプトを型理論のプルーフ・アシスタント Coq のフォーマットで書き出します. satallax -verb 21 -p coqscript -c ./demo1.v ./demo1.p 保存されたファイルを CoqIDE に読み込み coqide ./demo1.v パネルの「↓」を繰り返しクリックすれば,過程が確認できます. &ref(2013101401.png); - 反例の生成 echo 'thf(x,type,x : $tType). thf(y,type,y : $tType). thf(f,type,f : x > y). thf(g1,type,g1 : y > x). thf(g2,type,g2 : y > x). thf(ax1,axiom,! [Y : y] : ((f @ (g1 @ Y)) = Y)). thf(ax2,axiom,! [Y : y] : ((f @ (g2 @ Y)) = Y)). thf(gl,conjecture,g1 = g2 ).'> demo2.p satallax -p model ./demo2.p *リンク [#x8010cd7] - http://www.ps.uni-saarland.de/~cebrown/satallax/
タイムスタンプを変更しない
*Satallax [#ye7fa280] Satallax is an automated theorem prover for higher-order logic. The particular form of higher-order logic supported by Satallax is Church's simple type theory with extensionality and choice operators. Satallax は古典高階論理の高性能プルーバーです.原理は命題論理に変換後,SAT ソルバー MiniSat にタブロー法で解かせるものです. *インストール例 [#q39293b5] export CAS=/usr/local/CAS export MROOT=/usr/local/CAS/satallax-2.7/minisat sudo mkdir $CAS sudo chmod 777 $CAS cd $CAS wget http://www.ps.uni-saarland.de/~cebrown/satallax/downloads/satallax-2.7.tar.gz tar zxvf ./satallax-2.7.tar.gz cd ./satallax-2.7/minisat/core make Solver.o cd ../simp make SimpSolver.o cd ../../picosat-936 ./configure make cd .. ./configure make sudo ln -s /usr/local/CAS/satallax-2.7/bin/satallax.opt /usr/local/bin/satallax echo 'Add LoadPath "/usr/local/CAS/satallax-2.7/coq".' >> ~/.coqrc coqc ./coq/stt.v coqc ./coq/stttab.v *使用例 [#hd20376f] 入力の書式は TPTP の高階論理のコア言語 THF0 です. - 右逆写像の存在 echo 'thf(x,type,x : $tType). thf(y,type,y : $tType). thf(f,type,f : x > y). thf(gl,conjecture, ((! [Y : y] : ? [X : x] : ( (f @ X) = Y )) <=> (? [G : y > x] : ! [Y : y] : ((f @ (G @ Y)) = Y ) ))).'> demo1.p これが定理であることを示し,その証明スクリプトを型理論のプルーフ・アシスタント Coq のフォーマットで書き出します. satallax -verb 21 -p coqscript -c ./demo1.v ./demo1.p 保存されたファイルを CoqIDE に読み込み coqide ./demo1.v パネルの「↓」を繰り返しクリックすれば,過程が確認できます. &ref(2013101401.png); - 反例の生成 echo 'thf(x,type,x : $tType). thf(y,type,y : $tType). thf(f,type,f : x > y). thf(g1,type,g1 : y > x). thf(g2,type,g2 : y > x). thf(ax1,axiom,! [Y : y] : ((f @ (g1 @ Y)) = Y)). thf(ax2,axiom,! [Y : y] : ((f @ (g2 @ Y)) = Y)). thf(gl,conjecture,g1 = g2 ).'> demo2.p satallax -p model ./demo2.p *リンク [#x8010cd7] - http://www.ps.uni-saarland.de/~cebrown/satallax/
テキスト整形のルールを表示する
添付ファイル:
2013101401.png
1560件
[
詳細
]