2011 Fiscal Year Annual Research Report
MIZAR数学ライブラリの構築と大学数学向け高度遠隔教育用コンテンツ開発
| Project/Area Number |
22300285
|
|---|
| Research Institution | Shinshu University |
|---|
Principal Investigator |
師玉 康成 信州大学, 工学部, 教授 (20226129)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
KPAULINE Naomi 信州大学, 工学部, 准教授 (40283238)
和崎 克己 信州大学, 工学部, 教授 (70271492)
岡崎 裕之 信州大学, 工学系研究科, 助教 (50432167)
山崎 浩 信州大学, 工学部, 助教 (00293522)
|
|---|
| Keywords | eラーニング / プルーフチェッカ |
|---|
| Research Abstract |
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系においてこの学習成果を自動収集するシステムを運用するための準備として,他の形式検証システムを用いて実運用を行い,システムの評価を行い,その成果を複数の国際会議にて発表した.
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
ライブラリの作成,およびその教材化が順調に進んでいる.さらに教材用サーバの整備,強化を行い,本学において実際の授業(受講者が数十から百人規模を想定)での運用を行う準備が整ったことからも,おおむね順調に進展していると判断される.
|
| Strategy for Future Research Activity |
作成した論理思考訓練システムを実際の授業にて運用し,評価,改善を行う.実際の授業において本システムを運用する場合,受講学生が同時に接続する可能性がある.従って,24年度は特に,多数クライアント同時接続可能な論理思考訓練システムのスケーラビリティ検証と実運用ならびに運用実績に基づくシステム改善を行う.また,運用実績をもとに,教材のコンテンツ改良も行う.さらに教材作成も継続して行い,コンテンツの充実を進める.
|
