![[PukiWiki]](image/knxmpen.png "[PukiWiki]")
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 ボタンで実行．
