Я хочу знать, может ли Z3 отображать эквивалентные формулы после исключения квантификатора.
Пример (существует k) (i x k) = 1 и k > 5 эквивалентен
i > 0 и 5 i - 1 ‹ 0.
Здесь квантор k исключен.
Это возможно?
Спасибо, Каустубх.
Эквивалентные формулы без квантификатора
Ответы (2)
Да, Z3 может проверить эквивалентность двух формул. Чтобы проверить, эквивалентны ли p и q. Мы должны проверить, является ли (not (iff p q)) невыполнимым.
В вашем примере используется нелинейная арифметика i*k. Модуль исключения квантификаторов в Z3 имеет ограниченную поддержку нелинейной действительной арифметики. Он основан на виртуальной замене терминов, которая не является полной. Однако для вашего примера этого достаточно. Мы должны включить модуль исключения квантификатора в Z3 и нелинейные расширения (т. е. виртуальную подстановку терминов).
Вот как мы можем закодировать ваш пример в Z3: http://rise4fun.com/Z3/rXfi
person
Leonardo de Moura
schedule
01.05.2012
В общем случае можно получить результат исключения кванторов. Например, введя следующее в rise4fun:
(declare-const i Real)
(assert (exists ((k Real)) (and (= (* i k) 1.0) (> k 5.0))))
(apply qe)
В этом случае используется нелинейная арифметика, и Z3 не устраняет квантификатор.
person
Josh Berdine
schedule
01.05.2012
Поддержка нелинейной арифметики не включена по умолчанию в модуле исключения квантификатора. Вот почему Z3 не удаляет квантификатор в приведенном выше сценарии. Вот тот же пример с включенной нелинейной поддержкой: rise4fun.com/Z3/qrW1
- person Leonardo de Moura; 01.05.2012
Я вижу, моя ошибка. Для справки, я пытался использовать set-option, но это не сработало: rise4fun.com/Z3/vm7M.
- person Josh Berdine; 01.05.2012
Большое спасибо Джошу и Леонардо. У меня есть еще несколько вопросов, я задаю их отдельно в качестве новой темы.
- person Kaustubh Nimkar; 03.05.2012
