首页 | 本学科首页   官方微博 | 高级检索  
     

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

关 键 词:Coq  ZFC公理集合论  一阶逻辑
收稿时间:2022-09-05
修稿时间:2022-10-13

Coq Formalization of ZFC Set Theory for Teaching Scenarios
WAN Xin-Yi,XU Ke,CAO Qin-Xiang. Coq Formalization of ZFC Set Theory for Teaching Scenarios[J]. Journal of Software, 2023, 34(8): 3549-3573
Authors:WAN Xin-Yi  XU Ke  CAO Qin-Xiang
Affiliation:School of Electronic Information and Electrical Engineering, Shanghai Jiao Tong University, Shanghai 200240, China
Abstract: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.
Keywords:Coq  ZFC axiomatic set theory  first-order logic
本文献已被 万方数据 等数据库收录!
点击此处可从《软件学报》浏览原始摘要信息
点击此处可从《软件学报》下载全文
设为首页 | 免责声明 | 关于勤云 | 加入收藏

Copyright©北京勤云科技发展有限公司  京ICP备09084417号