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

• 研究課題/領域番号: 24K14897
• 研究種目: 基盤研究(C)
• 配分区分: 基金
• 応募区分: 一般
• 審査区分: 小区分60050:ソフトウェア関連
• 研究機関: 山口大学
• 研究代表者: 中正 和久 山口大学, 大学院創成科学研究科, 准教授 (40780242)
• 研究期間 (年度): 2024-04-01 – 2027-03-31
• 研究課題ステータス: 交付 (2024年度)
• 配分額: 4,550千円 (直接経費: 3,500千円、間接経費: 1,050千円); 2026年度: 1,430千円 (直接経費: 1,100千円、間接経費: 330千円); 2025年度: 1,430千円 (直接経費: 1,100千円、間接経費: 330千円); 2024年度: 1,690千円 (直接経費: 1,300千円、間接経費: 390千円)
• キーワード: 定理証明支援系 / 集合論 / 一階述語論理

研究開始時の研究の概要

現在主流の定理証明支援系は型理論を基礎とするが，現代数学の研究対象の大部分は集合論上に構築されているため，数学者にとっては使い勝手が悪い．本研究の目的は，LaTeXのように日常的に利用される定理証明支援系の構築を目指して，集合論ベースの定理証明支援系の言語仕様の刷新を提案するとともに，その有効性と実現可能性を検証することである．このための研究戦略は，近年のプログラミングパラダイムと自動定理証明の研究成果をシステムに取り込むことである．本研究の目標が実現されれば，数学論文の正しさを査読するプロセスが不要になるとともに，生成系AIを用いた定理証明支援に有益な言語的基盤を提供することにつながる．