九州大学-研究者情報 [溝口佳寛 (教授) マス・フォア・インダストリ研究所応用理論研究部門]

物理的・確率的システムの検証を支える形式的基盤の構築
2022.04～2026.03, 代表者：Affeldt Reynald, 産業技術総合研究所, 日本

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

関係計算の形式化を用いた数学とソフトウェア検証のための理論構築
2017.04～2020.03, 代表者：溝口佳寛, 九州大学, 九州大学
高信頼ソフトウェア開発の基礎となる数理論理学や離散数学, 特に計算機による自動検証可能な形式証明を意識した, 関係計算による証明を用いた数学体系を広げること..

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

デジタル映像数学の構築と表現技術の革新 (Mathematics for Expressive Image Synthesis)
2010.10～2015.03, 代表者：安生健一, オー・エル・エム・デジタル, JST(科学技術振興機構)(日本)
コンピュータグラフィックスに代表されるデジタル映像の応用は拡大の一途をたどっています。本研究は、作りやすさや効率を重視しつつ、従来よりさらに豊かな表現力を持つ映像の制作を可能にするために、デジタル映像表現を対象とする新たな数学分野形成の礎を築くことを目指します。特に、人間の動作や表情と流体の表現に焦点をあて、これらの映像表現の数学的特徴づけと、作り手の意図をより的確に反映できる数学モデルの構築を推進します。 .

研究業績

主要原著論文

全てを見る→

1.	Alex Derouet-Jourdan, Shizuo Kaji, Yoshihiro Mizoguchi, A linear algorithm for brick Wang tiling, Japan J. Indust. Appl. Math., https://doi.org/10.1007/s13160-019-00369-z, 1-13, 2019.04, [URL].
2.	Toshiaki Matsushima, Yoshihiro Mizoguchi, Alexandre Derounet-Jourdan, Verification of a brick Wang tiling algorithm, 7th International Symposium on Symbolic Computation in Software Science (SCSS2016), doi.org/10.29007/2m5f, 39, 107-116, 2016.03, [URL].
3.	MItsuhiro Kondo, Takuya Matsuo, Yoshihiro Mizoguchi, Hiroyuki Ochiai, A Mathematica module for Conformal Geometric Algebra and Origami Folding, 7th International Symposium on Symbolic Computation in Software Science (SCSS2016), doi.org/10.29007/6fc5, 39, 60-80, 2016.03, [URL].
4.	Mitsugu Hirasaka, Kyoung-Tark Kim, Yoshihiro Mizoguchi, Uniqueness of Buston Hadamard matrices of small degrees, Journal of Discrete Algorithms, doi:10.1016/j.jda.2015.05.009, 34, 70-77, 2015.06, [URL].
5.	Yuki Ikeda, yasunari fukai, Yoshihiro Mizoguchi, A Property of Random Walks on a Cycle Graph, Pacific Journal of Mathematics for Industry, DOI:10.1186/s40736-015-0015-3 , 7, 3, 2015.12, [URL].
6.	Hisaharu Tanaka, Issei Sakashita, Shuichi Inokuchi, Yoshihiro Mizoguchi, Formal Proofs for Automata and Sticker Systems, Proc. of First International Symposium on Computing and Networking, 10.1109/CANDAR.2013.100, 2013.12, [URL].
7.	Shuichi Inokuchi, Takahiro Ito, Mitsuhiko Fujio, Yoshihiro Mizoguchi, A formulation of Composition for Cellular Automata on Groups, IEICE Transactions on Information and Systems, E97- D, 3, 448-454, 2014.03, [URL].
8.	Shizuo Kaji, Sanpei Hirose, Yoshihiro Mizoguchi, Ken Anjyo, Mathematical Analysis on Affine Maps for 2D Shape Interpolation, Proceedings of SCA2012 (ACM/Eurographics Symposium on Computer Animation 2012), 71-76, 2012.07, [URL].
9.	Yoshihiro Mizoguchi, K.K.K.R. Perera, Bipartition of graphs based on the normalized cut and spectral methods, Part I: Minimum normalized cut, Journal of Math-for-Industry, 5, 59-72, 2013.04, [URL].
10.	T. Ito, M. Fujio, S. Inokuchi, Y. Mizoguchi, Composition, union and division of cellular automata on groups , Proc. of the 16th International Workshop on Cellular Automata and Discrete Complex Systems, Automata2010, 255-264, 2010.06.
11.	K.K.K.R.Perera, Yoshihiro Mizoguchi, Implementation of Haskell Modules for Automata and Sticker Systems, Journal of Math-for-industory, 1, 51-56, 2009.04, [URL].
12.	S. Inokuchi, Y. Mizoguchi, H. Y. Lee and Y. Kawahara, Periodic behaviors of quantum cellular automata, Bull. of Informatics and Cybernetics, Vol.40(2008), pp.17-50. , 2008.12.
13.	T. Ito, S. Inokuchi, Y. Mizoguchi, An abstract collesion system, Automata-2008, Theory and Applications of Cellular Automata, Luniver Press, pp.339-355., 2008.06.
14.	Y. Mizoguchi and P. Loucopoulos, Formalizing the Definition and Evolution of Models in a Repository, Proc. of the 5th RelMiCS (Seminar on Relational Methods in Computer Science), Quebec(Canada), pp.203-209, 2000.01.
15.	Y. Mizoguchi, Properties of graphs preserved by relational graph rewritings, Journal of Information Science, Vol.119,pp.289-299, 1999.01.
16.	溝口佳寛, 暗号化電子メールシステムの動向, 情報の科学と技術, Vol.46, pp.282-287, 1996.01.
17.	Yoshihiro Mizoguchi, Yasuo Kawahara, Relational Graph Rewritings, Theoretical Computer Science, 10.1016/0304-3975(94)00076-U, 141, 1-2, 311-328, 1995.01, [URL].
18.	Yoshihiro Mizoguchi, A Graph Structure over the Category of Sets and Partial Functions, Cahiers de topologie et g'eom'etrie diff'erentielle cat'egoriques, 34, 2-12, 1993.01, [URL].
19.	Yoshihiro Mizoguchi, Powerset Monad, Filter Monad and Primefilter Monad in the Category of Sets with Monoid Actions, Bull. of Informatics and Cybernetics, 21, 83-95, 1985.01.

