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/
終了行:
*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/
ページ名: