Satallax の変更点

• 追加された行はこの色です。
• 削除された行はこの色です。
• 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/