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

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

传统的离散数学实验教学,通常使用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.