9

多くの場合sledgehammer、証明を見つけるという問題が発生しますが、それを挿入しても終了しません。sledgehammerIsabelle の最も重要な部分の 1 つだと思いますが、証明が失敗すると面倒になります。

Sledgehammerのチュートリアルには、「なぜ Metis は証明の再構築に失敗するのか?」という小さな章があります。

それはリストします：

  1. isar_proofs各ステップが によって正当化される段階的な Isar 証明を取得するオプションを試してくださいmetis。ステップはかなり小さいので、 metis再生できる可能性が高くなります。
  2. smtの代わりに証明方法を試してくださいmetis。通常はより強力ですが、証明を再生するために Z3 を使用できるようにするか、SMT ソルバーを信頼するか、証明書を使用する必要があります。
  3. 、 、 、 、 、 、 、 、 、 、 、 、 、 、 、 、 、 、 、 、 、 、 、 、 、 、 、 、 、 、 、 、 、 、 、 、 、 、 、 、 、 、 、 、 、 、 、 、、、、 、を介して、必要な事実を渡しながら、blastまたは証明メソッドを試してください。autounfoldingusingintro:elim:dest:simp:

問題は、最初のオプションでは証明がより冗長になり、手動の介入が必要になることです。2 番目のオプションはほとんど機能しません。

では、3 番目のオプションはどうでしょうか。適用できる簡単なヒューリスティックはありますか?

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 の最も重要な部分の 1 つです。証明で成功するために大ハンマーは必要ありません。もちろん、スレッジハンマーは非常に便利で、面倒な推論を大幅に省くことができます。したがって、Isabelle を何年も使用していなかった人々にとって、Isabelle をより使いやすくするための非常に重要な部分であることは間違いありません。

あなたの質問に来ます

、 、 、 、 、 、 、 、 、 、 、 、 、 、 、 、 、 、 、 、 、 、 、 、 、 、 、 、 、 、 、 、 、 、 、 、 、 、 、 、 、 、 、 、 、 、 、 、、 、、 、を介して必要な事実を渡し、blastまたは証明メソッドを試してください。 [...] では、[この] オプションはどうでしょうか。適用できる簡単なヒューリスティックはありますか?autounfoldingusingintro:elim:dest:simp:

実際には次のようなものがあります:

unfolding: これは (再帰的に)方程式を展開します。つまり、 と非常によく似ていapply (simp only: ...)ます。ヒューリスティックとは、代わりにsimp: ...tryを使用しても期待される結果が得られないunfolding ...場合です (他の方程式が干渉している可能性があります)。

using: これは、現在のサブゴールに追加の仮定を追加するために使用されます。ヒューリスティックは、ファクトが以下のパターンのいずれにも当てはまらない場合は常に、using代わりに試行することです。

intro:: これは導入ルールに使用されます。つまり、特定の仮定が満たされるたびに、何らかの接続詞 (またはより一般的には定数) が導入される可能性があるという形式です。
例: A ==> B ==> A & B (導入された定数は(&))。

elim:: これは消去規則に使用されます。つまり、特定の接続詞 (またはより一般的には定数) の存在から、いくつかの事実が追加の仮定として結論付けられる可能性があるという形式のものです。
例: (ここで、明示的にandを仮定することを優先しA & B ==> (A ==> B ==> P) ==> Pて、定数(&)が削除されます)。結論の一般的な形式 (大前提 とは関係ありません) に注意してください。これは、証明可能性を失わないために重要です ( も参照)。ABA & Bdest:

dest:: これは、破壊規則に使用されます。つまり、特定の定数の存在から、いくつかの事実が直接結論付けられる形式のものです。
例: (保持されている情報は、例とは異なり、結論で失われるA & B ==> Bことに注意してください。)Aelim:

simp:: これは単純化ルール、つまり (条件付き) 方程式に使用され、常に左から右に適用されます (したがって、[symmetric]右から左に適用するためにファクトに追加すると便利な場合がありますが、終了しないことに注意してください。この方法でループ派生を導入するのは簡単だからです)。

そうは言っても、多くの場合、与えられた事実を証明内で使用するのに最適な方法を決定できるのは単なる経験です. sledgehammerIsar で遅すぎる証明を取得したときに私が通常行うことは、見つかった証明で使用されている事実を調べることです。次に、それらを上記のように分類し、auto適切に呼び出し、それで目標が完全に解決されなかった場合は、sledgehammerもう一度適用します (今回は「より簡単な」証明を提供できれば幸いです)。

于 2013-06-20T02:06:23.613 に答える
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 に答える