Z3 有一个prove()方法，可以证明两个公式的等价性。
但是，我找不到这种prove()方法的技术文档。prove()幕后使用的“等效”定义是什么？那是“部分等价”（在“回归验证”论文中提出），还是更强大的东西？
提醒一下，“部分等价”保证两个公式是等价的，如果给定相同的输入，它们会产生相同的输出。
问问题
295 次
1 回答
4
在“回归验证”中，我们正在检查程序的新版本是否产生与早期版本相同的输出。也就是说，它是一种检查程序等价性的方法。在这种方法中，使用了诸如 Z3 之类的定理证明器（SMT 求解器）。话虽如此，我们不应该将程序等价与一阶逻辑中的公式等价混淆。Z3 处理一阶逻辑公式。一阶逻辑具有明确定义的语义。一个关键概念是可满足性。例如，公式p or q是可满足的，因为我们可以通过将por赋值为 true 来使其q为真。另一方面，p and (not p)是不能满足的。我们可以在Z3教程的这一部分。
Z3 API 提供了检查一阶公式可满足性的过程。Z3 Python 接口有一个prove过程。它通过证明它的否定是不可满足的来表明一个公式是有效的。这是一个建立在 Z3 API 之上的简单函数。这是其文档的链接。文档是从代码中的 PyDoc 注释自动生成的。
请注意，prove(F)检查公式F是否有效。因此，我们可以用一阶公式来prove(F == G)尝试证明两个公式是等价的。也就是说，我们基本上表明这是一个有效的公式。FGF iff G
于 2012-12-26T17:12:28.010 回答