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

点击翻译按钮获取中文摘要

本研究は、数学における自動定理証明（ATP）に関わるものである。現在主流なのはTPTP問題集、MizarやFlyspeck等、広範な数学分野をカバーする大規模ライブラリにのっとった研究である。一方で本研究はこれらとは一線を画し、数学の中でも特定分野（線形代数）に特化したATPの基礎理論を構築すること、そのために数学基礎論由来の深い成果を援用すること、そしてたとえ控えめであっても一般人の目にわかりやすい成果を挙げることを目標としている。2022年度は、Satallax等の汎用型システムで採用されているSAT還元の手法についての研究を進め、線形算術との融合に取り組んだ。また派生的課題として、素代数的束の圏の線形分解により得られる線形論理のモデルに焦点を当て、単純型ラムダY計算の計算複雑性へ応用する手法を検討した。またクリーネ代数とトレースつきモノイダル圏の関係について調べ、線形論理の新たなモデルを得る研究に着手した。最後にATPの前処理において重要な役割を果たすスコーレム化について、実効的スコーレム化などの亜種の考察を行った。