了解 z3 中的量词

Question

我试图理解这个例子：

solve([y == x + 1, ForAll([y], Implies(y <= 0, x < y))])

但是看了explanation还是没看懂。

你怎么看这个？ []是什么意思？

我对此的错误解释是。 “给定定理 y == x + 1。它是否适用于所有 y 使得 Implies(y y = 0 和 x = -1 每个约束 (Implies(y

你对如何理解这个话题有任何帮助吗？

Answer 1

看起来这里有一些混淆。让我们首先理清绑定：在量词上下文中，变量是独立的，即可以在不改变语义的情况下对其进行重命名。所以，你的原件：

from z3 import *
x, y = Ints('x y')
solve([y == x + 1, ForAll([y], Implies(y <= 0, x < y))])

是完全等同于：

from z3 import *
x, y, z = Ints('x y z')
solve([y == x + 1, ForAll([z], Implies(z <= 0, x < z))])

请注意，我们将ForAll 的“范围”中的y 替换为z，但未触及第一个连词中的那个。只能在ForAll（或Exist）范围内重命名，不能超出范围。

而且这两个等价的表达式都是不可满足的。为什么？第一个合取容易满足；只需选择一个任意的x，并将y 设置为x+1，就完成了。这是不能满足的第二个合取。因为，无论您选择满足哪个x，您总能找到一个小于x 的z（只需选择min(0, x-1)），并且该分配的量化公式变为False。因此没有解决方案。

现在，让我们考虑一下您的 cmets 中的变体，x > z：

from z3 import *
x, y, z = Ints('x y z')
solve([y == x + 1, ForAll([z], Implies(z <= 0, x > z))])

同样，第一个合取很容易满足。这一次，第二次也是如此，因为你可以选择一个积极的x，只要z <= 0，这将比所有z 都要大，因此暗示总是正确的。这正是 z3 告诉你的，当它给你一个令人满意的任务时：

[x = 2, y = 3]

请注意，此赋值中没有关于变量z 的任何内容。您无法真正为普遍量化的公式提供模型；根据定义，z 的所有值都是 true。

希望这能解决问题。

Answer 2

[] 是一个 Python 列表；外层是一个约束列表（代表一个连词），ForAll 中的一个是要绑定的常量列表。

请注意，可以重复使用相同的常量名称。在这种情况下，y == x + 1 中的 y 是一个全局存在，ForAll 中的 y 是一个通用绑定变量，其名称也为 y。