2025/04/04 更新

写真a

ミゾグチ　ヨシヒロ
溝口 佳寛
MIZOGUCHI YOSHIHIRO
所属
マス・フォア・インダストリ研究所 応用理論研究部門 教授
数理・データサイエンス教育研究センター （併任）
情報基盤研究開発センター （併任）
理学部 数学科（併任）
数理学府 数理学専攻（併任）
マス・フォア・イノベーション連係学府 （併任）
職名
教授
連絡先
メールアドレス
プロフィール
[研究活動] ソフトウェア科学の基礎理論とそれらの応用プログラム開発について研究を行なっている. グラフ構造は, 複雑な状況を直観的に説明するための基本的な道具として計算機が生まれる前からその構造についての研究や応用が行なわれていた. 近年, 計算機の内部表現(データ構造)としてプログラム中でグラフが利用されるばかりか, グラフそのものを変換して計算を行なう新しい計算システムなども考案され, 従来の静的なグラフ構造の研究(グラフ理論)だけではなく, グラフを操作することに対する性質の変化を究明する研究(グラフ変換理論)が必要となっている. そこで, このグラフ変換理論の基礎研究を進めるとともに, その応用可能性を模索している. 特に, グラフ表現されたネットワークの信頼性をグラフ変換により計算するアルゴリズムとシステムの開発を進めている. [教育活動] 数理・データサイエンス教育研究センター副センター長として, データサイエンス教育に関わる企画立案, 指導, データベース構築に従事している. また, 近年の計算機ネットワークの発達により種々のデータ交換を電子メールで行なうことが多くなってきており, データの安全性(秘密)を守るために必要な暗号化技術が注目されている. これらに関連して, 公開鍵暗号化電子メールシステム, 分散オブジェクト認証技術, そして, 電子証明書による認証機能を利用した情報システムなどを, 実際的な側面としては運用面の立場から, 基礎的な側面としては数学理論の立場から教育, 及び, 研究指導を行っている. [社会活動] AIMaP(数学アドバンストイノベーションプラットフォーム事業:2018-2022)において数学技術相談ネットワーク構築のための活動をPostAMaP活動として続けている. また, 「計算機ネットワーク」を利用した教育や福祉などの諸活動に積極的に参加し協力している.
ホームページ
外部リンク

研究分野

  • 情報通信 / 情報学基礎論

  • 自然科学一般 / 応用数学、統計数学

学位

  • 博士(理学)

経歴

  • 九州大学 マス・フォア・インダストリ研究所 教授 

    2016年8月 - 現在

    　 詳細を見る

  • 九州工業大学情報工学部講師(1988年〜1993年) 同助教授(1993年〜2000年) 放送大学客員准教授(2008年〜2010年)   

研究テーマ・研究キーワード

  • 研究テーマ： 縮小写像型ニュ-ラルネットワ-ク

    研究キーワード： 縮小写像型ニュ-ラルネットワ-ク

    研究期間： 2024年

  • 研究テーマ： 数学理論を駆使した可視化技術の開発研究

    研究キーワード： 可視化技術, CG, 映像数学

    研究期間： 2014年4月 - 2018年3月

  • 研究テーマ： 離散遷移系による計算モデルの考察

    研究キーワード： オートマトン, 離散遷移系, 計算モデル

    研究期間： 2005年4月

  • 研究テーマ： 受容プロセスの促進を目的とした先天障害者支援情報システムの構築

    研究キーワード： 障害者支援, 情報システム, インターネット

    研究期間： 2002年4月 - 2011年3月

  • 研究テーマ： グラフ変換を用いた計算の単位の定式化と計算量理論の再構築

    研究キーワード： グラフ変換, アルゴリズム, 計算量, 分散計算

    研究期間： 1993年3月

