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

Design and Practice of Discrete Mathematics Experimental Teaching Based on Isabelle/HOL

作　　者：钱振江[1] 聂盼红[1] 肖乐[1] 闫海英[1] 严卫[1] 殷旭东[1] 靳勇[1] 龚声蓉[1] QIAN Zhenjiang;NIE Panhong;XIAO Le;YAN Haiying;YAN Wei;YIN Xudong;JIN Yong;GONG Shengrong(School of Computer Science and Engineering,Changshu Institute of Technology,Changshu 215500,China)

机构地区：[1]常熟理工学院计算机科学与工程学院,江苏常熟215500

出　　处：《常熟理工学院学报》2021年第5期110-115,共6页Journal of Changshu Institute of Technology

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

摘　　要：传统的离散数学实验教学,通常使用C、C++等程序设计语言来完成相应的课程验证性实验.学生在花费大量的时间和精力完成程序设计后,依然对程序的正确性没有直观的认识.借助Isabelle/HOL交互式定理证明器工具和形式化方法,构建离散数学实验环境,解决离散数学课程实验教学的直观表达问题以及逻辑推理实验的设置.以二叉树这种离散结构的知识点学习为例,阐述如何使用Isabelle/HOL来完成“离散数学”课程的实验教学设计.通过这种实验教学,能使学生对逻辑演算和推理有清晰的认识,同时培养学生的数学和逻辑思维以及创新、应用能力.Students are usually allowed to use C/C++or other programming languages to complete the corresponding verification experiments during traditional discrete mathematics experimental teaching.Although students spend a lot of time and energy in completing the program design,they still have no intuitive understanding of the correctness of the program.In this paper,the experimental environment for discrete mathematics is constructed with the help of the interactive theorem prover Isabelle/HOL and the formal methods,to solve the problem of intuitive expression in the experimental teaching of discrete mathematics and the setting of logical reasoning experiments.Taking the binary tree in discrete structure as an example,the authors of the paper illustrate how to use Isabelle/HOL to design and practice for the discrete mathematics experimental teaching.Through the proposed experimental teaching,the students will have a clear understanding of logical calculations and reasoning.Meanwhile,the students'mathematical and logical thinking is stimulated,and their innovation and application ability is also cultivated.

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

分 类 号：G642[文化科学—高等教育学]