2017-06-11 12 views
1

使用z3py API。 advanced examplesからの読書すべての例には、普遍的な量量子が外部にあります。量指定子の変更を使用したいと思います。例えばZ3の量子の変更?

for_all XがY

つが存在する私はそれが便利だと思うのインスタンスは、(すべてのグラフのために...機能が存在する)です。 私はZ3pyでそれを達成できますか?そうでない場合、私は何をすべきですか?ありがとう。

答えて

2

これは確かにZ3/Pythonで可能です。しかし、量指定子が存在するとき、論理は半決定可能になります。つまり、Z3はあなたの質問に答えることができないかもしれません。 (。それはあなたに何も悪いことを教えてくれませんが、クエリを解決するために失敗することがあります)

をここで算術の一階述語論理の一例ですが、それは些細だが、うまくいけば、それは構文を示しています

(∀x∃y.f(x,y)) → (∀x∃v∃y.(y ≤ v ∧ f(x,y))) 

Z3のチェックを:最後の行に私たちは私たちの定理の否定をsolveするZ3を依頼することを

from z3 import * 

f = Function('f', IntSort(), IntSort(), BoolSort()) 
x, y, v = Ints('x y v') 

lhs = ForAll(x, Exists(y, f(x, y))) 
rhs = ForAll(x, Exists([v, y], And(y <= v, f (x, y)))) 
thm = Implies(lhs, rhs) 

print thm 

solve(Not(thm)) 

注:ここでは、Z3で、fを仮定すると、2つの整数を取り、ブール値を返す関数のシンボルであることをコーディングすることができます方法ですsatisfiabiのために不安;ですから、私たちの定理の否定のためにunsatと言うなら、私たちは証明があることを知ります。

これは私が得る出力されます。この場合、Z3はtheoremhoodを確立することができた、

Implies(ForAll(x, Exists(y, f(x, y))), 
     ForAll(x, Exists([v, y], And(y <= v, f(x, y))))) 
no solution 

ので。

しかし、あなたの問題によっては、Z3が不完全さのために妥当性を判断できないことが判明した場合、あなたは答えとして「不明」を得るかもしれません。

+0

ありがとうございました。 n引数のすべての可能なブール関数を反復することは可能ですか? – user2754673

+0

"反復"の意味がわかりません。関数自体を定量化できるかどうかを尋ねるなら、答えは「いいえ」です。これには、SMTLib量指定子ではサポートされていない高次論理が必要です。 ( 'Int' /' Bool'などで定量化することはできますが、関数型自体を数値化することはできません) –

+0

はい。私は、機能を定量化することを意味していました。答えをありがとう。 – user2754673

関連する問題