Z3无法证明相等关系传递性等价表达式问题咨询

为什么会生成反例 #

你当前的代码试图证明两个合取表达式逻辑等价，但你实际的需求是验证相等关系的传递性，二者并不匹配：

• 你给出的等价式左右两边在逻辑上本身是等值的，你拿到的反例[c=1, b=0, a=0]代入代码计算时，左右两边结果都为False，等值判断结果为True，并不构成有效反例，大概率是你书写待验证表达式时出现了笔误（比如漏写了右侧的某个合取项，或者错误把传递性的蕴含逻辑写成了等价逻辑）。
• 如果你原本想写的是证明((a == b) and (b == c)) == (a == c)，这个命题本身就不成立：当a=1, b=2, c=1时，左边计算结果为False，右边计算结果为True，自然会返回反例。

正确的验证写法 #

相等关系的传递性是蕴含关系，而非等价关系：只要满足a==b且b==c，就一定能推出a==c，不需要反向成立。正确的验证代码如下：

from z3 import *
a = Int("a")
b = Int("b")
c = Int("c")
# 用Implies表示蕴含关系
prove(Implies(And(a == b, b == c), a == c))

运行上述代码会输出proved，符合预期。

内容的提问来源于stack exchange，提问作者Daniil Iaitskov