Sledgehammer: Judgement Day http://www4.in.tum.de/~boehmes/judgement/judgement.pdf ずいぶん昔に見かけて「タイトルが中二病www」と思ってた論文。 対話的定理証明系のIsabelleの中で一部の証明を自動定理証明器を呼び出して自動化する Sledgehammer の、色々な問題セットや自動定理証明器での定量的な評価。 対話的定理証明系から自動定理証明器を利用するのは意外と straight forward な話では済まないんだなあというのが分かって面白かった。
意外だったのは、自動定理証明器の出力した証明をそのまま用いるのではなく、自動定理証明器の出力した証明中で用いられていた前提を元に再度 Metis という専用の自動定理証明器を用いて、証明を再構成している点。 これは幾つかの技術的な理由と、あと長大な導出原理の繰り返しによる可読性の低い証明ではなく、自然演繹による可読性の高い証明が欲しいという理由。
また、うまくいかない場合として、タイムアウトなどを除くと、自動定理証明器に渡す時点で証明不能になってしまっている場合と、逆に自動定理証明器が証明に成功しても、それをIsabelleの証明に出来ない場合がある。前者は、Isabelleレベルでの前提の集合のうち、帰納法などの一階述語論理では有限公理化できない（述語毎に無限個のインスタンスが必要になる）場合や、そうでなくても無条件に全部入れてしまうと自動定理証明器が組み合わせ爆発するので、関連する前提をヒューリスティックに選んでいるため。後者は unsorted な一階述語論理にエンコードする際に、型情報を全部エンコードすると問題が複雑になり過ぎて自動定理証明器が失敗することが多いので、あえて型情報を全てはエンコードしないunsoundなエンコードを採用しているため。 unsoundなエンコードであっても、外部の自動定理証明器やMetisの発見する証明がたまたまunsoundnessをexploitしないものになっていれば問題ないわけで、そのほうが成功の可能性が高いという判断。
そういえば、Agda1 にもFOLプラグインとかがあったが、やはり同じような苦労があったのだろうか?
あと、自動定理証明器で発見した前提の最小化について、二分探索的なアルゴリズムよりも線形探索の方が速かったという話。 ありがちな話ではあるけど、ちょっとアルゴリズムが気になった。 [1] のらしいが、要はMUSの計算なのでQuickXplainとかみたいな感じなのかな?
[1] A. Bradley and Z. Manna. Property-directed incremental invariant generation. Formal Asp. Comput., 20:379–405, 2008.