主要総説, 論評, 解説, 書評, 報告書等

全てを見る→

1.	溝口佳寛, 論理と計算について考えた人たち, 数学セミナー, 2019年1月号, pp.57-61, 2018.12.
2.	Bob Anderssen, Philip Broadbridge, Yasuhide Fukumoto, Naoyuki Kamiyama, Yoshihiro Mizoguchi, Konrad Polthier, OSAMU SAEKI, The Role and Importance of Mathematics in Innovation, Proceedings of the Forum "Math-for-Industry" 2015, Mathematics for Industry 25, Springer, 2016.04, [URL].
3.	溝口佳寛, 田上真, ケプラー予想の計算機による証明と検証について, 数学セミナー, 2014年12月号, pp.48-54, 2014.12, [URL], 1600年代からの大問題ケプラー予想は1998年にHalesによって証明解決されたが, その証明の正当性を誰も検証出来なかった. そして, それから10年以上の時を経て, Hales自らの手で形式証明支援系を用いケプラー予想の計算機による証明と検証が2014年8月に与えられた. 本稿はその計算機による証明と検証の解説記事である..
4.	Yoshihiro Mizoguchi, Theory of Automata, Mathematics for Industry, Vol.5, pp.337-348, 2014.07, [URL].
5.	溝口佳寛, Jacques Garrigue, 萩原学, Reynald Affeldt, 高信頼な理論と実装のための定理証明および定理証明器, Kyushu University, 2015.03, [URL].
6.	溝口佳寛, オートマトン理論, その応用と抽象化, MI Lecture Note Series, Vol.46, 科学・技術の研究課題への数学アプローチ --数学モデリングの基礎と展開--, 九州大学, 2013.02, [URL].
7.	河原康雄・溝口佳寛, 有限オートマトンと正則表現, 電子情報通信学会・知識ベース「知識の森」, , 2011.03, [URL].

主要学会発表等

全てを見る→

