Как проверить теорему, которая включает в себя тригонометрию с Z3 Prover? - PullRequest
Новая
       17

Как проверить теорему, которая включает в себя тригонометрию с Z3 Prover?

0 голосов
/ 11 июля 2019

Я пытаюсь доказать следующее утверждение с помощью Z3 Теорема Доказатель : 

|CA|^2 = |AB|^2 + |BC|^2,
|AB| = cos(alpha),
|BC| = sin(alpha)
  =>
|CA| = 1

Что именно я делаю: 

(declare-const AB Real)
(declare-const BC Real)
(declare-const CA Real)
(declare-const alpha Real)

(assert  (and (>= AB 0) (>= BC 0) (>= CA 0)) )
(assert  (= (^ CA 2) (+ (^ AB 2) (^ BC 2))) )
(assert  (= AB (cos alpha)) )
(assert  (= BC (sin alpha)) )

(assert (not  (= CA 1) ))

(check-sat)

Я ожидаю unsat , но получил unknown .Также я знаю, что проблема сконцентрирована в части с функциями sin и cos .

Что я делаю неправильно?Можно ли вообще что-то сделать?

Спасибо за помощь!

1 Ответ

1 голос
/ 11 июля 2019

z3 имеет довольно ограниченное понимание sin и cos, и я не ожидаю, что он сможет решить все такие проблемы. Подробнее об этом см. https://github.com/Z3Prover/z3/issues/680.. Для сложных запросов нормально получить unknown в качестве ответа.

Сказав это, вам повезло! Z3 может действительно правильно ответить на ваш конкретный запрос; но вы должны использовать правильное заклинание. Вместо: 

(check-sat)

Используйте 

(check-sat-using qfnra-nlsat)

и z3 правильно выводят unsat для этой проблемы. Эта форма check-sat говорит z3 использовать внутренний механизм nl-sat для нелинейной вещественной арифметики.

...