logo标签列表

伊莎贝尔: Sledgehammer 找到了一个证明，但是它失败了。

isabelletheorem-proving
9
经常出现这样的问题，sledgehammer 找到了一个证明，但插入后无法终止。我猜测 sledgehammer 是 Isabelle 中最重要的部分之一，但如果证明失败，它就会变得非常恼人。
在 Sledgehammer 教程 中，有一个关于“为什么 Metis 无法重构证明？”的小章节。
它列出了以下内容：
  1. 尝试使用 isar_proofs 选项获取逐步 Isar 证明，其中每个步骤都由 metis 证明。由于步骤相当小，metis 更有可能重播它们。
  2. 尝试使用 smt 证明方法而不是 metis。它通常更强大，但您需要具备 Z3 以重播证明、信任 SMT 求解器或使用证书。
  3. 尝试使用 blast 或 auto 证明方法，通过 unfolding、using、intro:、elim:、dest: 或 simp: 传递必要的事实，视情况而定。
问题在于第一种选项使证明更冗长，并且需要手动干预。第二个选项很少奏效。
那么第三个选项呢？有没有易于遵循的启发式方法可以应用？ unfolding 和 using 之间有什么区别？此外，在从失败的 metis 证明中使用 intro:、elim: 和 dest: 方面是否有最佳实践？ 部分示例 
proof- 
  have "(det (?lm)) = (det (transpose ?lm))" by (smt det_transpose) 
  then have "(det (?lm)) = [...][not shown]"
    unfolding det_transpose transpose_mat_factor_col by auto
  then show ?thesis [...][not shown]
qed

我希望去掉证明的第一行，因为这行看起来很简单。如果我删掉第一行，sledgehammer 仍然能够找到一个证明，但这个证明会失败（不会终止）。

det_transpose 是什么样子？ - Lars Noschinski
det_transpose 是在 "HOL/Multivariate_Analysis/Determinants.thy" 文件中定义的，这里是引理的粘贴内容：http://pastebin.com/jL9yk2ci - mrsteve
能否提供一个最小工作示例？也就是一个包含完整但小型的 .thy 文件，我可以将其粘贴到我的编辑器中以重现您的问题。 - John Wickerson
3个回答
11
关于你的声明“sledgehammer是Isabelle中最重要的部分之一”： 你从来不需要使用sledgehammer来成功地进行证明。但是当然，sledgehammer非常方便，可以节省很多繁琐的推理。因此，对于那些没有花费许多时间使用它的人来说，它绝对是使Isabelle更易于使用的非常重要的部分（即使对于那些日常证明都更加高效的人来说也是如此）。
针对你的问题：
尝试使用blast或auto证明方法，通过unfolding，using，intro：，elim：，dest：或simp：传递必要的事实。[...]那么这个选项怎么样？是否有任何易于遵循的启发式方法可以应用？
确实有： unfolding：这个方法（递归地）展开等式，与apply（simp only:...）非常相似。启发式方法是，当你用simp：...不得到期望的结果时，尝试改用unfolding ...（可能是由于其他等式干扰所致）。 using：这是用于向当前子目标添加附加假设的方法。启发式方法是，每当一个事实不符合下面的模式之一时，请尝试改用using。
intro：这是用于引入规则的方法，即当满足某些假设时，可以引入某个连接符（或更一般的常量）。例如：A ==> B ==> A & B（其中引入的常量是 (&)）。

elim：用于推理规则，即从某种连接符（或更一般的常量）存在时，可以得出某些事实作为附加假设的形式。
例子：A&B==>(A==>B==>P)==>P(其中常量(&)被消除，而使用A和B作为假设)。注意结论的一般形式(与主前提A&B无关)，这对于不失可证性是重要的(也参见dest:)。

dest：用于破坏规则，即从某个常量存在时，可以直接得出某些事实。
例子：A&B==>B(注意，结论中丢失了A成立的信息，不像elim:的例子)。

simp：用于简化规则，即(条件)方程，始终从左到右应用(因此有时候添加[symmetric]到一个事实中是有用的，以便从右到左应用它，但要注意非终止性，因为这样很容易引入循环推导)。

在说完这些之后，通常是经验让你决定如何最好地在证明中使用给定的事实。当我用sledgehammer得到一个在Isar中太慢的证明时，我通常会检查使用找到的证明所用的事实。然后按照上述方式分类，适当地调用auto，如果这不能完全解决目标，则再次应用sledgehammer(希望这一次提供一个“更容易”的证明)。

7
你问了很多问题，但我会把你的标题和第二段作为你主要投诉的核心，我的回答可以总结为:
  • Sledgehammer是三种武器之一,
  • 通过不断试验和错误来提高经验是启发式的,
  • 不使用Sledgehammer返回的大量证明是使用Sledgehammer的重要部分，
  • minimize和preplay_timeout选项可以通过自动播放证明来节省时间和烦恼，这样可以给出时间信息，并有时显示找到的证明将失败。

从第二段开始，你说:

我经常遇到一个问题，就是Sledgehammer找到了一个证明。但是当我尝试使用它时，证明没有终止。我想Sledgehammer是Isabelle中最重要的部分之一，...

Sledgehammer很重要，但我认为它是三种武器之一，其中三个部分分别是:

  1. 使用自然推导的详细证明步骤。
  2. 自动证明方法，如auto, simp, rule等。其中一个重要的部分是创建自己的simp重写规则，并学习使用定理与rule和其他自动证明方法。
  3. 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的帖子，提供了更详细的信息。

1
我可以回答您的子问题“unfolding和using有什么区别？”。大致上来说，它的工作原理是这样的。
假设引理foo的形式为x = a+b+c。如果您写成：
unfolding foo

在你的证明中，所有出现的 x 都将被替换为 a+b+c。另一方面，如果你写成：
using foo

那么x=a+b+c将被添加到您的假设列表中。

网页内容由stack overflow 提供, 点击上面的
可以查看英文原文，
原文链接