論文

  • A linear algorithm for brick Wang tiling 査読 国際誌

    @Alex Derouet-Jourdan, Shizuo Kaji, Yoshihiro Mizoguchi

    Japan J. Indust. Appl. Math.   1 - 13   2019年4月

    　詳細を見る

    記述言語：英語   掲載種別：研究論文（学術雑誌）  

    DOI： https://doi.org/10.1007/s13160-019-00369-z

  • Verification of a brick Wang tiling algorithm 招待 査読 国際誌

    Toshiaki Matsushima, Yoshihiro Mizoguchi, Alexandre Derounet-Jourdan

    7th International Symposium on Symbolic Computation in Software Science (SCSS2016)   39   107 - 116   2016年3月

    　詳細を見る

    記述言語：英語   掲載種別：研究論文（学術雑誌）  

    DOI： doi.org/10.29007/2m5f

    その他リンク： https://doi.org/10.29007/2m5f

  • A Mathematica module for Conformal Geometric Algebra and Origami Folding 査読 国際誌

    MItsuhiro Kondo, Takuya Matsuo, Yoshihiro Mizoguchi, Hiroyuki Ochiai

    7th International Symposium on Symbolic Computation in Software Science (SCSS2016)   39   60 - 80   2016年3月

    　詳細を見る

    記述言語：英語   掲載種別：研究論文（国際会議プロシーディングス）  

    DOI： doi.org/10.29007/6fc5

    その他リンク： https://doi.org/10.29007/6fc5

  • A Property of Random Walks on a Cycle Graph 査読 国際誌

    Yuki Ikeda, yasunari fukai, Yoshihiro Mizoguchi

    Pacific Journal of Mathematics for Industry   7 ( 3 )   2015年12月

    　詳細を見る

    記述言語：英語   掲載種別：研究論文（学術雑誌）  

    DOI： DOI:10.1186/s40736-015-0015-3

    その他リンク： http://link.springer.com/article/10.1186/s40736-015-0015-3/fulltext.html

  • Uniqueness of Buston Hadamard matrices of small degrees 査読 国際誌

    Mitsugu Hirasaka, Kyoung-Tark Kim, Yoshihiro Mizoguchi

    Journal of Discrete Algorithms   34   70 - 77   2015年6月

    　詳細を見る

    記述言語：英語   掲載種別：研究論文（学術雑誌）  

    DOI： doi:10.1016/j.jda.2015.05.009

    その他リンク： http://www.sciencedirect.com/science/article/pii/S1570866715000623

▼全件表示

