• 研究課題をさがす
  • 研究者をさがす
  • KAKENの使い方
  1. 課題ページに戻る

2011 年度 実績報告書

MIZAR数学ライブラリの構築と大学数学向け高度遠隔教育用コンテンツ開発

研究課題

研究課題/領域番号 22300285
研究機関信州大学

研究代表者

師玉 康成  信州大学, 工学部, 教授 (20226129)

研究分担者 KPAULINE Naomi  信州大学, 工学部, 准教授 (40283238)
和崎 克己  信州大学, 工学部, 教授 (70271492)
岡崎 裕之  信州大学, 工学系研究科, 助教 (50432167)
山崎 浩  信州大学, 工学部, 助教 (00293522)
キーワードeラーニング / プルーフチェッカ
研究概要

23年度は,22年度に作成したe-Learning用コースマネジメントシステムMoodleにMizarシステムを組み込んだ(以下Mizar-Moodle系と略記)論理思考訓練システムの改良および教材コンテンツの追加を行った.師玉らは22年度に引き続き,多変数関数,複素関数の微積分学に関する定理とその証明の形式化記述を行い,その成果を専門学会誌論文誌Formalized Mathematics(以下F.M.と略記)に公表し,その成果をもとに教材コンテンツを作成した.同様に岡崎,山崎,和崎,カワモトらは代数学,離散数学,初等幾何に関する教材作成するため,同様に基礎定理とその証明の形式化記述を行ない,その成果をF.M.に公表した.その成果の一部を上記Mizar-Moodle系上で教材を作成した.特に暗号理論については,公開鍵暗号に利用される有限体上の楕円曲線ついての詳細な形式化記述を行なった.楕円曲線の形式化は暗号理論に限らず,代数学,幾何学においても重要なコンテンツとして利用できる.
開発された上記の教材群は
http://cai2.cs.shinshu-u.ac.jp/mizar/noodle/
で閲覧できる.
さらに,和崎らを中心に,教材システムを大規模人数の教育に用いて学習成果を自動収集するエージェントベースシステムの開発を進めた.上記Mizar-Moodle系においてこの学習成果を自動収集するシステムを運用するための準備として,他の形式検証システムを用いて実運用を行い,システムの評価を行い,その成果を複数の国際会議にて発表した.

現在までの達成度 (区分)
現在までの達成度 (区分)

2: おおむね順調に進展している

理由

ライブラリの作成,およびその教材化が順調に進んでいる.さらに教材用サーバの整備,強化を行い,本学において実際の授業(受講者が数十から百人規模を想定)での運用を行う準備が整ったことからも,おおむね順調に進展していると判断される.

今後の研究の推進方策

作成した論理思考訓練システムを実際の授業にて運用し,評価,改善を行う.実際の授業において本システムを運用する場合,受講学生が同時に接続する可能性がある.従って,24年度は特に,多数クライアント同時接続可能な論理思考訓練システムのスケーラビリティ検証と実運用ならびに運用実績に基づくシステム改善を行う.また,運用実績をもとに,教材のコンテンツ改良も行う.さらに教材作成も継続して行い,コンテンツの充実を進める.

  • 研究成果

    (14件)

すべて 2012 2011 その他

