CODEWITHSUNDEEP
z3z3pyquantifiers
user2754673
user2754673

Reputation: 459

Alternation of quantifiers in Z3?

using z3py API. Reading from advanced examples Every example has a universal quantifier outside. Would like to use quantifier alternation.

For example:

for_all X exists Y

One instance that I think it's useful is (for all graphs exists a function...). Can I achieve it in Z3py? If not, what should I do? Thanks.

Upvotes: 2

Views: 627

Answers (1)

alias
alias

Reputation: 30418

This is indeed possible with Z3/Python. But keep in mind that when quantifiers are present the logic becomes semi-decidable: That is, Z3 may or may not be able to answer your queries. (It won't tell you anything wrong, but might fail to solve the query.)

Here's an example from first order logic of arithmetic, it's trivial, but hopefully it illustrates the syntax:

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

Here's how you can code that in Z3, assuming f is a function symbol that takes two integers and returns a boolean:

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

Note that in the final line we ask Z3 to solve the negation of our theorem: Z3 checks for satisfiability; so if it says unsat for the negation of our theorem, then we will know that we have a proof.

This is the output I get:

Implies(ForAll(x, Exists(y, f(x, y))),
        ForAll(x, Exists([v, y], And(y <= v, f(x, y)))))
no solution

So, in this case Z3 was able to establish theoremhood.

Depending on your problem, however, you may also get "unknown" as the answer, if it turns out that Z3 cannot decide the validity due to incompleteness.

Upvotes: 3

Related Questions