theorem-proving - 在 Isabelle 中一起调用 Nitpick 和 Sledgehammer

Question

当我在Isabelle中陈述引理时，我经常输入nitpick，如果这没有给我一个反例。然后我键入sledgehammer以尝试自动查找证明。

我想知道：是否可以调用Nitpick和Sledgehammer以便它们同时运行？既然Sledgehammer已经将我的引理发送给了一堆自动证明者，那么这些证明者中的一个难道不能成为像Nitpick这样的反例发现者吗？

Answer 1

您可以尝试使用tryIsabelle 中的命令；它并行运行sledgehammer、nitpick和quickcheck许多其他求解器（例如auto、simp、force等），为您提供第一个完成的求解器的结果。

例如，运行以下命令：

lemma "(a * (b + 1)) = (a * b + a)"
  try

将从 中返回一个反例nitpick，表明该定理一般不成立。添加类型约束：

lemma "((a :: nat) * (b + 1)) = (a * b + a)"
  try

现在将返回一条消息，告诉您simp能够解决目标。

最后，将类型约束更改为更具挑战性的32 word类型（可从Wordin 获得HOL-Word）：

lemma "((a :: 32 word) * (b + 1)) = (a * b + a)"
  try

将从大锤返回一个结果。