2019 Fiscal Year Annual Research Report
Theory of relational calculus for formal verification of mathematics and software programs.
| Project/Area Number |
17K05346
|
|---|
| Research Institution | Kyushu University |
|---|
Principal Investigator |
溝口 佳寛 九州大学, マス・フォア・インダストリ研究所, 教授 (80209783)
|
|---|
| Project Period (FY) |
2017-04-01 – 2020-03-31
|
| Keywords | 数理論理学 / 関係計算 / 形式証明 / 形式手法 / Wangタイル / パターン生成 / Coq |
|---|
| Outline of Annual Research Achievements |
本研究の目的は、高信頼ソフトウェア開発の基礎となる数理論理学や離散数学、特に計算機による自動検証可能な形式証明を意識した、関係計算による証明を用いた数学体系を広げることである。今年度は、コンピュータグラフィックスへの応用プログラムの形式化と関係計算理論の形式化に関して、次の（１）、（２）、（３）の活動を行なった。
（１）コンピュータグラフィックスにおけるパターン画像生成にも応用されるパターン生成方法である、Wangタイルを用いた与えられた境界条件を満たすタイルパターン生成方法を考察した.。特にレンガ型Wangタイルと呼ぶタイル集合による、境界条件を満たす解を線形時間で生成するアルゴリズムを提案し、様々なパターン生成へ応用可能なことを例とともに示した。また、提案アルゴリズムの正当性の証明をCoq定理証明支援系による形式証明でも行なった。
（２）関係計算系の基本公理やデデキント圏の公理をCoq定理証明支援系で定式化し、関係、関数に関する補題や定理を形式的に与えた。特に、射の結合に関する基本補題の集積と自動証明を行う手順きをタクティクスとして実現した。さらに、Coq定理証明支援系の初歩的な補題を具体例とともに整理し、紹介文書、および、形式証明集を公表した。
（３）九州大学マス・フォア・インダストリ研究所短期共同研究「ゲーム開発へのモデル検査の適用」、および、 同研究集会「代数・論理・幾何と情報科学―理論から実世界への展開」において、参加者と討論を行い、成果の紹介、および、今後の展開についての議論を行なった。そして、今後の研究成果の活用を推進するため、研究成果に至るまでの成果等を、講演スライド、 数学ソフトウェア、公表論文等一覧として、ホームページ上に整理して公表した。
|
