为什么在Leon Online的PropositionalLogic示例中wrongCommutative超时？

Question

我对里昂的PropositionalLogic示例中的wrongCommutative属性非常好奇。

这对我来说似乎是一个正确的属性，我不明白为什么它只是在里昂超时。

这是链接：https://leon.epfl.ch#link/37040293ff5ff92c763f797f22f142f8-1

有人能帮我吗？

Answer 1

你是对的，这是成立的，谢谢你的观察！里昂没有开箱即用地证明这一点，因为它需要一些帮助。它最初是错误的，但我们更改了代码，以便该属性适用于这些函数的当前版本。

您的"Leon稳定“链接现在似乎指向另一个文件(由于leon.epfl.ch的更改和重启)，但该示例仍然可以从web and here is the stable github link上的示例列表中找到，以避免任何混淆。

了解原因

nnf(simplify(f)) == simplify(nnf(f)) 

对于该实现，您可以观察到

simplify(nnf(f)) = nnf(f)

这个引理成立就证明了这一点：

@induct
def nnfIsSimplified(f: Formula): Boolean = {
  require(isNNF(f))
  simplify(f) == f
} holds

事实上，nnf(simplify(f))==nnf(f)可以通过归纳来表示，但在这里，里昂可能需要一些提示。

有关此属性的完整证明，请参阅the updated example on Github。