1.	Yoshihiro Mizoguchi, A Coq Library for the Theory of Realational Calculus, Workshop on Formalization of Applied Mathematical Systems, 2016.09, [URL].
2.	Mohammad Deni Akbar, Yoshihiro Mizoguchi, Fuzzy Functional and Implication Dependency using Relational Calculus, The Asian Mathematical Conference (AMC2016), 2016.07, [URL].
3.	Yoshihiro Mizoguchi, Hiroyuki Ochiai, Symbolic Computations in Conformal Geometric Algebra for Three Dimensional Origami Folds, First International Workshop on Computational Origami and Applications, 2016.07, [URL].
4.	Yoshihiro Mizoguchi, Theory of Relational Calculus and its formalization, Universal Structures in Mathematics and Computing, 2016.06, [URL].
5.	溝口佳寛, 田中久治, Coqによる初等幾何の証明方法について, 日本数式処理学会, 2015.06, [URL].
6.	溝口佳寛, 松嶋聡昭, 田中久治, 井口修一, Coq関係計算ライブラリの開発と写像の性質の証明, 日本数式処理学会, 2015.06, [URL].
7.	Mohamad Deni Akbar, Yoshihiro Mizoguchi, Relational Database Model Using Relational Calculus, 7th International Conference on Soft Computing and Intelligent Systems, 2014.12, [URL].
8.	溝口佳寛, 田中久治, 坂下一生, 井口修一, 有限オートマトンとスティッカー系に関する Coq による形式証明について, 日本数学会2014年度年会, 2014.03, [URL], 有限オートマトンを構成する演算子や文字列の(無限) 集合をCoq 証明支援系を用いて形式的に定義しました. ここでは, Ssreflect (Small Scale Reflection Extension for the Coq system) も利用します. スティッカー系はPăun とRozenberg により1998 年に紹介されたDNA計算のための形式モデルです. 彼らは有限オートマトンと同等の能力を持つスティッカー系を構成する具体的な構成方法を示し, スティッカー系の計算能力が有限オートマトンのそれを含むことを示しました. しかし, その構成方法には小さな誤りがありました. それを修正した構成方法を示すことと同時に私たちの構成方法の正当性に対して,コンピュータで検証可能な形式的証明を与えることが本研究の目的です. 現在までに, 諸性質を形式証明するための有限オートマトンとスティッカー系の定義や関数の形式化が出来ました. いくつかの具体例の形式的証明, Păun らの構成に誤りがあることの形式証明を含めて報告します..
9.	Yoshihiro Mizoguchi, Mathematical Aspect of Interpolation Technique for Computer Graphics, Forum "Math-for-Industry" 2012 Information Recovery and Discovery, 2012.10, [URL], In this talk, we introduce a simple mathematical framework for 2D shape interpolation methods that preserve rigidity. An interpolation technique in this framework works for given initial and target 2D shapes, which are compatibly triangulated. Focusing on the local affine maps between the corresponding triangles, we describe a global transformation as a piecewise affine map. Several existing rigid shape interpolation techniques are mathematically analyzed through this framework. Geometric transformations are fundamental concept of computer graphics and most commonly represented as square matrices. A general framework of linear combination of transformations was introduced in [Alexa2002]. We also introduce the Laplacian matrix of a graph and show some crucial properties about eigenvalues and eigenvectors in connection with image segmentations in [Shi2000] and group formations in [Takahashi2009]. .
10.	Yoshihiro Mizoguchi, Generalization of Compositions of Cellular Automata on Groups, Workshop on Algebraic Combinatorics, Sept. 2011,, 2011.09, [URL], We introduce the notion of 'Composition', 'Union' and 'Division' of cellular automata on groups. We extend the notion to general cellular automata on groups and investigated their properties. We also show our formulation contains the representation using formal power series for linear cellular automata in Manzini (1998)..
11.	田中久治,溝口佳寛,熊原啓作, 初等幾何学定理の証明におけるRegular Chainの有効性の評価, 第19回日本数式処理学会大会, 2010.06.
12.	K.K.K.R.Perrera, Y.Mizoguchi, Laplacian energy of directed graphs, International Conference on Algebraic and Geometric Combinatorics, 2010.07.
13.	T. Ito, M. Fujio, S. Inokuchi, Y. Mizoguchi, Composition, union and division of cellular automata on groups , 16th International Workshop on Cellular Automata and Discrete Complex Systems, 2010.06, [URL].
14.	岡田幸治, 井口修一, 溝口佳寛, 廣川左千男, リンク共起情報に基づく概念グラフの提案とWeb空間の解析, 第4回ネットワーク生態学シンポジウム, 2008.03.
15.	T. Ito, S. Inokuchi, Y. Mizoguchi, The abstract collesion system, Automata-2008, 2008.06.
16.	A. Mikoda, S. Inokuchi, Y. Mizoguchi, M. Fujio, The number of orbits of periodic box-ball systems , International Conference on Unconventional Computation, 2006.09.

作品・ソフトウェア・データベース等

1.	Toshiaki Matsushima, Yoshihiro Mizoguchi and Alexandre Derouet-Jourdan, A certified Wang tiling program in Coq, 2016.03, [URL], 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..
2.	Mitsuhiro Kondo , Takuya Matsuo , Yoshihiro Mizoguchi and Hiroyuki Ochiai, A Mathematica module for Conformal Geometric Algebra and Origami Folding, 2016.03, [URL], 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..
3.	Genki Matsuda, Shizuo Kaji, Hiroyuki Ochiai, Yoshihiro Mizoguchi, ProbeDeformer for iPad, 2014.03, [URL], 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..
4.	Yoshihiro Mizoguchi, Mathematica Modules for Graph Laplacians, 2013.06, [URL], GraphLaplacian.m is a Mathematica module for graph laplacians, MMGLmanual.pdf Manual for the module and Example.m Example Mathematica file..
5.	Yoshihiro Mizoguchi, Haskell Modules for Automata and Sticker Systems, 2013.06, [URL], Haskell Modules for Sticker Systems, Finite Automata and Grammers..

