| 研究課題/領域番号 |
22300285
|
|---|
| 研究機関 | 信州大学 |
|---|
研究代表者 |
師玉 康成 信州大学, 工学部, 教授 (20226129)
|
|---|
| 研究分担者 |
山崎 浩 信州大学, 工学部, 助教 (00293522)
K PAU line Naomi 信州大学, 工学部, 准教授 (40283238)
岡崎 裕之 信州大学, 理工学研究科, 助教 (50432167)
和崎 克己 信州大学, 工学部, 教授 (70271492)
|
|---|
| 研究期間 (年度) |
2010-04-01 – 2014-03-31
|
| キーワード | e-learning / 形式化数学 / 定理証明支援系 / Mizar / 論理思考 / moodle |
|---|
| 研究概要 |
本年度はこの課題の計画の最終年度であり，これまでに形式化･教材化したものを整理・体系化するとともに，それによるe-learning教材システムを申請者が所属する大学の学科の全学部学生，専攻の修士課程全学生を対象に運用，実証実験を行ないシステムの改善を行なった． これと並行して申請者らが主催した定理証明支援系の研究会や国際学会等でその研究成果公表を行った． 本システムや手法の紹介，専門研究者との意見交換などによりシステムの改善，さらには利用普及促進の方策を検討した．
申請者が開発した証明記述問題と計算機によるチェックを利用した論理思考訓練用の教材システムとその手法は，数学,情報工学に限らず，工学全般，さらには証明記述などを通じの論理思考訓練が必要な学術分野の教育に広く適用可能である. また教育機関所属の学生に限らず，企業技術者の訓練にも有効と考えられるためこれへの展開を目指してその準備を進めた．その教材の土台になる数学定理の形式化ライブラリ構築については昨年度に引き続きその充実化を進めた．解析系では多変数関数の微積分，微分方程式論，関数空間論に関する基本定理を,代数系ではZ-加群や有限アーベル群，工学系では広範囲に利用され重要な最適化理論，離散系数学では，木構造を含むグラフ理論，数論アルゴリズム，さらには暗号などの計算機処理プログラムの動作の形式手法による正当性検証法などの研究を展開した．
申請者らが所属する大学では，全学的な汎用のe-learningシステムが既に稼働しており，申請者らが開発した手法やシステムをこの全学システムにプラグインとして組み込むために必要な諸作業を行なった．さらに，上記のe-learningシステムはCMSとし広く利用されるオープンソースウェアのMoodleをもとに作成されているので，他機関への本教材システムの提供を行うための準備も行った．
|
| 現在までの達成度 (区分) |
理由
25年度が最終年度であるため、記入しない。
|
| 今後の研究の推進方策 |
25年度が最終年度であるため、記入しない。
|
