CODEWITHSUNDEEP
z3z3py
Juan Ospina
Juan Ospina

Reputation: 1347

Z3Py is not able to make certain proof?

I am trying to prove that

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

for all n, m reals; using Z3Py online.

I am using the code:

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

and the output is : unknown.

Please can you tell why Z3 does not obtain "sat".

Upvotes: 2

Views: 170

Answers (1)

Nikolaj Bjorner
Nikolaj Bjorner

Reputation: 8359

Note that Z3 checks for "satisfiability" and not "validity". A formula is valid if and only if the negation is not satisfiable (unsat). So to prove validity of your inequality, you can add the negation of it to Z3 and see if it is able to reason about it.

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

It turns out that Z3 does establish that the inequality is unsat using the default Solver.

Upvotes: 2

Related Questions