2012 Fiscal Year Annual Research Report
ＭＩＺＡＲ数学ライブラリの構築と大学数学向け高度遠隔教育用コンテンツ開発
| Project/Area Number |
22300285
|
|---|
| Research Institution | Shinshu University |
|---|
Principal Investigator |
師玉 康成 信州大学, 工学部, 教授 (20226129)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
山崎 浩 信州大学, 工学部, 助教 (00293522)
K PAU line Naomi 信州大学, 工学部, 准教授 (40283238)
岡崎 裕之 信州大学, 理工学研究科, 助教 (50432167)
和崎 克己 信州大学, 工学部, 教授 (70271492)
|
|---|
| Project Period (FY) |
2010-04-01 – 2014-03-31
|
| Keywords | e-learning教材 / 形式化数学 / プルーフチェッカー / 論理思考 / 証明記述問題 / 計算機による検査 |
|---|
| Research Abstract |
Mizarは形式化記述された数学定理証明の正しさを機械的に検証するソフトウエアである．申請者らは,本研究課題でこれを用いた数学ライブラリの構築と大学数学向けの教材開発,それをe-learning用CMSに組み込んで実用する実証実験を行なってきた。
24年度は,前年度までに作成した教材コンテンツを用いて，論理思考，数理的思考訓練の実用システムを実際の授業で使用し評価，改善を行った．特に多数利用者の同時接続可能なシステムのスケーラビリティ検証と実運用ならびに運用実績に基づくシステム改善を行った．また，運用実績をもとに，教材のコンテンツ改良も行った．それらの成果はe-learning関連の学会などで公表した．さらに，研究目的を達成するため23年度に引き続き以下のライブラリ開発と教材化を行った．
(1)多変数関数，ノルム空間上の関数の微積分やルベーグ積分論などの命題群の形式化，それらを基にした教材の作成を作成した．関数解析関連では閉グラフ定理や写像定理さらに連続微分可能な関数による関数空間など基礎的な形式化ライブラリの作成を行なった．
(2) 離散数学系，暗号，アルゴリズム，並列処理等の形式化ライブラリ作成と教材の作成，23年度までに作成した教材の改良を行なった．代数系では有限群や巡回群の基礎定理，拡張ユークリッド互除法や,中国人剰余定理に関する数論アルゴリズム,また暗号については,DES暗号システムやAES暗号システムの暗号化,復号アルゴリズム,さらに,Z-加群や楕円曲線論の基礎までの形式化ライブラリを作成した．ペトリネットや並列処理回路動作の形式化と検証等を行なった．
(3) 線形代数学に関するライブラリ作成とそれを用いた教材を行なった．特に,情報工学分野に関連し,これの数理形態学的手法画像処理への応用やBOOLE変数の多重対から構成される線形空間に関してのライブラリ充実も図った．
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
大学数学の形式化ライブラリと教材作成については，工学系分野，特に，申請者らが所属する情報工学系の学科・専攻の学部生，修士課程学生を対象にした，論理思考訓練用の教材及びシステムの開発という点では，教材の質・量とも充実化しつつある．数論アルゴリズムや暗号など情報工学系分野に関わる教材に関しては，離散系数学の形式化ライブラリを用いて，今後，これをさらに充実化するため基盤が概ね整備されているものと考える． 例えば数論アルゴリズムについては計算機の処理プログラムを粗忠実に形式化表現することによって，その動作の正当性などを検証する手法を提示し，学習者にそのアルゴリズムの理解の徹底を促す演習問題作成などが可能になった。代数系についても同様で，特に暗号などに関わりの深い有限群やZ-加群や楕円曲線論などの基礎理論の形式化ライブラリ作成が進んだ。今後はガロア理論その他の形式化，教材化が課題となっている．一方，情報工学に限らず，工学系一般の学部生，修士課程学生の基礎教育に関して必要な，微積分，線形代数等については，適用範囲が広範囲になるため，重要事項に絞っての整備を行なってきた．多変数の実数値関数やノルム空間上の関数の微積分やルベーグ積分論，連続微分可能な関数や可積分関数による関数空間，閉グラフ定理や写像定理など，修士課程レベルの関数解析などの教材の充実化が進んでいる．今後はそれらを総合した，教材の組織的利用が課題になるものと考える．
教材システムの実用・実証実験についても，この教材システムを実際の授業で運用し，評価，改善作業が進んでいる．その実証実験の成果は，関連の学術学会等で公表し，専門研究者との意見交換を行なってきた。多数クライアント同時接続可能な論理思考訓練システムのスケーラビリティ検証と実運用ならびに運用実績に基づくシステム改善を行った．以上の状況からの区分(2)は妥当と考える．
|
| Strategy for Future Research Activity |
平成２５年度は本課題の計画の最終年度であり，これまでに形式化･教材化したものを整理・体系化するとともに，それによるe-learning教材システムを申請者が所属する大学の学科の全学部学生，専攻の修士課程全学生を対象に運用，実証実験を行ないシステムの改善を行なう．その実績をもとに，今後は他学科，他専攻を含む，大学全体での利用を提言し利用促進を図る予定である．申請者らが所属する大学では，全学的な汎用のe-learningシステムが既に稼働しており，申請者らが開発した，手法やシステムをこの全学システムにプラグインとして組み込むために必要な諸作業を行なう．利用促進のための講習会等を実施する．２５年度はそのための準備を行なう．
これと並行して既に行なってきたe-learning関連学会での研究成果公表等を通じて，本システムや手法の紹介，専門研究者との意見交換などによりシステムの改善，さらには利用普及促進を図る．申請者が開発した証明記述問題と計算機によるチェックを利用した論理思考訓練用の教材システムとその手法は，数学,情報工学に限らず，工学全般，さらには証明記述などを通じの論理思考訓練が必要な学術分野の教育に広く適用可能であり，また教育機関所属の学生に限らず，企業技術者の訓練にも有効と考えられるためこれへの展開を目指して行く．
数学定理の形式化ライブラリ構築については引き続きその充実化を進めていく．解析系では複素関数論や，多変数関数の微積分，陰関数定理，微分方程式論，関数空間論や，作用素論，幾何ではストークスの定理や，多様体，微分幾何の基礎，代数系ではZ-加群，ガロア群や有限アーベル群，工学系では広範囲に利用され重要な最適化理論，離散系数学では，木構造を含むグラフ理論，数論アルゴリズム，さらには暗号などの計算機処理プログラムの動作の形式手法による正当性検証法などの研究を予定している。
|
