定理証明支援系を用いた数学的定理の発見的証明

• 研究課題/領域番号: 24K14820
• 研究種目: 基盤研究(C)
• 配分区分: 基金
• 応募区分: 一般
• 審査区分: 小区分60010:情報学基礎論関連
• 研究機関: 名古屋大学
• 研究代表者: 才川 隆文 名古屋大学, 多元数理科学研究科, 研究員 (00897100)
• 研究分担者: 松田 一徳 北見工業大学, 工学部, 准教授 (20633241)
• 研究期間 (年度): 2024-04-01 – 2027-03-31
• 研究課題ステータス: 交付 (2024年度)
• 配分額: 4,550千円 (直接経費: 3,500千円、間接経費: 1,050千円); 2026年度: 1,560千円 (直接経費: 1,200千円、間接経費: 360千円); 2025年度: 1,300千円 (直接経費: 1,000千円、間接経費: 300千円); 2024年度: 1,690千円 (直接経費: 1,300千円、間接経費: 390千円)
• キーワード: 定理証明支援系 / Coq / グラフ理論 / 可換代数 / 型理論

研究開始時の研究の概要

数学および理論計算機科学において、性質や定理を厳密に記述し、また証明の正確さを検査するために用いられるソフトウェアとして、定理証明支援系がある。計算機科学において多くのシステムの健全性を保証してきた定理証明支援系であるが、数学への応用における既存の研究では、既に知られた定理に対して細部を厳密にした正確な再証明を与えるという形をとってきた。本研究は、定理証明支援系が数学における発見的活動をも支援できることを実証するため、グラフ理論と可換代数の境界分野という、未解決問題が多く呈示されている数学分野を題材として形式化を行ない、その厳密な基盤に立って新規定理の形式的証明を与えることを目標とする。