1

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

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

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

谁能帮我这个？

4

1 回答 1

2

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

您的“Leon stable”链接现在似乎指向另一个文件（由于 leon.epfl.ch 的更改和重新启动），但该示例仍然可以从网络上的示例列表中获得，这里是 stable github 链接，避免任何混淆。

看看为什么

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)可以通过归纳来证明这一事实，但在这里 Leon 可能也需要一些提示。

有关Leon 的证明 DSL 中表达的此属性的完整证明，请参阅Github 上的更新示例。

于 2016-03-18T08:18:55.510 回答