| 研究概要 |
Mizarは形式化記述された数学定理証明の正しさを機械的に検証するソフトウエアである．申請者らは,本研究課題でこれを用いた数学ライブラリの構築と大学数学向けの教材開発,それをe-learning用CMSに組み込んで実用する実証実験を行なってきた。
24年度は,前年度までに作成した教材コンテンツを用いて，論理思考，数理的思考訓練の実用システムを実際の授業で使用し評価，改善を行った．特に多数利用者の同時接続可能なシステムのスケーラビリティ検証と実運用ならびに運用実績に基づくシステム改善を行った．また，運用実績をもとに，教材のコンテンツ改良も行った．それらの成果はe-learning関連の学会などで公表した．さらに，研究目的を達成するため23年度に引き続き以下のライブラリ開発と教材化を行った．
(1)多変数関数，ノルム空間上の関数の微積分やルベーグ積分論などの命題群の形式化，それらを基にした教材の作成を作成した．関数解析関連では閉グラフ定理や写像定理さらに連続微分可能な関数による関数空間など基礎的な形式化ライブラリの作成を行なった．
(2) 離散数学系，暗号，アルゴリズム，並列処理等の形式化ライブラリ作成と教材の作成，23年度までに作成した教材の改良を行なった．代数系では有限群や巡回群の基礎定理，拡張ユークリッド互除法や,中国人剰余定理に関する数論アルゴリズム,また暗号については,DES暗号システムやAES暗号システムの暗号化,復号アルゴリズム,さらに,Z-加群や楕円曲線論の基礎までの形式化ライブラリを作成した．ペトリネットや並列処理回路動作の形式化と検証等を行なった．
(3) 線形代数学に関するライブラリ作成とそれを用いた教材を行なった．特に,情報工学分野に関連し,これの数理形態学的手法画像処理への応用やBOOLE変数の多重対から構成される線形空間に関してのライブラリ充実も図った．
|
