“量化自由逻辑”在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公式。 [related paper]

---

如果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}。

[source]

Answer 2

帕特里克给出了一个很好的答案，但这里还有一些想法。 （我已将此作为评论，但StackOverflow认为它太长了！）

• 请注意，您不能总是玩“否定并检查相反”的技巧。这只有效，因为如果对财产的否定是不可满足的，那么所有投入的财产必须为真。但它并没有反过来：一个属性可以满足，它的否定也是可以满足的。简单的例子：x < 10。这显然是令人满意的，它的否定x >= 10也是如此。所以，你不能总是通过玩这个技巧摆脱量词。它只有在你想要证明某些东西时才有效：然后你可以否定它，看看这种否定是否是不可满足的。如果您担心找到公式的模型，则该方法不适用。
• 您总是可以通过使用未解释的函数替换它们来消除公式并消除所有存在量词。你最终得到的是一个具有所有前缀普遍性的等公式。显然，这不是量词免费的，但这是大多数工具自动为您做的一个非常常见的技巧。
• 所有这些伤害都是交替量词。无论是何种方式，如果你有交替的量词，那么你的问题已经很难处理了。关于量词消除的维基百科页面相当简洁，但它给出了一个非常好的介绍：https://en.wikipedia.org/wiki/Quantifier_elimination底线：并非每个理论都承认量词消除，甚至那些可能需要指数算法来消除它们;导致性能问题。