形式検証のための解析学推論ライブラリの拡充

• 研究課題/領域番号: 23K11242
• 研究種目: 基盤研究(C)
• 配分区分: 基金
• 応募区分: 一般
• 審査区分: 小区分61030:知能情報学関連
• 研究機関: 岐阜工業高等専門学校
• 研究代表者: 遠藤 登 岐阜工業高等専門学校, その他部局等, 教授 (30342497)
• 研究期間 (年度): 2023-04-01 – 2028-03-31
• 研究課題ステータス: 交付 (2023年度)
• 配分額: 4,420千円 (直接経費: 3,400千円、間接経費: 1,020千円); 2027年度: 1,300千円 (直接経費: 1,000千円、間接経費: 300千円); 2026年度: 520千円 (直接経費: 400千円、間接経費: 120千円); 2025年度: 650千円 (直接経費: 500千円、間接経費: 150千円); 2024年度: 650千円 (直接経費: 500千円、間接経費: 150千円); 2023年度: 1,300千円 (直接経費: 1,000千円、間接経費: 300千円)
• キーワード: 形式検証 / 証明検証システム / 推論ライブラリ

研究開始時の研究の概要

近年コンピュータによる数学の形式化（形式化数学）及び形式検証システムが盛んに研究されている．形式化数学は理論を推論プログラムとして形式化し，形式検証システムは推論の正当性をコンピュータで検証するシステムであり，自動推論，自動検証などの高度なAIには必要不可欠な技術である．また形式化数学では定理の完全な検証とともに，その推論過程が推論ライブラリとして蓄積されることが重要である．しかし高度な問題を形式手法で解決するためには様々な分野を網羅した大規模な形式化数学ライブラリが必須であり，本研究では証明支援系Mizarを用いて解析学を中心とした推論ライブラリを拡充する．