Content Development for Distance Education in Advanced University Mathematics Using Mizar

使用 Mizar 进行高等大学数学远程教育内容开发

• 批准号: 22300285
• 负责人: SHIDAMA Yasunari
• 金额: $ 11.4万
• 依托单位: Shinshu University
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for Scientific Research (B)
• 财政年份: 2010
• 资助国家: 日本
• 起止时间: 2010-04-01 至 2014-03-31
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-22300285/
• 关键词: eラーニング; プルーフチェッカ; e-learning; 形式化数学; 定理証明支援系; Mizar; 論理思考; moodle; e-learning教材; プルーフチェッカー; 証明記述問題; 計算機による検査

The Mizar system is a software program to mechanically verify the correctness of theorem proofs written in a formal mathematical language. The applicants have helped to drive an international project for pursuing research on the formalization of mathematical theorems using the Mizar system and creating an open archive of the compiled mathematical knowledge. In order to apply the results of this work to education, the members built a module for embedding the Mizar system into an e-learning CMS used in a graduate curriculum and developed contents for training students in logic and advanced university mathematics. The results of this research offer an effective solution to the serious and difficult task of "training logical thinking skills to students" in higher education.

Mizar系统是一个软件程序，用于机械地验证用正式数学语言编写的定理证明的正确性。申请者帮助推动了一个国际项目，利用Mizar系统对数学定理的形式化进行研究，并建立一个已汇编的数学知识的公开档案。为了将这项工作的成果应用于教育，成员们建立了一个模块，将MIZAR系统嵌入到研究生课程中使用的电子学习CMS中，并开发了培训学生学习逻辑和高等大学数学的内容。本研究的成果为高校“培养学生逻辑思维能力”这一严峻而艰巨的任务提供了有效的解决方案。

项目成果

情報リテラシ教育向け大規模エージェントベースシステムの開発と評価-テンプレートマッチング処理を用いた学習結果自動収集の改善-

基于主体的大规模信息素养教育系统的开发和评估 - 使用模板匹配处理改进学习结果的自动收集 -

• 发表时间: 2010
• 作者: 田中敬一;和崎克己
• 通讯作者: 和崎克己

Riemann Integral of Functions from R into n-dimensional Real Normed Space

R 函数到 n 维实范空间的黎曼积分

• 发表时间: 2012
• 期刊: Formalized Mathematics
• 影响因子: 0.3
• 作者: Keiichi Miyajima;Artur Kornilowicz;Yasunari Shidama
• 通讯作者: Yasunari Shidama

negligible function の形式定義について

关于可忽略函数的正式定义

• 发表时间: 2014
• 作者: 岡崎裕之;布田 裕一
• 通讯作者: 布田 裕一

タイムアウト処理と調停者選出方法を拡張した分散合意アルゴリズムのPROMELAモデル

具有扩展超时处理和仲裁者选择方法的分布式共识算法PROMELA模型

• 发表时间: 2013
• 作者: 後藤亮馬;和崎克己
• 通讯作者: 和崎克己

VDMToolsを用いた資源管理システムの仕様実行とプロトタイピング

使用 VDMTools 进行资源管理系统的规范执行和原型设计

• 发表时间: 2013
• 作者: 村林 慧;和崎克己
• 通讯作者: 和崎克己