Z3の場合、a3 = x * y * zの場合、3a <= x + y + z

Question

私はZ3の初心者です（今日開始）。今のところそれはたくさん好きです。素晴らしいツール。残念ながら、構文は私を少し混乱させます。

Iは、IFことを証明する：（

^3 = X Y Z = M、X、Y、Z、M（0..1）とその後）

：

私はそれを満たすモデルを見つけることを試みることによってそう3A < =（X + Y + Z）

：

3A>（X + Y + Z）

ここで

はZ3コードです：

(declare-const a Real) 
(declare-const x Real) 
(declare-const y Real) 
(declare-const z Real) 
(declare-const m Real) 

(assert (> a 0)) 
(assert (< a 1)) 
(assert (> x 0)) 
(assert (< x 1)) 
(assert (> y 0)) 
(assert (< y 1)) 
(assert (> z 0)) 
(assert (< z 1)) 
(assert (> m 0)) 
(assert (< m 1)) 

(assert (= (* (* a a) a) m)) 
(assert (= (* (* x y) z) m)) 
(assert (> (* 3.0 a) (+ (+ z y) x))) 
(check-sat) 

モデルは満足できません。

私は何を望んでいたのですか？私が言ったように、私は完全な初心者なので、構文は私を混乱させます。

Answer 1

解決策は正しいです。

説明：

0 < x < 1 
0 < y < 1 
0 < z < 1 
0 < m < 1 
a * a * a = m 
x * y * z = m 
3 * a > x + y + z 

Z3はこれが充足不能であると言う：あなたが書いたものは同等です。したがって、 Z = M（と、X、Y、Z、M（0..1））

次いで

^3 = X yの場合、それ

3A>（X + Y + Z）

： その場合ではないでき0

この問題が発生した場合、SMTの問題は満足できるものとなり、SMTの問題が満たされないというZ3の主張と矛盾します。 3a > (x+y+z)であることができない場合は、最初に証明したかった文である3a <= (x+y+z)である必要があります。

Answer 2

あなたの解決策は正しいと思います。 Z3を使って文Aの妥当性を証明する方法について少し説明しましょう。

• Anegation(A)が充足不能であるときに限り有効である：キーアイデアは、古典論理で、例えば、命題論理と述語論理が、ということです。

これはかなりよく知られた結果です。例えば、this slideの4ページにある多くの教科書や教材で見つけることができます。したがって、P -> Qの妥当性は、その否定の不満足性をチェックすることによって証明することができます：P /\ negation(Q)。特に

は、ご例えば、

(a^3 = x*y*z = m) -> (3a <= x+y+z)は

(a^3 = m) /\ (x*y*z = m) /\ (3a > x+y+z) IFF

がUnsatifiableで、有効です。