Satallax

Satallax †

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 にタブロー法で解かせるものです．

インストール例 †

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

使用例 †

入力の書式は 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

パネルの「↓」を繰り返しクリックすれば，過程が確認できます．

• 反例の生成

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

リンク †

• http://www.ps.uni-saarland.de/~cebrown/satallax/

最新の20件