Ibaraki University's
College of Engineering
Department of Electrical and Electronic Engineering

顔写真
Associate Professor

MIYAJIMA Keiichi


Career

  1. 山口大学工学部知能情報システム工学科 助手 1999/04/01-2006/03/31
  2. Lecturer, Faculty of Engineering, Ibaraki University. 2006/04/01-2011/03/31
  3. Associate Professor, Department of Electrical and Electronic Engineering, Faculty of Engineering, Ibaraki university 2011/04/01-Present

Academic background

  1. Shinshu University Faculty of Engineering Department of Information Engineering 1994/03 Graduated
  2. Shinshu University Graduate School, Division of Engineering 情報工学専攻 Doctor prophase 1996/03 Completed
  3. Shinshu University Graduate School, Division of Engineering システム開発工学 Doctor later 1999/03 Completed

Academic degrees

  1. 博士(工学) Shinshu University 1999/03

Current state of research and teaching activities

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

Research Areas

  1. General Mathematics (includes Probability Theory/Statistical Mathematics)
  2. Fundamental Informatics

Research keywords

  1. Formalized Mathematics

Subject of research

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

Papers

  1. Research paper (scientific journal) Joint 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. Research paper (scientific journal) Joint 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. Research paper (scientific journal) Joint 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. Research paper (other science council materials etc.) Joint 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. Research paper (other science council materials etc.) Joint 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 複素数の値を持つ有限数列に関して、その数列の和や線形性などの関連する諸定理を形式化した。

Research presentations

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

Alloted class

  1. Computer Literacy
  2. Computer Architecture
  3. Information Network
  4. 電気電子工学特別実験I
  5. 電気電子工学特別演習I

Memberships of academic societies

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