Prover9 の変更点

• 追加された行はこの色です。
• 削除された行はこの色です。
• Prover9 へ行く。

*Prover9 [#m3e2f1e0]
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. 

等号をもつ一階述語論理プルーバーの定番です．
*インストール例 [#w56df5ea]

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

 sudo apt-get -y install prover9-mace4
*使用例 [#w6fd8796]
「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 ボタンで実行．

*リンク [#vc2358da]
- http://www.cs.unm.edu/~mccune/mace4/
- http://www.cs.unm.edu/~mccune/mace4/manual/2009-11A/