集合論ベースの定理証明支援系の言語仕様の刷新

Research Project

Project/Area Number	24K14897
Research Category	Grant-in-Aid for Scientific Research (C)
Allocation Type	Multi-year Fund
Section	一般
Review Section	Basic Section 60050:Software-related
Research Institution	Yamaguchi University
Principal Investigator	中正和久山口大学, 大学院創成科学研究科, 准教授 (40780242)
Project Period (FY)	2024-04-01 – 2027-03-31
Project Status	Granted (Fiscal Year 2024)
Budget Amount *help	¥4,550,000 (Direct Cost: ¥3,500,000、Indirect Cost: ¥1,050,000) Fiscal Year 2026: ¥1,430,000 (Direct Cost: ¥1,100,000、Indirect Cost: ¥330,000) Fiscal Year 2025: ¥1,430,000 (Direct Cost: ¥1,100,000、Indirect Cost: ¥330,000) Fiscal Year 2024: ¥1,690,000 (Direct Cost: ¥1,300,000、Indirect Cost: ¥390,000)
Keywords	定理証明支援系 / 集合論 / 一階述語論理
Outline of Research at the Start	現在主流の定理証明支援系は型理論を基礎とするが，現代数学の研究対象の大部分は集合論上に構築されているため，数学者にとっては使い勝手が悪い．本研究の目的は，LaTeXのように日常的に利用される定理証明支援系の構築を目指して，集合論ベースの定理証明支援系の言語仕様の刷新を提案するとともに，その有効性と実現可能性を検証することである．このための研究戦略は，近年のプログラミングパラダイムと自動定理証明の研究成果をシステムに取り込むことである．本研究の目標が実現されれば，数学論文の正しさを査読するプロセスが不要になるとともに，生成系AIを用いた定理証明支援に有益な言語的基盤を提供することにつながる．