Lemmas: Generation, Selection, Application

要約

補題は数学の重要な特徴であることに注意して、自動化された定理証明における補題の役割の調査に取り組みます。
この論文では、自動化された定理証明者にとって有用な補題を生成する学習技術を含む複合システムを使用した実験について説明し、いくつかの代表的なシステムの改善を示し、20 年間どのシステムでも解決されなかった困難な問題を解決しました。
凝縮された分離問題に焦点を当てることで、設定を大幅に簡素化し、補題の本質と証明探索におけるそれらの役割を理解できるようにします。

要約(オリジナル)

Noting that lemmas are a key feature of mathematics, we engage in an investigation of the role of lemmas in automated theorem proving. The paper describes experiments with a combined system involving learning technology that generates useful lemmas for automated theorem provers, demonstrating improvement for several representative systems and solving a hard problem not solved by any system for twenty years. By focusing on condensed detachment problems we simplify the setting considerably, allowing us to get at the essence of lemmas and their role in proof search.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google