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/
終了行:
*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/
ページ名: