isabelle - 如何管理所有各种证明方法

Isabelle的用户在尝试证明auto或sledgehammer无法立即证明的内容时，是否遵循“通用”非正式算法？如果auto需要由用户制定的其他引理才能成功，或者是否使用更好的其他证明方法，这是一种通常的计算方法。

一个相关的问题是:是否可能在所有证明方法以及应用它们的上下文中找到一个表？当我阅读Programming and Proving tutorial时，各种方法(分别是某些方法的变体，例如auto的许多变体)的描述分散在文本中，这使我不断地在文本和Isabelle代码之间回溯(还会导致忘记将什么准确地用于什么)，从而导致工作流程效率非常低下。

最佳答案

不，没有“通用”非正式方式。您可以使用try0尝试所有标准的证明方法(例如auto，blast，fastforce，...)和/或更高级的sledgehammer。

之后，有趣的部分开始。

可以用更简单的辅助引理来显示该定理吗？您可以使用命令“对不起”来假设引理为真。

我将如何在纸上证明这一点？然后尝试在Isabelle中做此证明。

寻求帮助:)很多人在堆栈溢出，freenode上的#isabelle和Isabelle邮件列表正在等待您的问题。

关于第二个问题:不，没有这样的概述。也许有人应该写一个，但是如前所述，您可以简单地使用try0。

关于isabelle - 如何管理所有各种证明方法，我们在Stack Overflow上找到一个类似的问题：https://stackoverflow.com/questions/42327026/