Z3 中量词的交替？

Question

使用 z3py API。 Reading from advanced examples 每个例子外面都有一个全称量词。想使用量词交替。

例如：

for_all X exists Y

我认为有用的一个实例是（对于所有图形都存在一个函数...）。我可以在 Z3py 中实现吗？如果没有，我该怎么办？谢谢。

Answer 1

Z3/Python确实可以做到这一点。但请记住，当出现量词时，逻辑变得半可判定：也就是说，Z3 可能会也可能不会回答您的查询。（它不会告诉你任何错误，但可能无法解决查询。）

这是一个来自算术一阶逻辑的例子，它很简单，但希望它能说明语法：

 (∀x∃y.f(x,y)) → (∀x∃v∃y.(y ≤ v ∧ f(x,y)))

这里是你如何在 Z3 中编写代码，假设 f 是一个函数符号，它接受两个整数和 returns 一个布尔值：

from z3 import *

f = Function('f', IntSort(), IntSort(), BoolSort())
x, y, v = Ints('x y v')

lhs = ForAll(x, Exists(y, f(x, y)))
rhs = ForAll(x, Exists([v, y], And(y <= v, f (x, y))))
thm = Implies(lhs, rhs)

print thm

solve(Not(thm))

请注意，在最后一行中，我们要求 Z3 solve 否定我们的定理：Z3 检查可满足性；所以如果它说 unsat 来否定我们的定理，那么我们就会知道我们有一个证明。

这是我得到的输出：

Implies(ForAll(x, Exists(y, f(x, y))),
        ForAll(x, Exists([v, y], And(y <= v, f(x, y)))))
no solution

因此，在这种情况下，Z3 能够建立定理。

然而，根据您的问题，如果事实证明 Z3 由于不完整而无法确定有效性，您也可能会得到 "unknown" 作为答案。

Z3 中量词的交替？

Alternation of quantifiers in Z3?

quantifiers

z3

z3py