Equivalent Quantifier Free Formulas

问题:

I want to know if Z3 can show equivalent formulas after Quantifier Elimination.

Example (exists k) (i x k) = 1 and k > 5 is equivalent to

i > 0 and 5 i - 1 < 0.

Here, quantifier k has been eliminated.

Is this possible?

Thanks, Kaustubh.

回答1:

Yes, Z3 can check whether two formulas are equivalent. To check whether p and q are equivalent. We must check whether (not (iff p q)) is unsatisfiable.

Your example uses nonlinear arithmetic i*k. The quantifier elimination module in Z3 has limited support for nonlinear real arithmetic. It is based on virtual term substitution, which is not complete. However, it is sufficient for your example. We must enable the quantifier elimination module in Z3, and the nonlinear extensions (i.e., virtual term substitution).

Here is how we can encode your example in Z3: http://rise4fun.com/Z3/rXfi

回答2:

In general, the result of eliminating quantifiers can be obtained. For instance by entering the following into rise4fun:

(declare-const i Real)
(assert (exists ((k Real)) (and (= (* i k) 1.0) (> k 5.0))))
(apply qe)

This case involves non-linear arithmetic, and Z3 does not eliminate the quantifier.