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

2013 年度 研究成果報告書

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

研究課題

  • PDF
研究課題/領域番号 22300285
研究種目

基盤研究(B)

配分区分補助金
応募区分一般
研究分野 教育工学
研究機関信州大学

研究代表者

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

研究分担者 和崎 克己  信州大学, 工学部, 教授 (70271492)
KPAULINE Naomi  信州大学, 工学部, 准教授 (40283238)
山崎 浩  信州大学, 工学部, 助教 (00293522)
岡崎 裕之  信州大学, 工学系研究科, 助教 (50432167)
連携研究者 布田 裕一  北陸先端科学技術大学院大学, 情報科学研究科, 准教授 (50706223)
荒井 研一  東京理科大学, 理工学部, 助教 (60645290)
研究期間 (年度) 2010-04-01 – 2014-03-31
キーワードeラーニング / プルーフチェッカ
研究概要

Mizarシステムは形式化記述された定理証明の正しさを機械的に検証するプルーフチェッカーと呼ばれるソフトウェアである.申請者らは,これを用いた数学定理の形式化研究とそのライブラリ編纂を行う国際プロジェクトを推進してきたが,その成果を教育に利用するためe-learning用のCMSにこのMizarシステムを組み込むモジュールを試作し, 大学院教育でその試験運用も進めてきた.本研究ではその成果をもとに,e-learningによる論理思考,数理的思考訓練の実用システムとその教材開発を行った。これは「学生の論理思考能力の育成」という高等教育の深刻な課題の一つに有効な解決手段の提供するものになっている.

  • 研究成果

    (49件)

