Prover9

Prover9 is an automated theorem prover for first-order and equational logic, and Mace4 searches for finite models and counterexamples. Prover9 is the successor of the Otter prover.

等号をもつ一階述語論理プルーバーの定番です.

インストール例

MathLibre (20130831) ではインストール済みです.それ以前のバージョンでは次を実行してください.

sudo apt-get -y install prover9-mace4

使用例

「p,qの最大公約数が1,かつ,q*q=p*p*r ならば p=1」

echo "formulas(assumptions).
all a all b all c (G(c,P(a,b)) = 1 <-> G(c,a) = 1 & G(c,b) = 1).
all x G(x,x) = x.
G(p,q) = 1.
P(q,q) = P(P(p,p),r).
-(p = 1).
end_of_list." | prover9

「n*n+n+1は5の倍数ではない」

echo "formulas(assumptions).
all n ( q (n) <-> -(MOD(p(p(t(n,n),n),1),5) = 0)).
all r ( r < 5 -> (r = 0)|(r = 1)|(r = 2)|(r = 3)|(r = 4) ).
( q(0) & q(1) & q(2) & q(3) & q(4) ).
all n ( MOD(n,5) < 5 ).
all n ( 0 < n -> (all k ( MOD(MOD(k,n),n) = MOD(k,n)))).
all n ( 0 < n -> (all j all k ( MOD(p(MOD(j,n) , MOD(k,n)),n) = MOD(p(j , k),n)))).
all n ( 0 < n -> (all j all k ( MOD(t(MOD(j,n) , MOD(k,n)),n) = MOD(t(j , k),n)))).
-(all n ( q(n) )).
end_of_list." | prover9 -t -1

反例の生成

echo "formulas(assumptions).
all a all b all c (G(c,P(a,b)) = 1 <-> G(c,a) = 1 & G(c,b) = 1).
all x G(x,x) = x.
G(p,q) = 1.
P(q,q) = P(P(p,p),r).
-(q = 1).
end_of_list." | mace4 -p 1

GUI

prover9-mace4

起動後,Goals ウインドウに http://d.hatena.ne.jp/ehito/20130301/1362109843 のテキストをコピペ,Start ボタンで実行.

リンク


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