Что означает «свободная логика» в контексте SMT? - PullRequest
Новая
       25

Что означает «свободная логика» в контексте SMT?

0 голосов
/ 18 февраля 2019

Даже для простейших арифметических задач SMT экзистенциальный квантор требуется для объявления символических переменных.И ∀ квантификатор может быть превращен в ∃ путем обращения ограничения.Итак, я могу использовать оба из них в QF_* логиках, и это работает.

Я так понимаю, «без квантификатора» означает что-то еще для таких логик SMT, но что именно?

Ответы [ 2 ]

0 голосов
/ 20 февраля 2019

Патрик дал отличный ответ, но вот еще несколько мыслей.(Я бы поставил это как комментарий, но StackOverflow считает, что это слишком долго для этого!)

  • Обратите внимание, что вы не всегда можете сыграть трюк «отрицание и проверка противоположного».Это работает только потому, что если отрицание свойства неудовлетворительно, то свойство должно быть истинным для всех входных данных.Но это не наоборот: свойство может быть выполнимым, и его отрицание также может быть выполнимым.Простой пример: x < 10.Это очевидно выполнимо, так же как и его отрицание x >= 10.Таким образом, вы не всегда можете избавиться от квантификаторов, используя этот трюк.Это работает, только если вы хотите что-то доказать: тогда вы можете отрицать это и посмотреть, является ли это отрицание неудовлетворительным.Если вас беспокоит поиск модели для формулы, метод не применяется.

  • Вы всегда можете сколемизировать формулу и исключить все экзистенциальные кванторы, заменив их неинтерпретированными функциями.,То, что вы в итоге получите, это уравновешенная формула, которая имеет все префиксные универсалии.Очевидно, это не без квантификатора, но это очень распространенный прием, который большинство инструментов делают для вас автоматически.

  • Где все это болит, это чередующиеся квантификаторы.Независимо от сколемизации, если у вас есть чередующиеся квантификаторы, с вашей проблемой уже трудно справиться.Страница Википедии об исключении кванторов довольно краткая, но она дает очень хорошее введение: https://en.wikipedia.org/wiki/Quantifier_elimination Итог: не каждая теория допускает исключение кванторов, и даже те, которые действительно могут требовать экспоненциальных алгоритмов, чтобы избавиться от них;вызывая проблемы с производительностью.

0 голосов
/ 19 февраля 2019

Утверждается, что квантификатор

∀ можно превратить в ∃ путем обращения ограничения

AFAIK , следующеесправедливы два отношения: 

 ∀x.φ(x) <=> ¬∃x.¬φ(x)
¬∀x.φ(x) <=>  ∃x.¬φ(x)

Поскольку формула SMT без кванторов φ(x) равна равнозначна ее экзистенциальному замыканию ∃x.φ(x), мы можем использовать фрагмент SMT без кванторовТеория для выражения (простого) отрицания вхождения универсального количественного определения, и [AFAIK] также (простого) положительного вхождения универсального количественного определения в тривиальнойформулы (например, если [∃x.]φ(x) равно unsat, то ∀x.¬φ(x) ¹) .

¹: предполагается, что φ(x) не содержит квантификаторов;Как отмечает @Levent Erkok в своем ответе, этот подход не дает результатов, когда и φ(x), и ¬φ(x) являются удовлетворительными

Однако мы не можем, например, найти модель для следующей количественной формулыиспользование фрагмента SMT без квантификатора: 

[∃y.]((∀x.y <= f(x)) and (∃z.y = f(z)))

Для записей это кодирование задачи OMT min(y), y=f(x) в качестве количественной формулы SMT.[ связанная бумага ]

Термин t не не содержит квантификаторов если t синтаксически не содержит квантификаторов.Формула без квантификатора φ является равноудаленной с ее экзистенциальным замыканием 

(∃x1. (∃x2 . . .(∃xn.φ ). . .))

, где x1, x2, . . . , xn - любое перечисление free(φ), свободные переменные в φ.

Набор свободных переменных члена t, free(t), индуктивно определяется как:

  • free(x) = {x}, если x является переменной,
  • free((f t1 t2 . . . tk)) = \cup_{i∈[1,k]} free(ti) для функциональных приложений,
  • free(∀x.φ) = free(φ) \ {x} и
  • free(∃x.φ) = free(φ) \ {x}.

[источник]

...