Z3Py 不能做出一定的证明？

【问题标题】：Z3Py is not able to make certain proof?Z3Py 不能做出一定的证明？
【发布时间】：2013-04-27 19:29:13
【问题描述】：

我试图证明这一点

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"。

【问题讨论】：

标签： z3 z3py

【解决方案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 确定了不等式是不满足的。

【讨论】：