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

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

Introduction

Yoshihiro Mizoguchi was born in Fukuoka on June 20, 1960. He received B.S. in 1983, the M.S. 1985 in Mathematics and the Dr. Sci. in 1992 in Information Systems from Kyushu University. Presently, he is a professor of Institute of Mathematics for Industry, Kyushu University at Fukuoka. His research interests are theoretical aspects in computer science, including logic of programming language, cellular automata, computer graphics, category theories and network securities.

Cf. Research Information (Kyushu Uiversity, JAPAN)

研究の背景

計算について論理的・数学的に考察する研究を行っています。1930年代 Alan Turingは「チューリング機械」と呼ばれる形式的な計算モデルを構成し、計算可能性、万能性に関する計算理論の礎を築きました。数の計算の実現に計算モデルのテープ上に記述された文字列が重要な役割を果たしました。計算モデル「有限オートマトン」の研究では1950年代に入り文字列集合の認識機械としての考察が始まり言語との重要な関係が導かれました。

その後、形式言語の研究は「自然言語の機械翻訳」「文献データベース」「人工知能」などの研究へと発展しています。数学(代数学)は「群」「環」「体」などの一種の集合上の演算を持つ代数系を対象とします。代数系はモナドと呼ばれる圏の間の関手たちにより多種の集合間の関数を演算として持つ系に一般化されます。多種代数系は「スタック」「木」「グラフ」などのプログラミングに必要なデータ構造を含みますので、多種代数系やモナドの研究成果は計算の性質を考察するための強力な武器になります。

近年の計算機の発展と普及により、社会システムは計算機(プログラム)にますます依存して来ています。システムに要求される仕様プログラムで実現し計算機で実行します。 プログラムが仕様を正しく実現していることは、数理論理学において証明定理を正しく導いていることに対応します。論理的に誤りがないプログラムのための仕様記述、開発、検証の技術は形式手法と呼ばれます。証券取引、交通網、航空宇宙工学、マイクロプロセッサなどプログラムの誤りにより多大な損失が生じるシステムに形式手法は活用されています。

最近は論理的・数学的な考察そのものにも計算機が利用され、形式手法のための数学理論の構築と実現がますます重要になっています。数の取り扱いのための文字列の研究のように、計算に必要な数学概念の計算モデルの研究を続けています。最近では、デジタル映像分野における計算のための新しい計算モデルも模索しています。

お知らせ

SICE2021でチュートリアルセッションを開催します (2021年9月8日オンライン) NEW
SICE-JSAE-AIMaP Advanced Automotive Control and Mathematics (AIMaP HP)
The 9th International Symposium on Symbolic Computation in Software Science -- In the era of Computational and Artificial Intelligence -- (SCSS2021 9/8-9/10) が開催されます. NEW
CEDEC2021チュートリアル案内 (2021年8月24日オンライン). NEW
ゲームプログラマのための数学の歩き方・クォータニオンとリー群編
ゲームプログラマのための数学の歩き方・デュアルクォータニオン編
第31回ALGI(代数, 論理, 幾何と情報科学研究集会) (9/3(木)-4(金)) が, ZOOMによりオンライン開催されました.
「マス・フォア・イノベーション卓越大学院」が文部科学省卓越大学院プログラムに採択されました. (IMI HP News)
The 9th International Symposium on Symbolic Computation in Software Science (SCSS2020)は延期(期日未定)となりました。
開講案内:モデル理論:普遍代数理論と一階述語論理(5/7 16:00開始)を掲示しました.
ホームページをリニューアルしました。
Software in Mathematics Demonstration Track in Hakata Workshop 2020が開催されました。
マス・フォア・インダストリ研究 No.17が発行されました。
代数・論理・幾何と情報科学 - 理論から実世界への展開
2020 Taipei International Conference on Combinatoricsは中止となりました。
第24回 情報・統計科学シンポジウムが開催されました。
PAGE TOP