離散構造体の計算理論に関する形式的証明と自動検証

• 研究課題/領域番号: 25610034
• 研究種目: 挑戦的萌芽研究
• 配分区分: 基金
• 研究分野: 数学基礎・応用数学
• 研究機関: 九州大学
• 研究代表者: 溝口 佳寛 九州大学, マス・フォア・インダストリ研究所, 准教授 (80209783)
• 研究期間 (年度): 2013-04-01 – 2015-03-31
• 研究課題ステータス: 完了 (2014年度)
• 配分額: 3,640千円 (直接経費: 2,800千円、間接経費: 840千円); 2014年度: 1,820千円 (直接経費: 1,400千円、間接経費: 420千円); 2013年度: 1,820千円 (直接経費: 1,400千円、間接経費: 420千円)
• キーワード: 数理論理学 / 数学の形式化 / 検証可能証明 / ソフトウェア検証 / 離散数学 / 計算理論 / 形式証明 / 定理証明検証 / Coq / 証明支援系 / 定理証明器 / 有限オートマトン / Isabelle / Mizar

研究成果の概要

組合せ数学, 論理と計算に関するセミナー等を中心に離散構造体に関する数学の形式化として, 有限オートマトン, スティッカー系, ファジー・データベースの定式化を行った. 研究集会「高信頼な理論と実装のための定理証明および定理証明器」では数学, 計算機科学, 産業界の各方面から, 国内外合わせて約80名の参加者が集い, 形式証明に関する結果の理解と今後の展開への道筋を共有することが出来た. また, 同時期に公開された400年来の難問であったケプラー予想の形式証明については, 解説記事を速報すると同時に, 数学教育現場に携わる先生方等への今後の数学の形式化についての傾向と展開について広報した.

研究成果

• [雑誌論文] A Property of Random Walks on a Cycle Graph (2015)
  • 著者名/発表者名: Y.Ikeda, Y.Fukai, Y.Mizoguchi
  • 雑誌名: Pacific Journal of Mathematics for Industry 巻: 印刷中
  • NAID: 40020727637
  • 査読あり / オープンアクセス / 謝辞記載あり
• [雑誌論文] ケプラー予想の計算機による証明と検証について (2014)
  • 著者名/発表者名: 溝口佳寛, 田上真
  • 雑誌名: 数学セミナー 巻: 12月号 ページ: 48-54
  • NAID: 40020260734
• [雑誌論文] Theory of Automata, Abstraction and Applications (2014)
  • 著者名/発表者名: Y.Mizoguchi
  • 雑誌名: A Mathematical Approach to Research Problems of Science and Technology, Mathematis for Industry 巻: 5 ページ: 337-348
• [雑誌論文] Formal Proofs for Automata and Sticker Systems (2014)
  • 著者名/発表者名: H.Tanaka, I.Sakashita, S.Inokuchi, Y.Mizoguchi
  • 雑誌名: Proc. of 1st International Workshop on Computing and Networking 巻: 1 ページ: 563-566
  • DOI: 10.1109/candar.2013.100
  • 査読あり
• [雑誌論文] A formulation of Composition for Cellular Automata on Groups (2014)
  • 著者名/発表者名: S.Inokuchi, T.Ito, M.Fujio, Y.Mizoguchi
  • 雑誌名: IEICE Transactions on Information and Systems 巻: E97-D(3) ページ: 448-454
  • NAID: 130003394860
  • 査読あり
• [学会発表] Mathematical Aspects of Interpolation Technique for Computer Graphics (2015)
  • 著者名/発表者名: Y.Mizoguchi
  • 学会等名: Kick-off Meeting of IMI Australia Branch in La Trobe
  • 発表場所: La Trobe University, Australia
  • 年月日: 2015-03-12 – 2015-03-13
  • 招待講演
• [学会発表] Coqチュートリアル (2015)
  • 著者名/発表者名: 溝口佳寛
  • 学会等名: ウィンタースクール「数学ソフトウェア・チュートリアル」
  • 発表場所: 九州大学
  • 年月日: 2015-02-18 – 2015-02-19
  • 招待講演
• [学会発表] 関係計算証明ライブラリによる写像の性質の証明 (2015)
  • 著者名/発表者名: 松嶋聡昭
  • 学会等名: Software in Mathematics Demonstration Track in Hakata Workshop 2015
  • 発表場所: 福岡市
  • 年月日: 2015-02-15
• [学会発表] ケプラー予想の計算機による証明と検証について (2014)
  • 著者名/発表者名: 溝口佳寛
  • 学会等名: 九州数学教育会第4回算数・数学教育研修会
  • 発表場所: 福岡市
  • 年月日: 2014-12-07
• [学会発表] Fuzzy Relational Database Model Using Relational Calculus, (2014)
  • 著者名/発表者名: M.D.Akbar, Y.Mizoguchi
  • 学会等名: 7th International Conference on Soft Computing and Intelligent Systems
  • 発表場所: 北九州市
  • 年月日: 2014-12-03
• [学会発表] A Mathematica module for Conformal Geometric Algebra (2014)
  • 著者名/発表者名: M.Kondo, T.Matsuo
  • 学会等名: Symposium MEIS 2014: Mathematical Progress in Expressive Image Synthesis
  • 発表場所: 九州大学西新プラザ
  • 年月日: 2014-11-12 – 2014-11-14
• [学会発表] 有限オートマトンとスティッカー系に関するCoqによる形式証明について (2014)
  • 著者名/発表者名: 溝口佳寛,田中久治,坂下一生,井口修一
  • 学会等名: 日本数学会2014年度年会
  • 発表場所: 学習院大学
• [学会発表] Formal Proofs for Automata and Sticker Systems (2013)
  • 著者名/発表者名: H.Tanaka, I.Sakashita, S.Inokuchi, Y.Mizoguchi
  • 学会等名: 1st International Workshop on Computing and Networking
  • 発表場所: Ehime, Japan.
• [学会発表] グラフ上の追跡戦略と回避戦略 (2013)
  • 著者名/発表者名: 池田有希,溝口佳寛
  • 学会等名: 情報処理学会ネットワーク生態学研究会第10回シンポジウム
  • 発表場所: かんぽの宿有馬
• [備考] 組合せ数学セミナー
  • URL: http://comb.math.kyushu-u.ac.jp
• [備考] 論理と計算セミナー
  • URL: http://sakura.imi.kyushu-u.ac.jp/wiki/index.php?Seminar
• [備考] 研究集会「高信頼な理論と実装のための定理証明および定理証明器」
  • URL: http://imi.kyushu-u.ac.jp/lasm/tpp2014/
• [備考] 発表資料「有限オートマトンとスティッカー系に関するCoqによる形式証明について」
  • URL: http://catalog.lib.kyushu-u.ac.jp/recordID/1430787
• [備考] 有限オートマトンとスティッカー系に関するCoqによる形式証明について
  • URL: http://hdl.handle.net/2324/1430787