Z3 无法检查两个公式的等价性

Question

（为什么数学公式显示不正确？）

我正在 Python (Collab) 中对 Z3 库进行测试，看它是否知道区分公式。

测试如下：（1）我对公式 $phi_1$ 进行量词消除，（2）我以保持语义等价的方式更改公式：例如，$phi_1 \equiv (a

要查看 $phi_1=phi_2$，我执行以下查询：对于所有变量，我查看公式是否相互暗示。像 $\forall * 。 (\phi_1 \rightleftarrow \phi_2)$ 这样对吗？

所以，想象一下我在我的机器上应用这个：

x, t1, t2 = Reals('x t1 t2')
g = Goal()
g.add(Exists(x, And(t1 < x, x < t2)))
t = Tactic('qe')
res = t(g)

结果res 是[[Not(0 <= t1 + -1*t2)]]，所以语义上等价的公式是：[[Not(0 <= -1*t2 + t1)]] 我说的对吗？

让我们检查是否[[Not(0 <= t1 + -1*t2)]] = [[Not(0 <= -1*t2 + t1)]]。所以我应用了上面的通用双重蕴涵公式：

w = Goal()
w.add(ForAll(t1, (ForAll(t2, And(
                                  Implies(Not(0 <= -1*t2 + t1), Not(0 <= t1 + -1*t2)),
                                  Implies(Not(0 <= t1 + -1*t2), Not(0 <= -1*t2 + t1)),                   
                        )))))
tt = Tactic('qe')
areThey = tt(w)
print (areThey)

结果是..[[]]我不知道如何解释。一种乐观的方法是认为它返回空，因为量词消除已经能够成功消除两个量词（即具有 true 结果）。

我认为这可能是使用错误策略的问题，或者 Z3 可能无法处理全称量词。

但是，最可能的情况是我可能遗漏了一些关键的东西，而 Z3 足够聪明，可以区分。

有什么帮助吗？

Answer 1

这仅仅意味着量词消除策略将目标减少为空子集；即，它完全消除了它。你无事可做。

一般来说，要检查两个公式在 z3 中是否等价，您可以断言它们的等价是否定；并看看 z3 是否可以提出一个模型：如果否定是可满足的，那么这就是原始等价的反例。如果你得到unsat，那么你得出结论，原始等价对所有输入都成立。这就是你在 z3 中编码的方式：

from z3 import *

t1, t2 = Reals('t1 t2')

s = Solver()
fml1 = Not(0 <= -1*t2 + t1)
fml2 = Not(0 <= t1 + -1*t2)
s.add(Not(fml1 == fml2))
print(s.check())

如果你运行这个，你会看到：

unsat

表示等价成立。