| 研究概要 |
師玉,和崎らは多変数関数,複素関数の微積分学に関する教材を作成するため,先ずそれらを構成する基礎定理とその証明の形式化記述を行い,その成果を専門学会論文誌Formalized Mathematics(以下F.M.と略記)に公表した。それと並行してその形式化記述を利用して,e-Learning用コースマネージメントシステムMoodleにMizarシステムを組み込んだシステム(以下Mizar-Moodleシステムと略記)により教材作成を作成した。同様に岡崎,山崎,和崎,カワモトらは線形代数学,離散数学,初等幾何に関する教材作成するため,同様に基礎定理とその証明の形式化記述を行ない,その成果をF.M.に公表,併せて上記Mizar-Moodleシステム上で教材を作成した。特に暗号論については,DES暗号システムの数学的正当性についての詳細な形式化記述を行ない,これと整数論の初等的な内容に関する教材をMizar-Moodleシステムにより作成した。開発された上記の教材群はhttp://cai2.cs.shinshu-u.ac.jP/mizar/moodle/で閲覧できる。集合論については,ポーランドの研究者らの協力を得て,集合演算や2項関係に関する教材を作成した。上記教材作成による論理思考訓練システムの構築と検証を行なうため,特に証明チェック時のエラーログから,学生の弱点等を抽出可能とする仕組みの検討,遠隔教育,ブレンディング教育上実用に供するかどうかの確認を行なうため,信州大学情報工学科・情報工学専攻で実際に教材として試用を開始した。特に和崎は,今後これらの教材システムを大規模人数の教育に用いる場合に備え,学習成果を自動収集するエージェントベースシステムの開発にまで考察を進めた。
|