講演・口頭発表等

  • A Coq Library for the Theory of Realational Calculus 招待 国際会議

    Yoshihiro Mizoguchi

    Workshop on Formalization of Applied Mathematical Systems  2016年9月 

    　詳細を見る

    開催年月日： 2016年9月 - 2016年10月

    記述言語：英語   会議種別：口頭発表（一般）  

    開催地：University of Hawai`i, Manoa, USA   国名：日本国  

    その他リンク： http://math.hawaii.edu/~jb/workshop2/

  • Fuzzy Functional and Implication Dependency using Relational Calculus 国際会議

    Mohammad Deni Akbar, Yoshihiro Mizoguchi

    The Asian Mathematical Conference (AMC2016)  2016年7月 

    　詳細を見る

    開催年月日： 2016年7月

    記述言語：英語   会議種別：口頭発表（一般）  

    開催地：Bali Nusa Dua Convention Center   国名：インドネシア共和国  

    その他リンク： http://www.amc2016.org/home/

  • Symbolic Computations in Conformal Geometric Algebra for Three Dimensional Origami Folds 国際会議

    Yoshihiro Mizoguchi, Hiroyuki Ochiai

    First International Workshop on Computational Origami and Applications  2016年7月 

    　詳細を見る

    開催年月日： 2016年7月

    記述言語：英語   会議種別：口頭発表（一般）  

    開催地：Vienna University of Technology   国名：オーストリア共和国  

    その他リンク： http://www.cse.chalmers.se/~laurako/links/COA.html

  • Theory of Relational Calculus and its formalization 招待 国際会議

    Yoshihiro Mizoguchi

    Universal Structures in Mathematics and Computing  2016年6月 

    　詳細を見る

    開催年月日： 2016年6月

    記述言語：英語   会議種別：口頭発表（一般）  

    開催地：City Campus of La Trobe University (in Melbourne CBD)   国名：オーストラリア連邦  

    その他リンク： http://usmac.ltumathstats.com/home

  • Coqによる初等幾何の証明方法について

    溝口 佳寛, 田中久治

    日本数式処理学会  2015年6月 

    　詳細を見る

    開催年月日： 2015年6月

    記述言語：日本語   会議種別：口頭発表（一般）  

    開催地：筑波大学   国名：日本国  

▼全件表示

MISC

  • 論理と計算について考えた人たち

    溝口 佳寛

    数学セミナー, 2019年1月号, pp.57-61   2018年12月

    　詳細を見る

    記述言語：日本語   掲載種別：記事・総説・解説・論説等（学術雑誌）  

  • The Role and Importance of Mathematics in Innovation, Proceedings of the Forum "Math-for-Industry" 2015

    Bob Anderssen, Philip Broadbridge, Yasuhide Fukumoto, Naoyuki Kamiyama, Yoshihiro Mizoguchi, Konrad Polthier, OSAMU SAEKI

    Mathematics for Industry 25, Springer   2016年4月

    　詳細を見る

    記述言語：英語   掲載種別：機関テクニカルレポート，技術報告書，プレプリント等  

    その他リンク： http://www.springer.com/jp/book/9789811009617

  • 高信頼な理論と実装のための定理証明および定理証明器

    溝口 佳寛, Jacques Garrigue, 萩原学, Reynald Affeldt

    Kyushu University   2015年3月

    　詳細を見る

    記述言語：日本語   掲載種別：機関テクニカルレポート，技術報告書，プレプリント等  

    Theorem proving and provers for reliable theory and implementations (TPP2014)

    その他リンク： http://imi.kyushu-u.ac.jp/lasm/tpp2014/

  • ケプラー予想の計算機による証明と検証について

    溝口 佳寛, 田上 真

    数学セミナー, 2014年12月号, pp.48-54   2014年12月

    　詳細を見る

    記述言語：日本語   掲載種別：記事・総説・解説・論説等（学術雑誌）  

    1600年代からの大問題ケプラー予想は1998年にHalesによって証明解決されたが, その証明の正当性を誰も検証出来なかった. そして, それから10年以上の時を経て, Hales自らの手で形式証明支援系を用いケプラー予想の計算機による証明と検証が2014年8月に与えられた. 本稿はその計算機による証明と検証の解説記事である.

  • Theory of Automata

    Yoshihiro Mizoguchi

    Mathematics for Industry, Vol.5, pp.337-348   2014年7月

    　詳細を見る

    記述言語：英語   掲載種別：記事・総説・解説・論説等（学術雑誌）  

    その他リンク： http://link.springer.com/chapter/10.1007%2F978-4-431-55060-0_25

▼全件表示

Works（作品等）

  • 誤り訂正符号の原理と応用について

    溝口佳寛

    2024年7月

    　詳細を見る

    作品分類：教材   発表場所：九州大学  

    2024年度QFC-SPプライマリーコース講義「誤り訂正符号の原理と応用について」配布資料(抜粋)

    リポジトリ公開URL： https://hdl.handle.net/2324/7326921

  • A certified Wang tiling program in Coq

    Toshiaki Matsushima, Yoshihiro Mizoguchi and Alexandre Derouet-Jourdan

    2016年3月

    　詳細を見る

    We have implemented a certified Wang tiling program for tiling a rectangle region using a brick corner Wang tile set. A brick corner Wang tile set is a special Wang tile set introduced by A. Derouet-Jourdan et al. in computer graphics in 2015 to model wall patterns texture. We have implemented a tiling algorithm using Coq proof assistant and proved its correctness. This correctness assures the existence of a tiling of any brick corner Wang tile set for any size of rectangle. The essential points of our proof are the existence of a tiling for a $2 \times 2$ rectangle and a simple induction process. Since the brick corner Wang tile is a class of infinite kinds of tile sets, it is not straightforward and there are many conditional branches to prove the correctness. The certification with Coq assures that there are no lack of conditions.

    その他リンク： https://github.com/KyushuUniversityMathematics/BrickCornerWangTiling

  • A Mathematica module for Conformal Geometric Algebra and Origami Folding

    Mitsuhiro Kondo , Takuya Matsuo , Yoshihiro Mizoguchi and Hiroyuki Ochiai

    2016年3月

    　詳細を見る

    We implemented a Mathematica module of CGA which includes functions to denote CGA elements and compute several operations in CGA. We can draw the figure in 3D space which is corresponding to a CGA element. Our draw function is using Gr\"{o}bner Basis for simplifying equations of figures. It can be used for any dimensional figures. One of our motivations is to realize 3D origami system using our own CGA Library. We follow the 2D computational origami system E-Origami-System developed by Ida et.al. and formulated simple fold operations in 3D by using CGA points and motions. Then, we proved some geometric theorems about origami properties by computing CGA equation formulas.

    その他リンク： https://github.com/KyushuUniversityMathematics/MathematicaCGA

  • A certified Wang tiling program in Coq

    Toshiaki Matsushima, Yoshihiro Mizoguchi and Alexandre Derouet-Jourdan

    2016年3月

    　詳細を見る

    We have implemented a certified Wang tiling program for tiling a rectangle region using a brick corner Wang tile set. A brick corner Wang tile set is a special Wang tile set introduced by A. Derouet-Jourdan et al. in computer graphics in 2015 to model wall patterns texture. We have implemented a tiling algorithm using Coq proof assistant and proved its correctness. This correctness assures the existence of a tiling of any brick corner Wang tile set for any size of rectangle. The essential points of our proof are the existence of a tiling for a $2 \times 2$ rectangle and a simple induction process. Since the brick corner Wang tile is a class of infinite kinds of tile sets, it is not straightforward and there are many conditional branches to prove the correctness. The certification with Coq assures that there are no lack of conditions.

    researchmap

  • ProbeDeformer for iPad

    Genki Matsuda, Shizuo Kaji, Hiroyuki Ochiai, Yoshihiro Mizoguchi

    2014年3月

    　詳細を見る

    A simple 2D image deforming system using Dual Complex Numbers.

    [1] G.Matsuda, S.Kaji, H.Ochiai, Anti-commutative Dual Complex Numbers and 2D Rigid Transformation, Mathematical Progress in Expressive Image Synthesis, MI Lecture Note, Vol.50, pp.128-133, Kyushu University, 2013.

    その他リンク： https://github.com/KyushuUniversityMathematics/iPad-ProbeDeformer

▼全件表示

所属学協会

  • Association for Computing Machinery

  • 電子情報通信学会

  • 日本応用数理学会

  • ソフトウェア科学会

  • 情報処理学会

▼全件表示

委員歴

  • 公益社団法人九州数学教育会   会長   国内

    2019年12月 - 2020年11月   

  • 日本数学会社会連携協議会   運営委員   国内

    2017年7月 - 2019年6月   

  • 日本自動車技術会自動車制御とモデル部門委員会   委員   国内

    2017年6月 - 2019年5月   

  • 公益社団法人九州数学教育会   理事   国内

    2013年7月 - 2019年11月   

  • 特定非営利活動法人数理の翼   理事   国内

    2001年10月 - 2003年9月   

学術貢献活動

  • Organizer

    New Encounters in Spatial Intelligence, Intelligent Mobility and Mathematics Part-1 & Part-2  （ Mie University Japan ） 2023年9月

    　詳細を見る

    種別：大会・シンポジウム等 

    参加者数：50

  • 学術論文等の審査

    役割：査読

    2023年

    　詳細を見る

    種別：査読等 

    外国語雑誌　査読論文数：2

  • 学術論文等の審査

    役割：査読

    2022年

    　詳細を見る

    種別：査読等 

    外国語雑誌　査読論文数：2

  • 学術論文等の審査

    役割：査読

    2021年

    　詳細を見る

    種別：査読等 

    外国語雑誌　査読論文数：2

    国際会議録　査読論文数：1

  • Program Committee 国際学術貢献

    SCSS2020, The 9th International Symposium on Symbolic Computation Software Science  （ Gammarth Tunisia ） 2020年9月

    　詳細を見る

    種別：大会・シンポジウム等 

▼全件表示

共同研究・競争的資金等の研究課題

  • 物理的・確率的システムの検証を支える形式的基盤の構築

    2022年4月 - 2026年3月

    日本 

    　 詳細を見る

    担当区分：研究分担者 

    今日, コンピュータプログラムは, デジタル情報の操作やそのネットワークに加えて, 外界との相互作用を行うため, プログラムの検証には, 形式論理と離散数学だけでなく, 実解析や確率論や幾何学などの数学が必要となり, プログラムの様々な副作用の厳密な検証が困難になっている. その複雑さを抑えるためには, プログラムの意味論の基礎的な研究と, 高度な数学に一貫性のある形式表現を与える統合的な研究の双方が必要である. 本研究では, 定理証明支援系Coq上, 実解析, 連続確率, 剛体幾何を形式化し, モナドと等式推論に基づいて, 形式的基盤の構築とその評価を行う.

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

    2017年4月 - 2020年3月

    九州大学 

    　 詳細を見る

    担当区分：研究代表者 

    高信頼ソフトウェア開発の基礎となる数理論理学や離散数学, 特に計算機による自動検証可能な形式証明を意識した, 関係計算による証明を用いた数学体系を広げること.

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

    研究課題/領域番号：17K05346  2017年 - 2019年

    日本学術振興会  科学研究費助成事業  基盤研究(C)

    　 詳細を見る

    担当区分：研究代表者  資金種別：科研費

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

    2013年4月 - 2015年3月

    日本学術振興会 

    　 詳細を見る

    担当区分：研究代表者 

    本研究は離散構造体の変換による計算理論をグラフ変換, セルオートマトン, 言語理論の一般化として定式化するものである.　特に, 関係計算を用いて形式的な自動検証可能な証明を与えながら理論を構築する. 離散構造物の変換(変形)による計算理論の構築は, それそのものでも数学的対象として興味深いが, 全く新しい仕組みの計算機の実現へのヒントを与える可能性もあり, 非常に将来性のある研究課題である. 「圏論」「関係計算理論」「オートマトン理論」を基盤に「グラフ」「セル」という離散構造体を利用した計算を一般化し離散構造体の変換による計算理論を形式的証明とともに研究対象として構築することが目的である.

  • 離散構造体の変換による計算理論と証明の自動検証

    研究課題/領域番号：25610034  2013年 - 2014年

    科学研究費助成事業  挑戦的萌芽研究

    　 詳細を見る

    担当区分：研究代表者  資金種別：科研費

▼全件表示

教育活動概要

  • 計算機数学に関する学部科目, 教職免許情報に関わる教職科目, 学部や大学院における数学講究などを担当している. 数理・データサイエンス教育研究センターの活動として, 企業とともに, PBL科目の実施等を行なっている.

担当授業科目

  • 複素関数論

    2024年10月 - 2025年3月   後期

  • 情報社会における企業とその職業観

    2024年4月 - 2025年3月   通年

  • 数理・データサイエンス活用PBL

    2024年4月 - 2024年9月   前期

  • 情報科指導法Ⅱ

    2024年4月 - 2024年9月   前期

  • 情報数学特論１

    2023年10月 - 2024年3月   後期

▼全件表示

FD参加状況

  • 2022年4月   役割：参加   名称：数理学府FD

    主催組織：部局

  • 2021年7月   役割：参加   名称：数理学府FD

    主催組織：部局

  • 2019年7月   役割：参加   名称：数理学府教員会議

    主催組織：部局

  • 2019年3月   役割：参加   名称：数理学府教員会議

    主催組織：部局

  • 2018年7月   役割：参加   名称：数理学府教員会議

    主催組織：部局

▼全件表示

他大学・他機関等の客員・兼任・非常勤講師等

  • 2011年  釜山国立大学  区分:集中講義  国内外の区分:国外 

  • 2009年  鹿児島大学理学部  区分:集中講義  国内外の区分:国内 

  • 2008年  放送大学大学院  区分:客員教員  国内外の区分:国内 

  • 2005年  愛媛大学理学部  区分:集中講義  国内外の区分:国内 

  • 2003年  島根大学総合理学部  区分:集中講義  国内外の区分:国内 

▼全件表示

その他教育活動及び特記事項

  • 2016年  その他特記事項  城西大学理学部数学科講演会「計算機を用いて数学の問題を解くということ」(於.城西大学東京紀尾井町キャンパス, 坂戸キャンパス)

    　詳細を見る

    城西大学理学部数学科講演会「計算機を用いて数学の問題を解くということ」(於.城西大学東京紀尾井町キャンパス, 坂戸キャンパス)

社会貢献・国際連携活動概要

  • アジア開発銀行第30回福岡大会・インターネット環境支援プロジェクト指導者(1997年)
    認定NPO法人数理の翼理事(2001-2003年)
    九州数学教育会理事(2013-2020年)

社会貢献活動

  • 九州大学キャンパスウォーク

    九州大学  九州大学理学部棟・情報基盤センター  2023年2月

    　詳細を見る

    対象：社会人・一般,　学術団体,　企業,　市民団体,　行政機関

    種別：その他

    福岡県朝倉市立秋月中学校中学生への スパコンITO見学, 若手数学研究者との座談会など.

  • Campus Walk in 九州大学

    朝倉市立秋月中学校  2023年2月

    　詳細を見る

    対象：幼稚園以下,　小学生,　中学生,　高校生

    種別：その他

  • Campus Walk in 九州大学

    朝倉市立秋月中学校  2023年2月

    　詳細を見る

    種別：その他

    researchmap

  • 九州大学キャンパスウォーク

    九州大学  九州大学理学部棟・情報基盤センター  2023年2月

    　詳細を見る

    種別：その他

    福岡県朝倉市立秋月中学校中学生への スパコンITO見学, 若手数学研究者との座談会など.

    researchmap

  • 講義「バーコードの数理」

    福岡県立香住ヶ丘高校  2019年12月

    　詳細を見る

    対象：幼稚園以下,　小学生,　中学生,　高校生

    種別：セミナー・ワークショップ

▼全件表示

メディア報道

  • 教育最前線（座談会） 新聞・雑誌

    西日本新聞  2004年2月

    　詳細を見る

    教育最前線（座談会）

外国人研究者等の受け入れ状況

  • University college London

    受入れ期間： 2018年6月 - 2018年9月   （期間）：1ヶ月以上

    国籍：グレートブリテン・北アイルランド連合王国(英国)

    専業主体：日本学術振興会

  • Pusan National University

    受入れ期間： 2017年10月 - 2018年2月   （期間）：1ヶ月以上

    国籍：大韓民国

    専業主体：その他

  • Pusan National University

    受入れ期間： 2012年12月 - 2013年3月   （期間）：1ヶ月以上

    国籍：大韓民国

    専業主体：その他

海外渡航歴

  • 2014年11月

    滞在国名1：大韓民国   滞在機関名1：釜山国立大学

  • 2005年6月

    滞在国名1：カナダ   滞在機関名1：McMaster University

  • 1998年3月 - 1999年1月

    滞在国名1：グレートブリテン・北アイルランド連合王国(英国)   滞在機関名1：マンチェスター工科大学

学内運営に関わる各種委員・役職等

  • 2018年4月 - 2019年3月   全学 基幹教育情報科目実施班員

  • 2014年4月 - 2015年3月   全学 ハラスメント対策委員会

  • 2013年4月 - 2025年3月   学府 数理学府経理委員

  • 2011年4月 - 2025年3月   研究所 マス・フォア・インダストリ研究所計算機委員

  • 2010年4月 - 2016年3月   学部 理学系総合研究教育棟移転作業情報ネットワークチーム委員

▼全件表示