| 基于Isabelle/HOL的离散数学实验教学设计与实践 |
| |
| 引用本文： | 钱振江,聂盼红,肖乐,闫海英,严卫,殷旭东,靳勇,龚声蓉.基于Isabelle/HOL的离散数学实验教学设计与实践[J].常熟理工学院学报,2021,35(5):110-115. |
| |
| 作者姓名： | 钱振江 聂盼红 肖乐 闫海英 严卫 殷旭东 靳勇 龚声蓉 |
| |
| 作者单位： | 常熟理工学院计算机科学与工程学院,江苏常熟 215500 |
| |
| 摘 要： | 传统的离散数学实验教学,通常使用C、C++等程序设计语言来完成相应的课程验证性实验.学生在花费大量的时间和精力完成程序设计后,依然对程序的正确性没有直观的认识.借助Isabelle/HOL交互式定理证明器工具和形式化方法,构建离散数学实验环境,解决离散数学课程实验教学的直观表达问题以及逻辑推理实验的设置.以二叉树这种离散结构的知识点学习为例,阐述如何使用Isabelle/HOL来完成"离散数学"课程的实验教学设计.通过这种实验教学,能使学生对逻辑演算和推理有清晰的认识,同时培养学生的数学和逻辑思维以及创新、应用能力.
|
| 关 键 词： | 离散数学 实验教学 形式化方法 Isabelle/HOL |
Design and Practice of Discrete Mathematics Experimental Teaching Based on Isabelle/HOL |
| |
| QIAN Zhenjiang,NIE Panhong,XIAO Le,YAN Haiying,YAN Wei,YIN Xudong,JIN Yong,GONG Shengrong.Design and Practice of Discrete Mathematics Experimental Teaching Based on Isabelle/HOL[J].Journal of Changshu Institute of Technology,2021,35(5):110-115. |
| |
| Authors: | QIAN Zhenjiang NIE Panhong XIAO Le YAN Haiying YAN Wei YIN Xudong JIN Yong GONG Shengrong |
| |
| Abstract: | |
| |
| Keywords: | |
| 本文献已被 CNKI 万方数据 等数据库收录！ |
|
