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

Question

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

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

Answer 1

Утверждается, что

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

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},

[источник]

Answer 2

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

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

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

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