问题描述
我想知道Z3是否可以在量词消除后显示等效公式.
I want to know if Z3 can show equivalent formulas after Quantifier Elimination.
示例(存在 k)(i x k) = 1 且 k > 5相当于
Example (exists k) (i x k) = 1 and k > 5is equivalent to
i > 0 和 5 i - 1
i > 0 and 5 i - 1 < 0.
这里，量词 k 已被删除.
Here, quantifier k has been eliminated.
这可能吗?
谢谢，考斯图布.
推荐答案
是的，Z3 可以检查两个公式是否等价.检查 p 和 q 是否等价.我们必须检查 (not (iff p q)) 是否不可满足.
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.
您的示例使用非线性算术i*k.Z3 中的量词消除模块对非线性real 算法的支持有限.它基于虚拟术语替换，这是不完整的.但是，对于您的示例来说已经足够了.我们必须在 Z3 中启用量词消除模块，以及非线性扩展(即虚拟项替换).
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).
以下是我们如何在 Z3 中对您的示例进行编码:http://rise4fun.com/Z3/rXfi
Here is how we can encode your example in Z3: http://rise4fun.com/Z3/rXfi
这篇关于等效量词免费公式的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持！