9

很多时候我遇到的问题是sledgehammer找到一个证明，但是当我插入它时，它并没有终止。我想sledgehammer这是 Isabelle 最重要的部分之一，但如果证明失败，它会变得很烦人。

在Sledgehammer 教程中，有一个小章节是“为什么 Metis 无法重构证明？”。

它列出：

  1. 尝试isar_proofs获取逐步 Isar 证明的选项，其中每一步都由metis. 由于步骤相当小， metis因此更有可能重播它们。
  2. 尝试smt证明方法而不是metis. 它通常更强大，但您需要有 Z3 可用于重放证明、信任 SMT 求解器或使用证书。
  3. 尝试blastor autoproof 方法，根据需要通过unfolding, using, intro:, elim:, dest:, 或传递必要的事实simp:。

问题是第一个选项使证明更加冗长，并且还涉及人工干预。第二个选项很少奏效。

那么第三个选项呢。我可以应用任何易于遵循的启发式方法吗？

unfolding和有什么区别using？还有关于如何使用intro:,elim:和dest:来自失败metis证明的最佳实践吗？

部分示例

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仍然会找到一个证明，但是这个找到的证明失败（不会终止）。

4

3 回答 3

12

关于你的陈述，大锤是伊莎贝尔最重要的部分之一：你永远不需要大锤来成功证明。但是当然大锤很方便，可以省去很多繁琐的推理。因此，对于那些没有花很多年使用它的人来说，它绝对是让 Isabelle 更有用的一个非常重要的部分（甚至对于那些大锤使日常证明更有效率）。

来回答你的问题

尝试blastor autoproof 方法，根据需要通过unfolding, using, intro:, elim:, dest:, 或传递必要的事实simp:。
[...]
那么 [this] 选项呢。我可以应用任何易于遵循的启发式方法吗？

确实有：

unfolding：这（递归地）展开方程，即，它与 非常相似apply (simp only: ...)。simp: ...启发式方法是，当您使用try没有得到预期结果时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再次应用（希望这次提供“更简单”的证明）。

于 2013-06-20T02:06:23.613 回答
5

你问了很多问题，但我会把你的标题和第二段作为你主要抱怨的本质，我最终给出了一个冗长的答案，可以总结为，

  • 大锤是三管齐下的武器库的一部分，
  • 你变得更有经验，不断的实验，伴随着试错是启发式的，
  • 不使用 Sledgehammer 返回的许多证明是使用 Sledgehammer 的重要组成部分，并且
  • 和选项可以通过自动回放证明来节省您一些时间和挫败感，这会为您提供时间信息，有时会显示找到的证明将失败minimize。preplay_timeout

从你的第二段开始，你说：

我经常遇到大锤找到证据的问题。但是后来我尝试了一下，但证明并没有终止。我猜大锤是伊莎贝尔最重要的部分之一，...

大锤很重要，但我认为它是三管齐下的武器库的一部分，其中三个部分是：

  1. 使用自然演绎的详细证明步骤。
  2. 自动证明方法，例如auto、simp、rule等。其中很大一部分将是创建自己的simp重写规则，并学习将定理与rule无数其他自动证明方法一起使用。
  3. 大锤调用自动定理证明器 (ATP)。使用第 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 毫秒或更短的证明，那么我认为这是一个很好的证明，但我仍然尝试使用tryisar-ref.pdf 第 208 页第 9.4.4 节的自动证明方法。很多时候，我可以在 5 毫秒或更短的时间内得到一个证明。
  • 总时间超过 100 毫秒的metis证明，我愿意工作 30 分钟或更长时间来尝试获得更快的证明。
  • 一个metis200 毫秒到 500 毫秒的证明，我将尽我所能尝试将其降低到 100 毫秒以下，这在很多时候意味着转换为详细的证明。
  • Asmt或metis大于 1 秒的证明我只认为好的作为临时证明。
  • 输出面板中 Sledgehammer 报告的大于 3 秒的证明，我通常什至不尝试，因为即使它最终起作用，我也必须努力寻找另一个证明，所以我会宁愿花时间在前面试图找到一个好的证据。

选项 3 启发式

你说，

那么第三个选项呢。我可以应用任何易于遵循的启发式方法吗？

启发式是：

  • “作为适当的”，

也就是说，启发式是“将大锤用作三管齐下的武器库的一部分”。

启发式方法也是“阅读大量教程和文档，以便您可以在 Sledgehammer 中使用很多其他东西”。Sledgehammer 很强大，但不是无限强大，对于某些定理，您可以使用自己的simp规则在 0ms 内证明apply(simp)Sledgehammerapply(auto)永远不会证明的内容。

对我自己来说，我有大约 150 到 200 个定理，所以“适当”对我来说比以前更有意义。基本上，您尝试按照需要设置的方式设置 Sledgehammer。

Sledgehammer 需要设置的方式有时意味着运行auto或simp首先，但有时不是，因为多次运行auto或simp将注定 Sledgehammer 失败。

但有时，您甚至不需要metisSledgehammer 的证明，除非作为初步证明，直到您找到更好的证明，对我而言，这通常意味着使用自动证明方法进行更快的证明。

我不是 Sledgehammer 的权威，但 Sledgehammer 似乎擅长匹配旧定理的假设和结论，并将假设和结论用于新定理。它不擅长的是证明我通过使用simpand大大扩展的公式auto。

我继续以 Sledgehammer 为中心的冗长启发式：

  • 使用 Sledgehammer 通过用 Sledgehammer 证明一些您不知道如何证明的定理来启动证明过程。
  • 如 tutorial.pdf 第 9 章所述，将您的等价定理转化为simp重写规则，以便与 、 、 等自动证明方法一起simp使用auto。fastforce
  • 将您的一些定理用于与intro和一起使用的条件重写规则rule。
  • 最后两个步骤用于完全解决证明步骤或用于“酌情”设置 Sledgehammer。大锤永远不会停止有用，无论你知道多少，当你知道的不多时它非常有用，但只有大锤并不是通往成功的道路。
  • 如果 Sledgehammer 无法证明某个定理，则求助于详细证明，从简单的详细证明开始。有时，当 Sledgehammer 无法证明 if-and-only-if 时，将 if-and-only-if 分解为两个条件可以让 Sledgehammer 轻松证明这两个条件。
  • 在你证明了很多东西之后，回去优化你的证明。有时，使用您创建的所有重写规则，simp并且auto会神奇地证明事情，并且您会摆脱metisSledgehammer 为您找到的一些证明。有时，您会使用 Sledgehammer 找到metis更快的证明。

使用此命令优化时序：

ML_command "Toplevel.timing := true"

还有另一个 SO 帖子提供了更多详细信息。

于 2013-06-19T22:10:03.597 回答
1

unfolding我可以回答您的子问题“和之间有什么区别using？”。粗略地说，它是这样工作的。

假设引理foo的形式是x = a+b+c。如果你写

unfolding foo

在您的证明中，所有出现的x都将替换为a+b+c. 另一方面，如果你写

using foo

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

于 2013-06-19T06:43:50.913 回答