すべて 2013 2012 2011 2010 その他

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

  • [雑誌論文] Differential Equations on Functions from R into Real Banach Space2013

    • 著者名/発表者名
      Keiko Narita, Noboru Endou,Yasunari Shidama
    • 雑誌名

      Formalized Mathematics

      巻: 21(4) ページ: 261-272

    • DOI

      10.2478/forma-2013-0028

    • 査読あり
  • [雑誌論文] Submodule of free Z-module2013

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

      Formalized Mathematics

      巻: 21(4) ページ: 273-282

    • DOI

      10.2478/forma-2013-0029

    • 査読あり
  • [雑誌論文] Isometric Differentiable Functions on Real Normed Space2013

    • 著者名/発表者名
      Yuichi Futa, Noboru Endou, Yasunari Shidama
    • 雑誌名

      Formalized Mathematics

      巻: 21(4) ページ: 249-260

    • DOI

      10.2478/forma-2013-0027

    • 査読あり
  • [雑誌論文] Formulation of Cell Petri Nets2013

    • 著者名/発表者名
      Mitsuru Jitsukawa, Pauline N. Kawamoto, Yasunari Shidama
    • 雑誌名

      Formalized Mathematics

      巻: 21(4) ページ: 241-247

    • DOI

      10.2478/forma-2013-0026

    • 査読あり
  • [雑誌論文] The Linearity of Riemann Integral on Functions from R into Real Banach Space2013

    • 著者名/発表者名
      Keiko Narita, Noboru Endou, Yasunari Shidama
    • 雑誌名

      Formalized Mathematics

      巻: 21(3) ページ: 185-191

    • DOI

      10.2478/forma-2013-0020

    • 査読あり
  • [雑誌論文] Formalization of the Advanced Enc ryption Standard. Part I2013

    • 著者名/発表者名
      Kenichi Arai, Hiroyuki Okazaki
    • 雑誌名

      Formalized Mathematics

      巻: 21(3) ページ: 171-184

    • DOI

      10.2478/forma-2013-0019

    • 査読あり
  • [雑誌論文] Double Sequences and Limits2013

    • 著者名/発表者名
      Noboru Endou, Hiroyuki Okazaki, Yasunari Shidama
    • 雑誌名

      Formalized Mathematics

      巻: 21(3) ページ: 163-170

    • DOI

      10.2478/forma-2013-0018

    • 査読あり
  • [雑誌論文] Isomorphisms of Direct Products of Cyclic Groups of Prime-power Order2013

    • 著者名/発表者名
      Hiroshi Yamazaki, Hiroyuki Okazaki, Kazuhisa Nakasho , Yasunari Shidama
    • 雑誌名

      Formalized Mathematics

      巻: 21(3) ページ: 207-211

    • DOI

      10.2478/forma-2013-0022

    • 査読あり
  • [雑誌論文] Riemann Integral of Funtions from R into Real Banach Space2013

    • 著者名/発表者名
      Keiko Narita, Noboru Endou, Yasunari Shidama
    • 雑誌名

      Formalized Mathematics

      巻: 21(2) ページ: 145-152

    • DOI

      10.2478/forma-2013-0016

    • 査読あり
  • [雑誌論文] Differentiation in Normed Spaces2013

    • 著者名/発表者名
      Noboru Endou, Yasunari Shidama
    • 雑誌名

      Formalized Mathematics

      巻: 21(2) ページ: 95-102

    • DOI

      10.2478/forma-2013-0011

    • 査読あり
  • [雑誌論文] N-dimensional Binary Vector Spaces2013

    • 著者名/発表者名
      Kenichi Arai, Hiroyuki Okazaki, Yasunari Shidama
    • 雑誌名

      Formalized Mathematics

      巻: 21(2) ページ: 75-81

    • DOI

      10.2478/forma-2013-0008

    • 査読あり
  • [雑誌論文] Constructing Binary Huffman Tree2013

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

      Formalized Mathematics

      巻: 21(2) ページ: 133-143

    • DOI

      10.2478/forma-2013-0015

    • 査読あり
  • [雑誌論文] Gaussian Integers2013

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

      Formalized Mathematics

      巻: 21(2) ページ: 115-125

    • DOI

      10.2478/forma-2013-0013

    • 査読あり
  • [雑誌論文] Random Variables and Product of Probability Spaces2013

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

      Formalized Mathematics

      巻: 21(1) ページ: 33-39

    • DOI

      10.2478/forma-2013-0003

    • 査読あり
  • [雑誌論文] Isomorphisms of Direct Products of Finite Commutative Groups2013

    • 著者名/発表者名
      Hiroyuki Okazaki, Hiroshi Yamazaki, Yasunari Shidama
    • 雑誌名

      Formalized Mathematics

      巻: 21(1) ページ: 65-74

    • DOI

      10.2478/forma-2013-0007

    • 査読あり
  • [雑誌論文] The C^k Space2013

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

      Formalized Mathematics

      巻: 21(1) ページ: 25-31

    • DOI

      10.2478/forma-2013-0002

    • 査読あり
  • [雑誌論文] Formal Definition of Probability on Finite and Discrete Sample Space for Proving Security of Cryptographic Systems Using Mizar2013

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

      Artificial Intelligence Research

      巻: 2(4) ページ: 37-48

    • DOI

      10.5430/air.v2n4p37

    • 査読あり
  • [雑誌論文] Formalization of Definitions and Theorems Related to an Elliptic Curve Over a Finite Prime Field by Using Mizar2013

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

      Journal of Automated Reasoning

      巻: 50(2) ページ: 161-172

    • DOI

      10.1007/s10817-012-9265-2

    • 査読あり
  • [雑誌論文] On L1 Space Formed by Complex-Valued Partial Functions2012

    • 著者名/発表者名
      Yasushige Watase, Noboru Endou, Yasunari Shidama
    • 雑誌名

      Formalized Mathematics

      巻: 20(4) ページ: 349-357

    • DOI

      10.2478/v10037-012-0039-4

    • 査読あり
  • [雑誌論文] Isomorphisms of Direct Product of Finite Cyclic Groups2012

    • 著者名/発表者名
      Kenichi Arai, Hiroyuki Okazaki, Yasunari Shidama
    • 雑誌名

      Formalized Mathematics

      巻: 20(4) ページ: 343-347

    • DOI

      10.2478/v10037-012-0038-5

    • 査読あり
  • [雑誌論文] Contracting Mapping on Normed Linear Space2012

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

      Formalized Mathematics

      巻: 20(4) ページ: 291-301

    • DOI

      10.2478/v10037-012-0035-8

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

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

      Formalized Mathematics

      巻: 20(4) ページ: 257-280

    • DOI

      10.2478/v10037-012-0033-x

    • 査読あり
  • [雑誌論文] Banach's Continuous Inverse Theorem and Closed Graph Theorem2012

    • 著者名/発表者名
      Hideki Sakurai, Hiroyuki Okazaki, Yasunari Shidama
    • 雑誌名

      Formalized Mathematics

      巻: 20(4) ページ: 271-274

    • DOI

      10.2478/v10037-012-0032-y

    • 査読あり
  • [雑誌論文] Quotient Module of Z-module2012

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

      Formalized Mathematics

      巻: 20(3) ページ: 205-214

    • DOI

      10.2478/v10037-012-0024-y

    • 査読あり
  • [雑誌論文] Extended Euclidean Algorithm and CRT Algorithm2012

    • 著者名/発表者名
      Hiroyuki Okazaki, Yosiki Aoki, Yasunari Shidama
    • 雑誌名

      Formalized Mathematics

      巻: 20(2) ページ: 175-179

    • DOI

      10.2478/v10037-012-0020-2

    • 査読あり
  • [雑誌論文] Formalization of the Data Encryption Standard2012

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

      Formalized Mathematics

      巻: 20(2) ページ: 125-146

    • DOI

      10.2478/v10037-012-0016-y

    • 査読あり
  • [雑誌論文] Higher Order Partial Differentiation2012

    • 著者名/発表者名
      Noboru Endou, Hiroyuki Okazaki, Yasunari Shidama
    • 雑誌名

      Formalized Mathematics

      巻: 20(2) ページ: 113-124

    • DOI

      10.2478/v10037-012-0015-z

    • 査読あり
  • [雑誌論文] Operations of Points on Elliptic Curve in Projective Coordinates2012

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

      Formalized Mathematics

      巻: 20(1) ページ: 87-95

    • DOI

      10.2478/v10037-012-0012-2

    • 査読あり
  • [雑誌論文] 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

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

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

      Formalized Mathematics

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

    • DOI

      10.2478/v10037-012-0009-x

    • 査読あり
  • [雑誌論文] Morphology for Image Processing. Part I2012

    • 著者名/発表者名
      Hiroshi Yamazaki, Czeslaw Bylinski, Katsumi Wasaki
    • 雑誌名

      Formalized Mathematics

      巻: 20(1) ページ: 61-63

    • DOI

      10.2478/v10037-012-0008-y

    • 査読あり
  • [雑誌論文] 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

    • 査読あり
  • [雑誌論文] Functional SpaceC(Ω), C_0(Ω)2012

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

      Formalized Mathematics

      巻: 20(1) ページ: 15-22

    • DOI

      10.2478/v10037-012-0003-3

    • 査読あり
  • [雑誌論文] 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

    • 査読あり
  • [雑誌論文] More on the Cont inuity of Real Functions2012

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

      Formalized Mathematics

      巻: 19(4) ページ: 233-239

    • DOI

      10.2478/v10037-011-0032-3

    • 査読あり
  • [雑誌論文] Partial Differentiation, Differentiation and Continuity on n-Dimensional Real Normed Linear Spaces2011

    • 著者名/発表者名
      Takao Inoue, Adam Naumowicz, Noboru Endou, Yasunari Shidama
    • 雑誌名

      Formalized Mathematics

      巻: 19(2) ページ: 65-68

    • DOI

      10.2478/v10037-011-0011-8

    • 査読あり
  • [雑誌論文] Banach Algebra of Bounded Complex-Valued Functionals2011

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

      Formalized Mathematics

      巻: 19(2) ページ: 121-126

    • DOI

      10.2478/v10037-011-0019-0

    • 査読あり
  • [雑誌論文] Differentiable Functions into Real Normed Spaces2011

    • 著者名/発表者名
      Hiroyuki Okazaki, Noboru Endou, Keiko Narita, Yasunari Shidama
    • 雑誌名

      Formalized Mathematics

      巻: 19(2) ページ: 69-72

    • DOI

      10.2478/v10037-011-0012-7

    • 査読あり
  • [雑誌論文] 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

    • 査読あり
  • [雑誌論文] Cartesian Products of Family of Real Linear Spaces2011

    • 著者名/発表者名
      Hiroyuki Okazaki, Noboru Endou, Yasunari Shidama
    • 雑誌名

      Formalized Mathematics

      巻: 19(1) ページ: 51-59

    • DOI

      10.2478/v10037-011-0009-2

    • 査読あり
  • [雑誌論文] Formalization of Integral Linear Space2011

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

      Formalized Mathematics

      巻: 19(1) ページ: 61-64

    • DOI

      10.2478/v10037-011-0010-9

    • 査読あり
  • [雑誌論文] Moreon Continuous Functions on Normed Linear Spaces2011

    • 著者名/発表者名
      Hiroyuki Okazaki, Noboru Endou, Yasunari Shidama
    • 雑誌名

      Formalized Mathematics

      巻: 19(1) ページ: 45-49

    • DOI

      10.2478/v10037-011-0008-3

    • 査読あり
  • [雑誌論文] Riemann Integral of Functions R into C2010

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

      Formalized Mathematics

      巻: 18(4) ページ: 201-206

    • DOI

      10.2478/v10037-010-0024-8

    • 査読あり
  • [雑誌論文] Differentiation of Vector-Valued Functions on n-Dimensional Real Normed Linear Spaces2010

    • 著者名/発表者名
      Takao Inoue, Noboru Endou, Yasunari Shidama
    • 雑誌名

      Formalized Mathematics

      巻: 18(4) ページ: 207-212

    • DOI

      10.2478/v10037-010-0025-7

    • 査読あり
  • [雑誌論文] 電子テキストを利用した情報リテラシ教育の実施結果収集を行う大規模工-ジェントベースシステムの開発と評価2010

    • 著者名/発表者名
      田中敬一, 和崎克己
    • 雑誌名

      教育システム情報学会誌

      巻: 27(3) ページ: 267-279

    • 査読あり
  • [学会発表] Content Development for Distance Education in Advanced University Mathematics Using Mizar2013

    • 著者名/発表者名
      Takaya IDO, Hiroyuki OKAZAKI, Hiroshi YAMAZAKI, Pauline Naomi, KAWAMOTO, Katsumi WASAKI, Yasunari SHIDAMA
    • 学会等名
      Proceedings of the 2013 International Conference on e-Learning,e-Business, Enterprise Information Systems, and e-Government(EEE'13)
    • 発表場所
      Las Vegas, Nevada, USA
    • 年月日
      20130722-25
  • [学会発表] 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)
    • 発表場所
      Las Vegas, Nevada, USA (DOI : 10.1109/ITNG.2011.8)
    • 年月日
      20110411-13
  • [備考]

    • URL

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

URL: 

公開日: 2015-06-25  

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

Powered by NII kakenhi