Вот запрос Z3, который выдает «sat» в качестве результата.(Я использую Z3 версии 4.8.0, результаты идентичны в веб-интерфейсе rise4fun.)
(assert (forall ((x Real))
(exists ((y Real))
(and (<= 0.0 y) (<= y 1.0) (<= x (* y y))))))
(check-sat)
Однако эта формула должна быть неудовлетворительной!Не каждое действительное число меньше или равно квадрату числа от 0 до 1.
Результат изменится, если я переставлю формулы в соединении:
(assert (forall ((x Real))
(exists ((y Real))
(and (<= x (* y y)) (<= 0.0 y) (<= y 1.0)))))
(check-sat)
Тогда я получу "unsat ", что хорошо.
Если я включу генерацию пробных отпечатков, то получу" unknown ", по крайней мере, звук.
(set-option :produce-proofs true)
(assert (forall ((x Real))
(exists ((y Real))
(and (<= 0.0 y) (<= y 1.0) (<= x (* y y))))))
(check-sat)
Может кто-нибудь подсказать, чтопродолжается?Я что-то упустил или это ошибка?