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

2022 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の基礎理論を構築すること、そのために数学基礎論由来の深い成果を援用すること、そしてたとえ控えめであっても一般人の目にわかりやすい成果を挙げることを目標としている。

2022年度は、Satallax等の汎用型システムで採用されているSAT還元の手法についての研究を進め、線形算術との融合に取り組んだ。また派生的課題として、素代数的束の圏の線形分解により得られる線形論理のモデルに焦点を当て、単純型ラムダY計算の計算複雑性へ応用する手法を検討した。またクリーネ代数とトレースつきモノイダル圏の関係について調べ、線形論理の新たなモデルを得る研究に着手した。最後にATPの前処理において重要な役割を果たすスコーレム化について、実効的スコーレム化などの亜種の考察を行った。

Current Status of Research Progress

3: Progress in research has been slightly delayed.

Reason

依然としてATPシステムの実装面における問題（SAT還元と単一化に基づく等式推論、および条件的等式の取り扱いを融合させる点）が解決していない。別のアプローチに取り組む必要があるかもしれない。
成果普及については、ATPのSAT還元を中心として執筆を進めているが、新規性を目指す一方、基礎知識も組み込まなくてはならないためその兼ね合いに苦慮している。
派生的テーマについては、クリーネ代数など専門外の知識が必要のため、調査を進めている段階である。

Strategy for Future Research Activity

ATPの実装面における問題を解決するため、別のアプローチも試みる。また昨年度台頭した派生的テーマにも重点をおき、クリーネ代数と線形論理の関係や精密なスコーレム化など専門外の分野へも研究範囲を広げる予定である。

Causes of Carryover

主な使用予定は海外出張に関わるものであるが、前年度は健康上の問題のため出張を控えていた。今年度は複数の出張予定があるため、そのために利用する予定である。