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檢查「可滿足性」而不是「有效性」。 當且僅當否定不可滿足（不滿足）時，公式纔有效。 因此，要證明您的不平等的有效性，您可以將它的否定添加到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的確使用默認的求解器確定不等式不成立。