| 研究課題/領域番号 |
22300285
|
|---|
| 研究種目 |
基盤研究(B)
|
| 配分区分 | 補助金 |
|---|
| 応募区分 | 一般 |
|---|
| 研究分野 |
教育工学
|
|---|
| 研究機関 | 信州大学 |
|---|
研究代表者 |
師玉 康成 信州大学, 工学部, 教授 (20226129)
|
|---|
| 研究分担者 |
和崎 克己 信州大学, 工学部, 教授 (70271492)
K PAULINE Naomi (KPAULINE Naomi / K PAU line Naomi) 信州大学, 工学部, 准教授 (40283238)
山崎 浩 信州大学, 工学部, 助教 (00293522)
岡崎 裕之 信州大学, 工学系研究科, 助教 (50432167)
|
|---|
| 連携研究者 |
布田 裕一 北陸先端科学技術大学院大学, 情報科学研究科, 准教授 (50706223)
荒井 研一 東京理科大学, 理工学部, 助教 (60645290)
|
|---|
| 研究期間 (年度) |
2010-04-01 – 2014-03-31
|
| 研究課題ステータス |
完了 (2013年度)
|
| 配分額 *注記 |
17,810千円 (直接経費: 13,700千円、間接経費: 4,110千円)
2013年度: 3,380千円 (直接経費: 2,600千円、間接経費: 780千円)
2012年度: 4,160千円 (直接経費: 3,200千円、間接経費: 960千円)
2011年度: 4,810千円 (直接経費: 3,700千円、間接経費: 1,110千円)
2010年度: 5,460千円 (直接経費: 4,200千円、間接経費: 1,260千円)
|
|---|
| キーワード | eラーニング / プルーフチェッカ / e-learning / 形式化数学 / 定理証明支援系 / Mizar / 論理思考 / moodle / e-learning教材 / プルーフチェッカー / 証明記述問題 / 計算機による検査 |
|---|
| 研究概要 |
Mizarシステムは形式化記述された定理証明の正しさを機械的に検証するプルーフチェッカーと呼ばれるソフトウェアである．申請者らは,これを用いた数学定理の形式化研究とそのライブラリ編纂を行う国際プロジェクトを推進してきたが，その成果を教育に利用するためe-learning用のCMSにこのMizarシステムを組み込むモジュールを試作し, 大学院教育でその試験運用も進めてきた．本研究ではその成果をもとに，e-learningによる論理思考，数理的思考訓練の実用システムとその教材開発を行った。これは「学生の論理思考能力の育成」という高等教育の深刻な課題の一つに有効な解決手段の提供するものになっている.
|
