関係計算の形式化を用いた数学とソフトウェア検証のための理論構築

2019 年度 研究成果報告書

• 研究課題/領域番号: 17K05346
• 研究種目: 基盤研究(C)
• 配分区分: 基金
• 応募区分: 一般
• 研究分野: 数学基礎・応用数学
• 研究機関: 九州大学
• 研究代表者: 溝口 佳寛 九州大学, マス・フォア・インダストリ研究所, 教授 (80209783)
• 研究期間 (年度): 2017-04-01 – 2020-03-31
• キーワード: 数理論理学 / 関係計算 / 形式証明 / 形式手法 / モデル検査 / 圏論のモナドの形式化

研究成果の概要

本研究の目的は、高信頼ソフトウェア開発の基礎となる数理論理学や離散数学、特に計算機による自動検証可能な形式証明を意識した関係計算による証明を用いた数学体系を広げることてある。特に、関係計算系の基本公理やデデキント圏の公理をCoq定理証明支援系で定式化し、関係、関数に関する補題や定理を形式的に与えた。また、射の結合に関する基本補題の集積と自動証明を行う手順きをタクティクスとして実現した。さらに、Coq定理証明支援系の初歩的な補題を具体例とともに整理し、紹介文書、および、形式証明集を公表した。

自由記述の分野

理論計算機科学

研究成果の学術的意義や社会的意義

本研究は高信頼ソフトウェア開発の基礎となる数理論理学や離散数学、特に計算機による自動検証可能な形式証明を意識した関係計算による証明を用いた数学体系を拡げることである。
近年の計算機能力、および、定理証明支援系ソフトウェアの進歩により、数値計算、数式処理計算のみならず、論理計算についても自動検証可能になり、四色定理、ケプラー予想など,計算機でしか厳密に検証出来ない数学定理の証明も発表されるようになっている。このような背景のもと本研究では論理計算を内包する関係計算に主眼を置いた数学理論の再構築、形式証明データベースの作成など、自動検証可能な数学理論体系を提案するものである。