我正在努力理解这个例子:
solve([y == x + 1, ForAll([y], Implies(y <= 0, x < y))])
但是看了解释后我还是不明白。
你怎么看这个?[]是什么意思?
我的错误解释是。已知定理y == x + 1。是否对所有y都成立，这样就意味着(y <= 0, x <y)>
你对如何理解这个话题有什么建议吗?
看起来这里有几个混淆。让我们首先整理绑定:在量词上下文中，变量是独立的，也就是说，它可以在不改变语义的情况下重命名。那么，你原来的:
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))])
注意，我们在"作用域"中替换了y;从ForAll到z，但保留第一个连接词的一个不变。只能在ForAll(或Exist)范围内重命名，不能在CC_7范围外重命名。
这两个等价表达式都是不满足的。为什么?第一个连词很容易满足;只要任意选择一个x，并将y设置为x+1，就完成了。第二个连词是不令人满意的。因为，无论您选择哪个x来满足第一个条件，您总能找到一个小于x的z(只需选择min(0, x-1))，并且对于该赋值，量化公式变为False。因此没有解决方案。
现在，让我们考虑一下您在评论中的变体，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，只要z <= 0，因此其含义总是正确的。这就是z3告诉你的，当它给你满意的赋值
[x = 2, y = 3]
注意在这个赋值中没有关于变量y = 00。你不能给出一个普遍量化公式的模型;根据定义，为true
希望这能澄清一切。
[]是一个Python列表;外面的一个是约束列表(表示连接)，ForAll中的一个是要绑定的常量列表。
注意，相同的常量名可以重复使用。在这种情况下，y == x + 1中的y是一个全局存在变量，ForAll中的y是一个通用绑定变量，名称也为y。