| 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 2022)
|
| 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の基礎理論を構築すること、そのために数学基礎論由来の深い成果を援用すること、そしてたとえ控えめであっても一般人の目にわかりやすい成果を挙げることを目標としている。
2022年度は、Satallax等の汎用型システムで採用されているSAT還元の手法についての研究を進め、線形算術との融合に取り組んだ。また派生的課題として、素代数的束の圏の線形分解により得られる線形論理のモデルに焦点を当て、単純型ラムダY計算の計算複雑性へ応用する手法を検討した。またクリーネ代数とトレースつきモノイダル圏の関係について調べ、線形論理の新たなモデルを得る研究に着手した。最後にATPの前処理において重要な役割を果たすスコーレム化について、実効的スコーレム化などの亜種の考察を行った。
|
| Current Status of Research Progress |
Current Status of Research Progress
3: Progress in research has been slightly delayed.
Reason
依然としてATPシステムの実装面における問題（SAT還元と単一化に基づく等式推論、および条件的等式の取り扱いを融合させる点）が解決していない。別のアプローチに取り組む必要があるかもしれない。
成果普及については、ATPのSAT還元を中心として執筆を進めているが、新規性を目指す一方、基礎知識も組み込まなくてはならないためその兼ね合いに苦慮している。
派生的テーマについては、クリーネ代数など専門外の知識が必要のため、調査を進めている段階である。
|
| Strategy for Future Research Activity |
ATPの実装面における問題を解決するため、別のアプローチも試みる。また昨年度台頭した派生的テーマにも重点をおき、クリーネ代数と線形論理の関係や精密なスコーレム化など専門外の分野へも研究範囲を広げる予定である。
|
