茨城大学
工学部
電気電子工学科

顔写真
准教授

宮島 啓一

ミヤジマ ケイイチ
MIYAJIMA Keiichi

経歴

  1. 山口大学工学部知能情報システム工学科 助手 1999/04/01-2006/03/31
  2. 茨城大学工学部電気電子工学科 講師 2006/04/01-2011/03/31
  3. 茨城大学工学部電気電子工学科 准教授 2011/04/01-現在

学歴

  1. 信州大学 工学部 情報工学科 1994/03 卒業
  2. 信州大学 工学系研究科 情報工学専攻 博士前期 1996/03 修了
  3. 信州大学 工学系研究科 システム開発工学 博士後期 1999/03 修了

学位

  1. 博士(工学) 信州大学 1999/03

教育・研究活動状況

形式化数学
数学の証明をコンピュータ言語化し、極めて厳密な数学の証明検証システムを構築する。

研究分野

  1. 数学一般(含確率論・統計数学)
  2. 情報学基礎

研究キーワード

  1. 形式化数学

研究テーマ

  1. Mizarを用いた暗号理論および暗号関連システムの形式化 Mizarと呼ばれる形式化言語システムを用いて、現代暗号理論ならびに現代暗号で用いられているハッシュ関数等を形式化し、安全性の検証を行う。 2014/04-現在
  2. 微分方程式論の形式化 2011/04-現在
  3. R→R^nへの関数におけるRiemann積分の形式化 R→R^nへの関数におけるRiemann積分の定義、ならびに関連諸定理の形式化 2007/04-2011/03

論文

  1. 研究論文(学術雑誌) 共著 Contracting Mapping on Normed Linear Space Keiichi Miyajima, Artur Kornilowicz and Yasunari Shidama Formalized Mathematics, 20/ 4, 295-303 2012/12 1426-2630 10.2478/v10037-012-0035-8 縮小写像と縮小写像による不動点定理の形式化、単純な積分方程式から、フレッドホルム型積分作用素の定義の形式化。
  2. 研究論文(学術雑誌) 共著 Riemann Integral of Functions from R into n-dimensional Real Normed Space. Keiichi Miyajima, Artur Kornilowicz, Yasunari Shidama Formalized Mathematics 20/ 1, 81-89 2012/08 1426-2630 10.2478/v10037-012-0011-3 実数からn次元実ノルム空間上への関数におけるリーマン積分についての形式化を行った。また同関数空間におけるリーマン積分の積分作用素の線形性に関する諸定理、ならびに関連する各種定義や定理の形式化なども行った。
  3. 研究論文(学術雑誌) 共著 Riemann Integral of Functions from R into Real Normed Space Keiichi Miyajima, Takahiro Kato, Yasunari Shidama Formalized Mathematics 19/ 1, 17-22 2011/03 10.2478/v10037-011-0003-8 実数から実ノルム空間上への関数におけるリーマン積分についての形式化を行った。また同関数空間におけるリーマン積分の積分作用素の線形性に関する諸定理の形式化なども行った。
  4. 研究論文(その他学術会議資料等) 共著 Riemann Integral of Functions R into C Keiichi Miyajima, Takahiro Kato, Yasunari Shidama Formalized Mathematics 18/ 4, 201-206 2010 10.2478/v10037-010-0024-8 実数から複素数への関数に関するリーマン積分の定義を形式化した。またそれらに関する諸定理(リーマン和の収束性や、リーマン積分の線形性など)の形式化を行った。
  5. 研究論文(その他学術会議資料等) 共著 The Sum and Product of Finite Sequences of Complex Numbers Keiichi Miyajima, Takahiro Kato Formalized Mathematics 18/ 2, 107-111 2010 10.2478/v10037-010-0014-x 複素数の値を持つ有限数列に関して、その数列の和や線形性などの関連する諸定理を形式化した。

研究発表

  1. 口頭発表(一般) 縮小写像と常微分方程式論 日本Mizar学会2012年度秋季総会 2012/10
  2. 口頭発表(一般) ノルム線形空間上の縮小写像の形式化 日本Mizar学会2011年度秋季総会 2011/11
  3. 口頭発表(一般) 実数からn次元実ノルム空間への関数に関するリーマン積分と微分の形式化 日本Mizar学会2010年度夏季総会 2010/09
  4. 口頭発表(一般) 実数から複素数への関数に関するリーマン積分の形式化 日本Mizar学会2009年度秋季総会 2009/11
  5. 口頭発表(一般) 為替レートの統計的解析 電子情報通信学会2009年基礎・境界ソサエティ大会 2009/09

担当授業科目

  1. 情報処理概論【情報リテラシー】
  2. 電子計算機工学
  3. 情報ネットワーク
  4. 電気電子工学特別実験I
  5. 電気電子工学特別演習I

所属学協会

  1. 日本Mizar学会 2007/04-現在
  2. Association of Mizar Users 2007/04-現在
  3. 電子情報通信学会 1998/05-現在
  4. 日本シミュレーション学会 2001/06-現在