Investigations into Proof Structures

要約

タイトル：Proof構造の調査
要約：
– Proofをグローバルなオブジェクトとして操作および分析するための新しい形式論法を紹介し、詳しく説明します。
– 最初のアプローチでは、縮約脱着によって特徴付けられる1階問題に制限されています。
– {\L}ukasiewiczが広く研究されている問題の歴史的な証明の包括的な形式的再構成および分析に適用されます。
– このアプローチの基盤となるものは、証明検証の過程で補題を生成する新しい体系的方法への道を開くものです。
– 検証に関する数多くの報告実験の中で、人間または機械によって見つかった証明よりもはるかに短い{\L}ukasiewiczの問題の証明が自動的に発見されました。

要約のポイントは次のとおりです。

– プルーフ構造についての新しい形式論法の紹介
– 縮約脱着に特化するアプローチ
– 広く研究されている{\L}ukasiewiczの問題の歴史的な証明の例示的な再構成および分析
– 証明検証における新しい補題生成体系についてのアプローチ
– 人間または機械によって見つかったそれ以前に見つかったものよりはるかに短い{\L}ukasiewiczの問題の証明が、自動的に発見された。

要約(オリジナル)

We introduce and elaborate a novel formalism for the manipulation and analysis of proofs as objects in a global manner. In this first approach the formalism is restricted to first-order problems characterized by condensed detachment. It is applied in an exemplary manner to a coherent and comprehensive formal reconstruction and analysis of historical proofs of a widely-studied problem due to {\L}ukasiewicz. The underlying approach opens the door towards new systematic ways of generating lemmas in the course of proof search to the effects of reducing the search effort and finding shorter proofs. Among the numerous reported experiments along this line, a proof of {\L}ukasiewicz’s problem was automatically discovered that is much shorter than any proof found before by man or machine.

arxiv情報

提供元, 利用サービス

arxiv.jp, OpenAI