基于Isabelle/HOL的离散数学实验教学设计与实践

作     者：钱振江 聂盼红 肖乐 闫海英 严卫 殷旭东 靳勇 龚声蓉 QIAN Zhenjiang;NIE Panhong;XIAO Le;YAN Haiying;YAN Wei;YIN Xudong;JIN Yong;GONG Shengrong

作者机构：常熟理工学院计算机科学与工程学院江苏常熟215500 

基　　金：江苏省高等教育教学改革研究项目“产教融合背景下应用型本科人工智能行业学院模式的探索与实践”(2019JSJG582) 江苏省高校“青蓝工程”中青年学术带头人培养对象项目(2019) 

出 版 物：《常熟理工学院学报》 (Journal of Changshu Institute of Technology)

年 卷 期：2021年第35卷第5期

页      码：110-115页

摘      要：传统的离散数学实验教学,通常使用C、C++等程序设计语言来完成相应的课程验证性实验.学生在花费大量的时间和精力完成程序设计后,依然对程序的正确性没有直观的认识.借助Isabelle/HOL交互式定理证明器工具和形式化方法,构建离散数学实验环境,解决离散数学课程实验教学的直观表达问题以及逻辑推理实验的设置.以二叉树这种离散结构的知识点学习为例,阐述如何使用Isabelle/HOL来完成“离散数学”课程的实验教学设计.通过这种实验教学,能使学生对逻辑演算和推理有清晰的认识,同时培养学生的数学和逻辑思维以及创新、应用能力.

主 题 词：离散数学 实验教学 形式化方法 Isabelle/HOL 

学科分类：0401[教育学-教育学类] 04[教育学] 040102[040102] 

D　O　I：10.3969/j.issn.1008-2794.2021.05.023

馆 藏 号：203105000...