问等价的无量词公式

EN

可以，Z3可以检查两个公式是否等价。检查p和q是否等价。我们必须检查(not (iff p q))是否不可满足。

您的示例使用了非线性算术i*k。Z3中的量词消除模块对非线性实数运算的支持有限。它是基于虚拟术语替换的，这是不完整的。但是，对于您的示例来说，这已经足够了。我们必须启用Z3中的量词消除模块和非线性扩展(即虚拟项替换)。

下面是我们如何在Z3中对示例进行编码：http://rise4fun.com/Z3/rXfi

一般情况下，可以得到消除量词的结果。例如，通过在rise4fun中输入以下内容

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

这种情况涉及非线性算术，并且Z3不会消除量词。