z3 - Z3Py 不能做出一定的证明？

Question

我试图证明

4*n^3*m+4*n*m^3 <= n^4+6*n^2*m^2+m^4

为所有n，m实数；在线使用 Z3Py。

我正在使用代码：

n, m = Reals('n m')

s = Solver()

s.add(ForAll([n, m], n**4+6*n**2*m**2+m**4 >= 4*n**3*m+4*n*m**3))

print s.check()

输出是： unknown。

请你告诉为什么Z3没有获得 "sat"。

Answer 1

请注意，Z3 检查“可满足性”而不是“有效性”。当且仅当否定不可满足（unsat）时，公式才有效。因此，为了证明你的不等式的有效性，你可以将它的否定添加到 Z3 中，看看它是否能够推理它。

n, m = Reals('n m')

s = Solver()

s.add(Not(n**4+6*n**2*m**2+m**4 >= 4*n**3*m+4*n*m**3))

print s.check()

事实证明，Z3 确实使用默认的 Solver 确定了不等式是不满足的。