学会活動

所属学会名

日本自動車技術会

日本数学会

情報処理学会

ソフトウェア科学会

日本応用数理学会

電子情報通信学会

Association for Computing Machinery

学協会役員等への就任

2019.12～2020.11, 公益社団法人九州数学教育会, 会長.

2017.06～2019.05, 日本自動車技術会自動車制御とモデル部門委員会.

2017.07～2019.06, 日本数学会社会連携協議会, 運営委員.

2013.07～2019.11, 公益社団法人九州数学教育会, 理事.

2001.10～2003.09, 特定非営利活動法人数理の翼, 理事.

学会大会・会議・シンポジウム等における役割

2020.08.03～2020.08.04, 第３１回代数, 論理, 幾何と情報科学研究集会, 座長.

2020.09.10～2020.09.13, SCSS2020, The 9th International Symposium on Symbolic Computation Software Science, Program Committee.

2020.02.06～2020.02.08, 2020 Taipei International Conference on Combinatorics, Scienctific Committee.

2019.08.31～2019.09.01, 第３０回代数, 論理, 幾何と情報科学研究集会, 世話人.

2017.09.19～2017.09.19, CG技術の実装と数理2017, 実行委員.

2016.08.23～2016.08.23, 研究集会「三次元幾何モデリング評価手法の提案とソフトウェア開発」, 司会（Moderator）.

2016.06.13～2016.06.13, 研究集会「複数画像間のパターンマッチによる土木測量技術の開発」, 司会（Moderator）.

2015.10.26～2015.10.30, Forum "Math-for-Industry" 2015, 司会（Moderator）.

2015.09.25～2015.10.01, Workshop on Formalization of Applied Mathematical Systems, 座長（Chairmanship）.

2015.12.03～2015.12.05, 研究集会「高信頼な理論と実装のための定理証明および定理証明器」, 座長（Chairmanship）.

2004.03.15～2004.03.15, 情報処理学会九州支部火の国情報シンポジウム, 座長（Chairmanship）.

2016.07.09～2016.09.21, CG技術の実装と数理2016, プログラム委員長.

2015.10.26～2015.10.30, Forum "Math-for-Industry" 2015 -The Role and Importance of Mathematics in Innovation-, Organized Committee.

2016.03.28～2016.03.31, The 7th International Symposium on Symbolic Computation in Software Science, Program Committee.

2014.12.03～2014.12.05, 研究集会「高信頼な理論と実装のための定理証明および定理証明器」, 幹事.

2013.10.21～2013.10.23, Mathematical Progress in Expressive Image Synthesis, Committee.

2014.01.25～2014.01.27, Korea-Japan workshop on algebra and combinatorics, Organizing committee.

2013.01.24～2013.01.26, Japan-Korea workshop on algebra and combinatorics, Organizing committee.

2013.09.09～2013.09.11, 日本応用数理学会2013年度年会, 実行委員.

学会誌・雑誌・著書の編集への参加状況

2019.01～2021.03, International Journal of Mathematics for Industry, 国際, 編集委員.

2016.08～2017.03, International Journal of Applied & Experimental Mathematics, 国際, 編集委員.

2016.07～2017.03, Malaysian Journal of Industrial and Applied Mathematics, 国際, 編集委員.

2004.03～2013.03, 電子情報通信学会英文誌特集号, 国際, 編集委員.

2007.12, Mathematical Review, 国際, Reviwer.

2003.05, 電子情報通信学会英文誌D, 国際, 査読委員.

1999.05～2003.05, 電子情報通信学会英文誌D, 国際, 編集委員.

学術論文等の審査

年度	外国語雑誌査読論文数	国際会議録査読論文数	国内会議録査読論文数	合計
2022年度	2			2
2021年度	2	1		3
2020年度	2			2
2019年度	2			2
2018年度	2			2
2017年度	2	2		4
2016年度	2	1		3
2015年度	2	3		5
2014年度	3	2		5
2013年度	3			3
2012年度	3			3
2011年度	3	1		4
2010年度	2			2
2009年度	3			3
2008年度	3			3
2007年度	2			2
2006年度	1			1
2005年度		1		1
2004年度	1		1	2
2003年度	4			4