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

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

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

リンク


添付ファイル: file2013101401.png 1372件 [詳細]

トップ   編集 凍結 差分 バックアップ 添付 複製 名前変更 リロード   新規 一覧 単語検索 最終更新   ヘルプ   最終更新のRSS
Last-modified: 2015-01-09 (金) 18:44:24 (2516d)