| Project/Area Number |
20K11679
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Allocation Type | Multi-year Fund |
|---|
| Section | 一般 |
|---|
| Review Section |
Basic Section 60010:Theory of informatics-related
|
|---|
| Research Institution | Kyoto University |
|---|
Principal Investigator |
照井 一成 京都大学, 数理解析研究所, 准教授 (70353422)
|
|---|
| Project Period (FY) |
2020-04-01 – 2025-03-31
|
| Project Status |
Granted (Fiscal Year 2023)
|
| Budget Amount *help |
¥4,550,000 (Direct Cost: ¥3,500,000、Indirect Cost: ¥1,050,000)
Fiscal Year 2024: ¥910,000 (Direct Cost: ¥700,000、Indirect Cost: ¥210,000)
Fiscal Year 2023: ¥910,000 (Direct Cost: ¥700,000、Indirect Cost: ¥210,000)
Fiscal Year 2022: ¥910,000 (Direct Cost: ¥700,000、Indirect Cost: ¥210,000)
Fiscal Year 2021: ¥910,000 (Direct Cost: ¥700,000、Indirect Cost: ¥210,000)
Fiscal Year 2020: ¥910,000 (Direct Cost: ¥700,000、Indirect Cost: ¥210,000)
|
|---|
| Keywords | 自動定理証明 / 線形論理 / 循環証明系 / 数理論理学 / 実線形算術 / 自動定理生成 |
|---|
| Outline of Research at the Start |
数学における自動定理証明の成功例は、ごく限られている。この現状を打破するための第一歩として、大学数学、とくに線形代数に特化した自動定理証明の研究を行う。理論面では数学基礎論・コンピュータ科学論理（とくに最近の証明論）に由来するアイデアを援用する。また、有意味な定理を大量に自動生成する方法を考案し、機械学習に役立てる。最後に「楽しいコンピュータ証明」を実現するために、わかりやすい教科書を執筆し、簡易的な証明システムを公開することで多くの人に自動定理証明を身近なものとして体験してもらう。それにより、数学における自動定理証明の研究機運を次第に高めていきたいというのが目論見である。
|
| Outline of Annual Research Achievements |
本研究は、数学における自動定理証明（ATP）に関わるものである。現在主流なのはTPTP問題集、MizarやFlyspeck等、広範な数学分野をカバーする大規模ライブラリにのっとった研究である。一方で本研究はこれらとは一線を画し、数学の中でも特定分野（線形代数）に特化したATPの基礎理論を構築すること、そのために理論コンピュータ科学や数学基礎論由来の深い成果を援用することを目標としている。さらにはいくつかの派生的話題を設定し萌芽的研究を進めることで、ATP研究の幅を広げることも企図している。
2023年度は主に派生的課題に取り組んだ。とくに線形論理の意味論において重要な役割を果たす集合と関係の圏Relと形式言語理論におけるクリーネ代数の基本的関係について考察した。後者には代数的なアプローチに加え、有効な循環定理証明系の存在も知られているため、これを足掛かりとして循環定理証明系の圏論的解釈へとつなげることを画策している。また、一部のトレースつきモノイダル圏の内部言語に対して有効な循環定理証明系を与えるための手がかりを得た。さらに2021年度からの継続課題として、非可術的証明論におけるΩ規則を論理の代数的意味論におけるデーデキンド・マクニール完備化に対応づける研究を進めた。両者を足掛かりとして、非可術的論理に対する循環定理証明系の考案、および「潰し」と呼ばれる証明論的技法に対して代数的解釈・圏論的解釈を与えることを目論んでいる。
|
| Current Status of Research Progress |
Current Status of Research Progress
4: Progress in research has been delayed.
Reason
前年度に引き続き、証明システムの実装がうまくいっていない。具体的には実計算における条件付き等式の取り扱いが、筆者の意図する証明システムと相性が悪い。そのためATP方面において目立った成果は未だ出ていない。
派生的話題については、クリーネ代数とRelの基本的対応は得られている。しかしそこから線形論理や形式言語理論で有意な結果を得るとなると話は別であり、そのためにはもう少しクリーネ代数の深い結果について調査を進める必要があると考えている。またトレース付きモノイダル圏の内部言語に対して循環定理証明系を与えるという着想も、いまだ具現化ができていない。循環定理証明系に圏論的解釈を与えるという逆方向の研究についても同様である。最後にΩ規則とデーデキンド・マクニール完備化について、代数的解釈はすでに得られている。しかしそこから伝統的証明論において有意な結果を得るところで難点を抱えている。
|
| Strategy for Future Research Activity |
ATP関連については、現状のアプローチの問題点が浮き彫りになったので、別の着想を得る必要がある。そのためにまずは既存研究（大規模ライブラリからの定理証明）のさらなる調査を進めたい。一方派生的話題については、着想、基本的性質、進むべき方向性についてはすでに有力な手掛かりが得られている。それらをさらに突き詰めて、有意な成果につなげることに専念したい。そのため形式言語理論、非可術的証明論、トレース付きモノイダル圏について再調査を行うとともに、循環定理証明系と論理の代数的意味論の研究をさらに進めたい。
|
