Z3中量词的交替?

Question

using z3py API.从高级示例中读取 每个示例都有一个通用量词。想使用量词交替。

例如：

for_all X 存在 Y

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

Answer 1

这在 Z3/Python 中确实是可能的。但请记住，当存在量词时，逻辑变得半可判定：也就是说，Z3 可能无法回答您的查询。(它不会告诉您任何错误，但可能无法解决查询。

这是算术一阶逻辑的一个例子，它微不足道，但希望它能说明语法：

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

以下是在 Z3 中编写代码的方法，假设f是一个函数符号，它接受两个整数并返回一个布尔值：

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))

请注意，在最后一行中，我们要求 Z3solve定理的否定：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 由于不完整而无法确定有效性，您也可能获得"未知"作为答案。