针对教学场景的ZFC集合论Coq形式化

离散数学是计算机类专业的基础课程之一,命题逻辑、一阶逻辑与公理集合论是其重要组成部分.教学实践表明,初学者准确理解语法、语义、推理系统等抽象概念是有一定难度的.近年来,已有一些学者开始在教学中引入交互式定理证明工具,以帮助学生构造形式化证明,更透彻地理解逻辑系统.然而,现有的定理证明器有较高上手门槛,直接使用会增加学生的学习负担.鉴于此,在Coq中开发了针对教学场景的ZFC公理集合论证明器.首先,形式化了一阶逻辑推理系统和ZFC公理集合论;之后,开发了数条自动化推理规则证明策略.学生可以在与教科书风格相同的简洁证明环境中使用自动化证明策略完成定理的形式化证明.该工具被用在了大一新生离散数学课程的教学中,没有定理证明经验的学生使用该工具可以快速完成数学归纳法和皮亚诺算术系统等定理的形式化证明,验证了该工具的实际效果.

Coq Formalization of ZFC Set Theory for Teaching Scenarios

Discrete mathematics is one of the foundation courses of computer science, whose components include propositional logic, first-order logic and axiomatic set theory. Teaching practice shows that it is difficult for beginners to accurately understand abstract concepts such as syntax, semantics and deduction system. In recent years, some scholars have begun to introduce interactive theorem provers into teaching to help students construct formal proofs so that they can understand logical systems more thoroughly. However, existing theorem provers have a high threshold for getting started, directly employing these tools will increase students'' learning burden. To address this problem, this study proposes a ZFC axiomatic set theory prover developed in Coq for teaching scenarios. First-order deduction system and ZFC axiomatic set theory are formalized, then several automated reasoning tactics are developed. Students can utilize these tactics to reason formally in a concise, textbook-style proving environment. This tool has been introduced into the discrete mathematics course for freshmen. Students with no prior theorem proving experience can exploit this tool to quickly construct formal proofs of theorems like mathematical induction and Peano arithmetic system, which verifies the practical effect of this tool.