すべて 雑誌論文 (9件) (うち査読あり 9件) 学会発表 (4件) 備考 (1件)

  • [雑誌論文] Riemann Integral of Functions from R into n-dimensional Real Normed Space2012

    • 著者名/発表者名
      Keiichi Miyajima, Artur Kornilowicz, Yasunari Shidama
    • 雑誌名

      Formalized Mathematics

      巻: 20(1) ページ: 79-86

    • DOI

      10.2478/v10037-012

    • 査読あり
  • [雑誌論文] Z-modules2012

    • 著者名/発表者名
      Yuichi Futa, Hiroyuki Okazaki, Yasunari Shidama
    • 雑誌名

      Formalized Mathematics

      巻: 20(1) ページ: 47-59

    • DOI

      10.2478/v10037-012-0007-z

    • 査読あり
  • [雑誌論文] Differentiable Functions on Normed Linear Spaces2012

    • 著者名/発表者名
      Yasunari Shidama
    • 雑誌名

      Formalized Mathematics

      巻: 20(1) ページ: 31-40

    • DOI

      10.2478/v10037-012-0005-1

    • 査読あり
  • [雑誌論文] The Differentiable Functions from R into R^n2012

    • 著者名/発表者名
      Keiko Narita, Artur Kornilowic, Yasunari Shidama
    • 雑誌名

      Formalized Mathematics

      巻: 20(1) ページ: 65-71

    • DOI

      10.2478/v10037-012-0009-x

    • 査読あり
  • [雑誌論文] Banach Algebra of Comple-Valued Continuous Functionals and Space of Complex-valued Continuous Functionals with Bounded Support2012

    • 著者名/発表者名
      Katuhiko Kanazashi, Hiroyuki Okazaki, Yasunari Shidama
    • 雑誌名

      Formalized Mathematics

      巻: 20(1)(採録決定済)

    • 査読あり
  • [雑誌論文] Riemann Integral of Functions from R into Real Normed Space2011

    • 著者名/発表者名
      Keiichi Miyajima, Takahiro Kato, Yasunari Shidama
    • 雑誌名

      Formalized Mathematics

      巻: 19(1) ページ: 17-22

    • DOI

      10.2478/v10037-011-0003-8

    • 査読あり
  • [雑誌論文] Automatic Generation of SPIN Model Checking Code from UML Activity Diagrams2011

    • 著者名/発表者名
      Yutaka YAMADA, Katsumi WASAKI
    • 雑誌名

      International Journal of Advancements in Computing Technology

      巻: 3(8) ページ: 189-197

    • DOI

      10.4156/ijact.vol3.issue8.22

    • 査読あり
  • [雑誌論文] Development and Evaluation of a Large-Scale Agent-Based System for Information Literacy Education-Improving the Automatic Collection of Learning Results through Template Matching2011

    • 著者名/発表者名
      Keiichi TANAKA, Katsumi WASAKI
    • 雑誌名

      The 8th International Conference on Information Technology : New Generations (ITNG2011)

      ページ: 1-6

    • DOI

      10.1109/ITNG.2011.8

    • 査読あり
  • [雑誌論文] Automatic Generation of SPIN Model Checking Code from UML Activity Diagram and Its Application. to Web Application Design2011

    • 著者名/発表者名
      Yutaka YAMADA, Katsumi WASAKI
    • 雑誌名

      7th International Conference on Digital Content, Multimedia Technology and its Applications (IDCTA2011)

      ページ: 139-144

    • DOI

      10.1109/ITNG.2011.8

    • 査読あり
  • [学会発表] 形式化数学システムMizarによる数論アルゴリズムの検証2012

    • 著者名/発表者名
      水島大地, 青木祥希, 岡崎裕之, 師玉康成
    • 学会等名
      2012年日本応用数理学会・研究部会連合発表会
    • 発表場所
      九州大学
    • 年月日
      2012-03-09
  • [学会発表] 形成化数学記述言語Mizarによる共通鍵暗号AESの形式化2012

    • 著者名/発表者名
      今村充志, 岡崎裕之, 師玉康成
    • 学会等名
      2012年日本応用数理学会・研究部会連合発表会
    • 発表場所
      九州大学
    • 年月日
      2012-03-08
  • [学会発表] 上流設計からモデル検査プロセスまでの一貫設計検証環境~UML記述からSPINモデル検査器用プロセス定義及び線形時相論理式への自動変換手法~2011

    • 著者名/発表者名
      宮本直樹, 和崎克己
    • 学会等名
      電子情報通信学会2011年度ソフトウェアインタプライズモデリング研究会ワークショップ,信学技報(SWIM2011-19)
    • 発表場所
      東海大学(査読ありワークショップ)
    • 年月日
      2011-11-18
  • [学会発表] Mizarによる素体上の楕円曲線の形式化2011

    • 著者名/発表者名
      布田裕一, 岡崎裕之, 師玉康成
    • 学会等名
      第9回「代数学と計算」研究集会
    • 発表場所
      首都大学東京
    • 年月日
      2011-11-07
  • [備考]

    • URL

      http://cai2.cs.shinshu-u.ac.jp/mizar/moodle/

URL: 

公開日: 2013-06-26  

サービス概要 検索マニュアル よくある質問 お知らせ 利用規程 科研費による研究の帰属

Powered by NII kakenhi