你问了很多问题,但我会把你的标题和第二段作为你主要投诉的核心,我的回答可以总结为:
- Sledgehammer是三种武器之一,
- 通过不断试验和错误来提高经验是启发式的,
- 不使用Sledgehammer返回的大量证明是使用Sledgehammer的重要部分,
minimize
和preplay_timeout
选项可以通过自动播放证明来节省时间和烦恼,这样可以给出时间信息,并有时显示找到的证明将失败。
从第二段开始,你说:
我经常遇到一个问题,就是Sledgehammer找到了一个证明。但是当我尝试使用它时,证明没有终止。我想Sledgehammer是Isabelle中最重要的部分之一,...
Sledgehammer很重要,但我认为它是三种武器之一,其中三个部分分别是:
- 使用自然推导的详细证明步骤。
- 自动证明方法,如
auto
, simp
, rule
等。其中一个重要的部分是创建自己的simp
重写规则,并学习使用定理与rule
和其他自动证明方法。
- Sledgehammer调用自动定理证明器(ATPs)。使用步骤1和2,结合经验来设置Sledgehammer。经验很重要。你可能使用
auto
简化事情,使Sledgehammer成功,但你可能不使用auto
,因为它会将公式展开到Sledgehammer无法成功的程度。
...但如果一个证明失败了,那就很烦人。
所以,在这里,你对Sledgehammer的期望和我的期望不同。现在,如果我感到恼火,那是因为我需要花费超过30秒的时间来证明一个定理。如果我对特定的Sledgehammer证明失败感到非常失望,那是因为我已经尝试了几个小时或几天都没有成功。
使用Sledgehammer不是为了找到证明,而是为了找到好的证明
自动化有时可以缓解挫折感。点击Sledgehammer证明,只发现它失败了,会令人沮丧。以下是我目前使用Sledgehammer的方式,除非我开始渴望一个证明:
sledgehammer_params[minimize=smart,preplay_timeout=10,timeout=60,verbose=true,
max_relevant=smart,provers="
remote_vampire metis remote_satallax z3_tptp remote_e
remote_e_tofof spass remote_e_sine e z3 yices
"]
选项
minimize=smart
和
preplay_timeout=10
与Sledgehammer在找到证明后播放证明有关。不使用Sledgehammer找到的许多证明是使用Sledgehammer的重要部分,而证明回放是筛选证明的重要部分。
对于我自己来说,我不太处理不终止的Sledgehammer证明,但这可能是因为我一开始就进行了选择。
我对Sledgehammer证明的第一个标准是它必须相当快,所以当Sledgehammer报告它找到了一个超过3秒的证明时,除非我迫切想知道一个定理是否可以被证明,否则我不会尝试使用它。
对于我来说,使用Sledgehammer通常是这样的:
- 陈述一个定理并看看我是否能运气好。
- 如果Sledgehammer给我一个30毫秒或更短的证明,那么我认为那是一个好的证明,但我仍然会尝试使用
try
和isar-ref.pdf第9.4.4节208页的自动证明方法进行实验。很多时候我可以把证明缩短到5ms或更短。
- 总时间超过100ms的
metis
证明,我愿意花费30分钟或更长时间来尝试获得更快的证明。
- 200ms到500ms的
metis
证明,我会尽我所知尝试将其缩短到100ms以下,这往往意味着转换为详细的证明。
- 大于1秒的
smt
或metis
证明,我只认为是临时证明。
- Sledgehammer在输出面板中报告超过3秒的证明,我通常甚至不会尝试,因为即使它最终起作用,我仍然必须努力找到另一个证明,所以我宁愿在前期花时间寻找一个好的证明。
选项3的启发式
你说:
那么第三个选项呢?有没有易于遵循的启发式可以应用?
启发式是:
也就是说,启发式是"使用Sledgehammer作为三管齐下的武器之一"。
启发式还是"阅读许多教程和文档,以便您拥有许多其他可与Sledgehammer一起使用的东西"。Sledgehammer很强大,但并非无限强大,对于某些定理,您可以使用自己的
simp
规则,通过
apply(simp)
或
apply(auto)
证明Sledgehammer永远无法证明。
对于我自己,我已经证明了大约150到200个定理,因此“视情况而定”对我来说有更多的含义。基本上,你尝试按照Sledgehammer需要的方式设置Sledgehammer。
Sledgehammer需要的设置有时意味着首先运行auto或simp,但有时不需要,因为很多时候运行auto或simp会导致Sledgehammer失败。
但有时,你甚至不需要从Sledgehammer获得metis证明,除非作为一种初步证明,直到你找到更好的证明为止,对我来说,通常是使用自动证明方法进行更快的证明。
我不是Sledgehammer的权威,但它似乎擅长匹配旧定理中的假设和结论与新定理中使用的假设和结论。它擅长证明公式,但不能够证明我通过使用simp和auto大大扩展的公式。
我继续遵循以Sledgehammer为中心的冗长启发式法则:
- 使用Sledgehammer启动证明过程,通过使用Sledgehammer证明一些你不知道如何证明的定理。
- 将等式的定理转换为simp重写规则,用于自动证明方法,例如simp、auto、fastforce等,如tutorial.pdf第9章所述。
- 对于使用intro和rule的条件重写规则,使用一些你的定理。
- 最后两步用于完全解决证明步骤或根据需要设���Sledgehammer。无论你知道多少,Sledgehammer都不会停止有用,当你不知道很多时,它非常有用,但仅使用Sledgehammer并不是成功的道路。
- 如果Sledgehammer不能证明一个定理,那么就诉诸详细的证明,从一个裸体的详细证明开始。有时,将一个if-and-only-if分成两个条件可以让Sledgehammer轻松地证明这两个条件,而无法证明if-and-only-if。
- 在证明了大量东西之后,回过头来优化你的证明。有时,通过所有你创建的重写规则,simp和auto会神奇地证明事情,并且你将摆脱一些Sledgehammer为你找到的metis证明。有时,你将使用Sledgehammer找到更快的metis证明。
- 使用此命令来优化时间:
ML_command "Toplevel.timing := true"
这里有另一篇Stack Overflow的帖子,提供了更详细的信息。
.thy
文件,我可以将其粘贴到我的编辑器中以重现您的问题。 - John Wickerson