2014 Fiscal Year Annual Research Report
| Project/Area Number |
25610034
|
|---|
| Research Institution | Kyushu University |
|---|
Principal Investigator |
溝口 佳寛 九州大学, マス・フォア・インダストリ研究所, 准教授 (80209783)
|
|---|
| Project Period (FY) |
2013-04-01 – 2015-03-31
|
| Keywords | 数理論理学 / 形式証明 / 定理証明検証 / ソフトウェア検証 / Coq / 証明支援系 / 定理証明器 |
|---|
| Outline of Annual Research Achievements |
最終年度は離散数学と理論計算機科学の合同研究集会の開催により, 今後の当萌芽研究課題の継続と発展のための礎を作る事を第一に考えた. 特に数学理論の形式化だけでなく, 産業界でのソフトウェア開発研究者との交流と課題の共有のための研究集会を企画した. 形式証明は日本においては普及していないので, 海外からの研究者を招聘し交流を行った. 具体的には, 証明支援系Coqを用いたプログラム検証研究について米MITのA.Chlipara氏, また, 数学理論, 特に群論の奇数位数定理の形式化のためのCoqモジュール開発者である仏INRIA研究所のC.Cohen氏を招待講演者とし, 九州大学IMI数学理論先進ソフトウェア開発室主催, 統計数理研究所数学恊働プログラム共催で研究集会「高信頼な理論と実装のための定理証明および定理証明器」を開催した. 本会は予想以上に盛況であり, 企業研究者9名, 大学院生26名を含む総数74名の参加者が全国から参集し, 本研究課題への関心が高いことが明らかになった.
個別の主結果は以下の3点である. (1)分子計算のモデルであるスティッカー系とオートマトンに関する形式証明について日本数学会において講演を行い研究成果を九州大学レポジトリに公開し, 数学理論の形式証明支援系の応用とソフトウェア検証技術との関連の広報も行った. (2)3次元球の最密充填問題であるケプラー予想の形式証明が2014年8月にT.Halesらで完了し公表されたが, その解説記事「ケプラー予想の計算機による証明と検証について」を数学セミナー誌へ掲載し数学の形式証明研究の広報を行った. (3)関係計算理論の重要性に気がつき, グラフ理論の形式化よりも優先するべきと判断し, 関係計算理論の形式証明へ着手した. その中で, ファジー関係計算を用いたデータベース理論の一般化, および, その制御理論への応用について成果を公表した. 関係計算, および, データベースを用いた制御系の信頼性評価への応用可能性が評価された.
|
