| 研究課題/領域番号 |
20K11679
|
|---|
| 研究機関 | 京都大学 |
|---|
研究代表者 |
照井 一成 京都大学, 数理解析研究所, 准教授 (70353422)
|
|---|
| 研究期間 (年度) |
2020-04-01 – 2025-03-31
|
| キーワード | 自動定理証明 / 線形論理 / 循環証明系 |
|---|
| 研究実績の概要 |
本研究は、数学における自動定理証明（ATP）に関わるものである。現在主流なのはTPTP問題集、MizarやFlyspeck等、広範な数学分野をカバーする大規模ライブラリにのっとった研究である。一方で本研究はこれらとは一線を画し、数学の中でも特定分野（線形代数）に特化したATPの基礎理論を構築すること、そのために理論コンピュータ科学や数学基礎論由来の深い成果を援用することを目標としている。さらにはいくつかの派生的話題を設定し萌芽的研究を進めることで、ATP研究の幅を広げることも企図している。
2023年度は主に派生的課題に取り組んだ。とくに線形論理の意味論において重要な役割を果たす集合と関係の圏Relと形式言語理論におけるクリーネ代数の基本的関係について考察した。後者には代数的なアプローチに加え、有効な循環定理証明系の存在も知られているため、これを足掛かりとして循環定理証明系の圏論的解釈へとつなげることを画策している。また、一部のトレースつきモノイダル圏の内部言語に対して有効な循環定理証明系を与えるための手がかりを得た。さらに2021年度からの継続課題として、非可術的証明論におけるΩ規則を論理の代数的意味論におけるデーデキンド・マクニール完備化に対応づける研究を進めた。両者を足掛かりとして、非可術的論理に対する循環定理証明系の考案、および「潰し」と呼ばれる証明論的技法に対して代数的解釈・圏論的解釈を与えることを目論んでいる。
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
4: 遅れている
理由
前年度に引き続き、証明システムの実装がうまくいっていない。具体的には実計算における条件付き等式の取り扱いが、筆者の意図する証明システムと相性が悪い。そのためATP方面において目立った成果は未だ出ていない。
派生的話題については、クリーネ代数とRelの基本的対応は得られている。しかしそこから線形論理や形式言語理論で有意な結果を得るとなると話は別であり、そのためにはもう少しクリーネ代数の深い結果について調査を進める必要があると考えている。またトレース付きモノイダル圏の内部言語に対して循環定理証明系を与えるという着想も、いまだ具現化ができていない。循環定理証明系に圏論的解釈を与えるという逆方向の研究についても同様である。最後にΩ規則とデーデキンド・マクニール完備化について、代数的解釈はすでに得られている。しかしそこから伝統的証明論において有意な結果を得るところで難点を抱えている。
|
| 今後の研究の推進方策 |
ATP関連については、現状のアプローチの問題点が浮き彫りになったので、別の着想を得る必要がある。そのためにまずは既存研究（大規模ライブラリからの定理証明）のさらなる調査を進めたい。一方派生的話題については、着想、基本的性質、進むべき方向性についてはすでに有力な手掛かりが得られている。それらをさらに突き詰めて、有意な成果につなげることに専念したい。そのため形式言語理論、非可術的証明論、トレース付きモノイダル圏について再調査を行うとともに、循環定理証明系と論理の代数的意味論の研究をさらに進めたい。
|
| 次年度使用額が生じた理由 |
コロナ禍による2020年度の出張キャンセル分が未だに影響している。また筆者の体調不良もあり研究がやや停滞しているため、成果発表のための旅費に余剰が生じている。2024年度は成果発表の機会を増やし、主に国内・国外旅費に残りの予算を用いる予定である。
|
| 備考 |
学会発表２件は指導する大学院生による研究発表である。本研究課題と密接に関係するため出張旅費を支出した。
|
