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

Coq Formalization of ZFC Set Theory for Teaching Scenarios

作　　者：万新熠 徐轲 曹钦翔 WAN Xin-Yi;XU Ke;CAO Qin-Xiang(School of Electronic Information and Electrical Engineering,Shanghai Jiao Tong University,Shanghai 200240,China)

机构地区：[1]上海交通大学电子信息与电气工程学院,上海200240

出　　处：《软件学报》2023年第8期3549-3573,共25页Journal of Software

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

关 键 词：COQ ZFC公理集合论 一阶逻辑 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]