Can Computer be a Mathematician? Automated Theorem Proving in Undergraduate Mathematics

2021 Fiscal Year Research-status Report

• Project/Area Number: 20K11679
• Research Institution: Kyoto University
• Principal Investigator: 照井 一成 京都大学, 数理解析研究所, 准教授 (70353422)
• Project Period (FY): 2020-04-01 – 2025-03-31
• Keywords: 自動定理証明 / 数理論理学 / 実線形算術

Outline of Annual Research Achievements

本研究は、数学における自動定理証明（ATP）に関わるものである。現在主流なのはTPTP問題集、MizarやFlyspeck等、広範な数学分野をカバーする大規模ライブラリにのっとった研究である。一方で本研究はこれらとは一線を画し、数学の中でも特定分野（線形代数）に特化したATPの基礎理論を構築すること、そのために数学基礎論由来の深い成果を援用すること、そしてたとえ控えめであっても一般人の目にわかりやすい成果を挙げることを目標としている。

2021年度は、先年に引き続き実線形算術に関するATP研究に取り組んだ。基本的な方針はタブロー法をSAT還元することにより定理証明を行うというものであるが、線形算術に特有の推論部分に関していくつか独自の方法を考案し、検討を行った。また派生研究として、デーデキント・マクニール完備化に基づくカット除去定理の証明法を算術理論の内部で形式化する研究を行った。それにより、帰納的定義の理論IDnと対応する論理体系が竹内同値の関係にあることを示した。

最後に、本研究の目標達成のためにはATPの普及活動が不可欠であるが、そのために入門書の執筆を進めた。現状、ブール代数、SATソルバー、SAT還元に関する章の執筆が終わっている。

Current Status of Research Progress

3: Progress in research has been slightly delayed.

Reason

前年度と同様、ATPシステム実装における問題が解決していない。論理推論部分についてはうまく働くものの、実線形算術に特有の部分（ある種の条件付き等式の取り扱い）に困難が生じている。そのため、2021年度は多少目先を変え、主に数学基礎論的な部分に取り組むことにした。算術におけるクライゼル予想のさらなる分析、循環証明系のタブロー化などが眼目であるが、未だこれらに関する成果は出ていない。

他方で派生的な研究であるデーデキント・マクニール完備化に基づくカット除去定理については新たな成果が得られている。また成果普及のための入門書執筆もある程度進められている。

Strategy for Future Research Activity

当初の研究計画通りに、理論研究、実装・実験、成果普及の３点を並行して進める。とくに遅れている実装・実験面に重点的に取り組みたい。

Causes of Carryover

コロナ禍のため出張が一切行えなかった。また2020年度分の繰越しが大きく影響している。今年度以降の国内・国外出張旅費に利用したい。