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

作者：钱振江; 聂盼红; 肖乐; 闫海英; 严卫; 殷旭东; 靳勇; 龚声蓉

来源：常熟理工学院学报, 2021, 35(05): 110-115.

DOI：10.16101/j.cnki.cn32-1749/z.2021.05.023

• 离散数学
• 实验教学
• 形式化方法
• Isabelle/HOL

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

• 单位
  常熟理工学院