在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 unsat ∀x.¬φ(x)__¹)上的一个(简单)正出现。

1:假设φ(x)是无量词的；正如@Levent在他的回答中指出的那样，当φ(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

帕特里克给出了一个很好的答案，但这里还有一些想法。(我本来会把这个作为评论的，但StackOverflow认为这太长了！)

• 请注意，您不能总是玩“否定并检查相反的”伎俩。这只是因为如果一个属性的否定是不可满足的，那么该属性对于所有输入都必须是真的。但事实并非如此:一个属性可以满足，它的否定也可以满足。简单的例子：x < 10。这显然是可满足的，它的否定x >= 10也是如此。所以，你不能总是通过玩这个把戏来摆脱量词。只有当你想证明某件事时，它才能起作用:然后你可以否定它，看看这种否定是否是不可满足的。如果你关心的是找到一个公式的模型，这个方法就不适用了。
• 通过用未解释的函数替换存在量词，您总是可以浏览公式并消除所有存在量词。你最终得到的是一个具有所有前缀普遍性的等差公式。显然，这不是免费的量词，但这是一个非常常见的技巧，大多数工具都是自动为您做的。
• 所有这些伤害的地方是交替量词。不管你的问题是什么，如果你有交替的量词，那么你的问题已经很难处理了。维基百科关于量词消除的页面相当简洁，但它给出了一个非常好的介绍：消去的底线是:并非所有理论都承认量化消除，即使是那些承认量化消除的理论也可能需要指数算法来消除它们；这会导致性能问题。