我有 2 个公式 F1 和 F2。这两个公式共享大多数变量，除了一些具有不同名称的“临时”（或者我称它们为“免费”）变量，这些变量出于某些原因而存在。
现在我想证明 F1 == F2，但是 Z3 的证明（）方法总是考虑到所有的变量。我如何告诉prove() 忽略那些“自由”变量，而只关注我真正关心的变量列表？
我的意思是对于我的变量列表的所有相同输入，如果在输出时，F1 和 F2 具有所有这些变量的相同值（不管“自由”变量的值），那么我认为它们是“等价的”
我相信这个问题已经在其他研究中得到解决，但我不知道在哪里寻找信息。
非常感谢。
我们可以使用存在量词来捕获“临时”/“自由”变量。例如，在以下示例中，公式F和G不等价。
x, y, z, w = Ints('x y z w')
F = And(x >= y, y >= z)
G = And(x > z - 1, w < z)
prove(F == G)
该脚本将生成反例[z = 0, y = -1, x = 0, w = -1]。如果我们将y和w作为“临时”变量，我们可以尝试证明：
prove(Exists([y], F) == Exists([w], G))
现在，Z3 将回归proved。Z3 本质上表明，对于所有x和z，当且仅当存在 a 为真时，存在 ay为真。FwG
这是完整的示例。
备注：当我们添加量词时，我们让 Z3 的问题变得更加困难。它可能会返回unknown包含量词的问题。
显然，我无法发表评论，所以我必须添加另一个答案。“忽略”某些变量的过程通常称为“投影”或“遗忘”。在超出命题逻辑的上下文中我不熟悉它，但如果直接存在量化是可能的（Leo 描述的），它在概念上是最简单的方法。