Z3, чтобы показать, что если a^3=x*y*z, то 3a <= x+y+z

Question

Я полный новичок с Z3 (началось сегодня). Пока что это очень нравится. Отличный инструмент. К сожалению, синтаксис меня немного смущает.

Я хочу доказать это, если:

a ^ 3 = xy z = m (с a, 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 говорит, что это неудовлетворительно. Таким образом, если

a ^ 3 = xy z = m (с a, x, y, z, m (0..1))

тогда не может быть так, чтобы:

3a> (x + y + z)

потому что, если бы это произошло, то поставленная вами проблема SMT была бы выполнимой, что противоречило бы утверждению Z3 о том, что проблема SMT является неудовлетворительной. Если это не может быть так, что 3a > (x+y+z), то это должно быть так, что 3a <= (x+y+z)Это утверждение, которое вы изначально хотели доказать.

Answer 2

Я думаю, что ваше решение верное. Позвольте мне объяснить немного об использовании Z3, чтобы доказать правильность утверждения A, Основная идея заключается в том, что в классической логике, например, логика высказываний и логика предикатов:

• A Действителен, если negation(A) неудовлетворительно

Это довольно известный результат. Вы можете найти его во многих учебниках и материалах, например, на странице 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) Неуязвим.