с помощью z3py API. Чтение из расширенных примеров. Каждый пример имеет снаружи универсальный квантификатор. Хотел бы использовать чередование кванторов.
Например:
for_all X существует Y
Один пример, который я считаю полезным, это (для всех графиков существует функция...). Могу ли я добиться этого в Z3py? Если нет, что мне делать? Спасибо.
Это действительно возможно с Z3/Python. Но имейте в виду, что при наличии квантификаторов логика становится полуразрешимой: то есть Z3 может или не может ответить на ваши запросы. (Он не скажет вам ничего неправильного, но может не решить запрос.)
Вот пример из логики первого порядка арифметики, он тривиален, но, надеюсь, он иллюстрирует синтаксис:
(∀x∃y.f(x,y)) → (∀x∃v∃y.(y ≤ v ∧ f(x,y)))
Вот как вы можете закодировать это в Z3, предполагая, что f — это функциональный символ, который принимает два целых числа и возвращает логическое значение:
from z3 import *
f = Function('f', IntSort(), IntSort(), BoolSort())
x, y, v = Ints('x y v')
lhs = ForAll(x, Exists(y, f(x, y)))
rhs = ForAll(x, Exists([v, y], And(y <= v, f (x, y))))
thm = Implies(lhs, rhs)
print thm
solve(Not(thm))
Обратите внимание, что в последней строке мы просим Z3 solve отрицать нашу теорему: Z3 проверяет на выполнимость; поэтому, если он говорит unsat для отрицания нашей теоремы, тогда мы будем знать, что у нас есть доказательство.
Это результат, который я получаю:
Implies(ForAll(x, Exists(y, f(x, y))),
ForAll(x, Exists([v, y], And(y <= v, f(x, y)))))
no solution
Итак, в этом случае Z3 удалось установить теоремность.
Однако в зависимости от вашей проблемы вы также можете получить «неизвестно» в качестве ответа, если окажется, что Z3 не может определить достоверность из-за неполноты.
Int/Bool и т. д., но вы не можете количественно оценить сами типы функций.)
- person alias; 12.06.2017
