![点击分享此内容可以赚币 分享](/master/images/share_but.png)
针对教学场景的ZFC集合论Coq形式化.pdf
《针对教学场景的ZFC集合论Coq形式化.pdf》由会员分享,可在线阅读,更多相关《针对教学场景的ZFC集合论Coq形式化.pdf(25页珍藏版)》请在咨信网上搜索。
1、 软件学报 ISSN 1000-9825,CODEN RUXUEW E-mail: Journal of Software,2023,34(8):35493573 doi:10.13328/ki.jos.006868 http:/ 中国科学院软件研究所版权所有.Tel:+86-10-62562563 针对教学场景的 ZFC 集合论 Coq 形式化 万新熠,徐 轲,曹钦翔(上海交通大学 电子信息与电气工程学院,上海 200240)通信作者:曹钦翔,E-mail: 摘 要:离散数学是计算机类专业的基础课程之一,命题逻辑、一阶逻辑与公理集合论是其重要组成部分.教学实践表明,初学者准确理解语法、语义、
2、推理系统等抽象概念是有一定难度的.近年来,已有一些学者开始在教学中引入交互式定理证明工具,以帮助学生构造形式化证明,更透彻地理解逻辑系统.然而,现有的定理证明器有较高上手门槛,直接使用会增加学生的学习负担.鉴于此,在Coq 中开发了针对教学场景的 ZFC 公理集合论证明器.首先,形式化了一阶逻辑推理系统和 ZFC 公理集合论;之后,开发了数条自动化推理规则证明策略.学生可以在与教科书风格相同的简洁证明环境中使用自动化证明策略完成定理的形式化证明.该工具被用在了大一新生离散数学课程的教学中,没有定理证明经验的学生使用该工具可以快速完成数学归纳法和皮亚诺算术系统等定理的形式化证明,验证了该工具的实
3、际效果.关键词:Coq;ZFC 公理集合论;一阶逻辑 中图法分类号:TP311 中文引用格式:万新熠,徐轲,曹钦翔.针对教学场景的 ZFC 集合论 Coq 形式化.软件学报,2023,34(8):35493573.http:/ 英文引用格式:Wan XY,Xu K,Cao QX.Coq Formalization of ZFC Set Theory for Teaching Scenarios.Ruan Jian Xue Bao/Journal of Software,2023,34(8):35493573(in Chinese).http:/ Coq Formalization of ZFC
4、 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)Abstract:Discrete mathematics is one of the foundation courses of computer science,whose components include propositional
5、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
6、 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 s
7、et 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
8、 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.Key words
9、:Coq;ZFC axiomatic set theory;first-order logic 近些年来,数学定理的形式化证明得到了广泛的发展和研究.定理证明工具如 Coq1,Isabelle2,Mizar3,Lean4等逐渐趋向成熟,基于这些工具,大量数学定理的证明得到了形式化,包括著名的四色定理5、哥德 本文由“约束求解与定理证明”专题特约编辑蔡少伟研究员、陈振邦教授、王戟研究员、詹博华副研究员、赵永望教授推荐.收稿时间:2022-09-05;修改时间:2022-10-13;采用时间:2022-12-14;jos 在线出版时间:2022-12-30 3550 软件学报 2023 年第 34
10、 卷第 8 期 尔不完全性定理6、Cauchy-Schwarz 不等式等.菲尔兹奖得主 Gowers 认为,计算机将在定理证明中起到关键作用,并将改变理论数学未来的研究模式7.Hanna 和 Yan8指出:定理证明器不仅可以帮助数学家进行理论研究,还能够改变面向数理逻辑初学者的教学方式.在我国高校计算机类专业的本科课程设置中,大多数高校院所都将离散数学课程设置为基础类必修课.而命题逻辑、一阶逻辑与公理集合论是离散数学课程的重要组成部分.教学实践中发现:初学数理逻辑的本科学生要学习并明晰语法、语义、推理系统等抽象概念是有一定难度的;同时,学生在学习使用一阶逻辑与公理集合论描述数学命题与数学证明时
11、也往往难以通过具体的例子形成直观理解.在教学中引入交互式定理证明器有望改善这一问题,计算机辅助的自动检查能够及时准确地反馈学生写的命题是否具有正确的语法、是否遵循逻辑系统的推理规则等情况,帮助学生构造一个正确且严格的证明,而无需等待助教可能长达数周的反馈.交互式定理证明器实时交互的特点,也能够让学生动态地看到推理过程,有助于加深对逻辑系统的理解.近年来,国际上越来越多的学者开始在数理逻辑课程,特别是计算机专业的相关课程中引入定理证明工具来辅助教学.例如:牛津大学开发了 Jape 用于谓词逻辑的教学9,Cezary 和 Freek 基于 Coq 开发了在线教学工具 ProofWeb10,Avig
12、ad 使用 Lean 进行一阶逻辑和集合论的概念的教学11.然而,以上工作大都使用了定理证明器的内置逻辑,这在教学中会有很多缺陷.(1)大部分定理证明工具如 Coq 采用了“自底向上”的反向证明模式,用户不断应用证明策略将待证目标分解为一系列子目标,最终得到所有子目标均为前提完成证明.而常用证明模式还包括从前提推导出新条件最终得出待证目标的正向推理;(2)学生应当根据当前学习的逻辑系统的推理规则进行推理,而不是使用定理证明器中内置的逻辑,偏离教学目标;(3)直接使用定理证明器进行证明更像是学习一门编程语言,学生需要额外付出大量时间熟悉操作该特定定理证明器的命令,不仅增加学习成本,而且容易忽视逻
13、辑系统本身;(4)由于仅提供了基本的证明策略,证明代码通常十分冗长,较大的工作量限制了学生完成更加复杂定理的形式化证明;(5)缺乏简洁的教科书风格的符号系统,不利于学生理解.简而言之,以辅助数学理论研究为目的开发的定理证明工具具有较高的上手门槛,在形式上与教科书中的逻辑系统差别较大,简单地直接引入教学中反而可能会加大学习成本,甚至使学生将定理证明器的内置逻辑与他正在学习的逻辑系统相混淆.考虑到这些问题,部分学者没有使用定理证明器,转而使用编程语言从头开发专用于教学的简易证明工具.Breitner12开发了 Incredible Proof Machine12,学生在可视化界面中使用鼠标将代表命
14、题和一阶逻辑推理规则的方块连接起来就可以构造证明.Lerner 等人提出了 Polymorprphic block13可视化界面,学生可以采用类似于拼拼图的方式将命题和推理块连接起来,完成自然演绎系统的推理.这些工具能够提供交互更简便、趣味性更强的体验,但从头开发需要极大的工作量.现有的交互式定理证明工具已经提供了完善的用户界面,包括证明界面、证明状态和错误信息,基于定理证明器开发教学工具能够极大减少开发成本,例如,本工作仅花费了 2 300 行 Coq 代码,在教学中是更为实际的选项;同时,针对不同教学场景进行调整也更加简便.作为辅助逻辑学习的工具,需要降低定理证明器中的形式化证明与教科书中
15、逻辑系统证明间的差距,使学生专注于他所学习的逻辑系统而非定理证明器的使用技巧.一款合格的基于定理证明概念的教学工具应当具有以下特点.(1)支持的推理模式应当与传统逻辑教材中使用的推理模式相同;(2)使用与教学内容相同的逻辑系统,所有操作都基于该系统的推理规则,尽可能少地暴露定理证明器的内置逻辑.此外,应当使用教科书上的逻辑术语和符号,而非定理证明器中新创建的变量名;(3)只需要简单的几条指令就可以完成证明,降低学生使用定理证明器的学习成本.这几条证明指令需 万新熠 等:针对教学场景的 ZFC 集合论 Coq 形式化 3551 要具有较高的自动化程度,从而减少代码量,帮助学生完成更复杂命题的严格
16、证明.针对上述问题,本文在 Coq 中开发了一个包含自动化证明策略的 ZFC 公理集合论证明器,用于辅助一阶逻辑和公理集合论的教学.本文在 Coq 中从抽象语法树开始形式化了基于一阶逻辑的 ZFC 公理集合论,采用sequent calculus 式的逻辑系统,并利用 notation 机制提供了简洁的符号.我们开发了数条自动化证明策略以简化证明过程,包括命题逻辑自动证明指令 FOL_Tauto,该指令将可证问题转化为合取范式的布尔可满足性问题,并调用我们在Coq中实现的DPLL可满足性求解器自动求解,实现了逻辑连接词的完全自动化处理.对于量词推理规则,我们分别开发了指令以支持多层量词的同时引
17、入和消去;对等号替换规则开发了指令peq_sub_tac 自动替换命题中的一阶逻辑项.以上所有指令均能自动处理-等价,且采用了与教材相同的正向推理模式.通过以上方法,我们构造了一个简洁快速的集合论证明环境,隐藏了 Coq本身的诸多细节,更贴近教科书风格的证明且更加自动化.学生使用该工具进行集合论定理的证明相比直接使用现有的定理证明器更为容易.图 1 给出了一个证明示例,两个集合的交集必然是其中一个集合的子集.(a)证明代码 (b)最后一步之前的 Coq 证明状态栏 图 1 ZFC 集合论证明器证明环境示例 我们在离散数学课程的实际教学中引入了该工具,并取得了良好效果.作为课程项目之一,学生需要
18、使用该证明器完成数学归纳法的证明.实践表明,首次接触一阶逻辑和公理集合论的大一新生经过简单学习后就可以完成该定理的形式化证明.较为优秀的学生可以在完成离散数学课程后,利用该工具进一步构造皮亚诺算术系统并证明了加法和乘法的相关性质,体现了该工具的简洁性和有效性.本文第 1节介绍研究背景,包括 Coq交互式定理证明器和基于定理证明器的逻辑教学工具研究现状.第 2节阐述 ZFC 集合论证明器的设计框架.第 3 节给出对 ZFC 公理集合论的形式化.第 4 节介绍自动证明策略的实现.第 5 节展示我们在离散数学课程教学中引入该证明器的实际效果.最后总结全文.1 研究背景 1.1 基于定理证明器的逻辑教
19、学工具研究现状 引入定理证明器辅助教学的主要问题在于:定理证明器在形式上与教科书中的逻辑系统有较大差距,如何缩小这一差距成为主要研究方向.一种思路试图在证明形式上逐渐使定理证明器的代码证明向教科书证明靠拢.Bhne 等人14在 Coq 中为每一条推理规则提供了一条证明指令,要求学生首先在 Coq 中完成命题的证明,之后在每一行证明代码前后通过注释写出此时对应的待证一阶逻辑命题,最后要求学生根据 Coq 证明写出与其结构相同的、教科书风格的纸笔证明,这样的证明具有与 Coq 相同的反向推理模式.实践表明,学生能够完成并理解 Coq 中的证明与逻辑系统之间的对应关系.Avigad11使用 Lean
20、 的内置逻辑进行一阶逻辑和集合论的教学,并让学生比较理解证明代码和纸笔证明.在系统学习 Lean 的使用方法后,学生也能够成功完成证明.另一种思路试图直接开发与教科书风格更相近的定理证明工具.早在 20 世纪末,牛津大学开发的 Jape9就提供了良好的可视化界面,可以将证明显示成树状或盒状的形式.受此启发,Kaliszyk 等人基于 Coq 开发了ProofWeb10,其采用了 Gentzen风格的自然演绎系统,并提供了轻量化的在线 GUI,学生同样通过应用每一条推理规则对应的指令自底向上进行证明.Theorem intersect_subset1:ZF?u,v,uvu.Proof.pose
21、proof Intersection_iff.universal instantiation H,u,v,z.assert ZF?zuvzu by FOL_Tauto.universal generalization H1,u,v,z.The conclusion is already proved.Qed.1 subgoal H:ZF?x,y,z,zxyzxzy H0:ZF?zuvzuzv H1:ZF?zuvzu H2:ZF?u,v,z,zuvzu _(1/1)ZF?u,v,uvu 3552 软件学报 2023 年第 34 卷第 8 期 国内的集合论相关研究大多关注重要集合论定理的形式化,如
22、杨忠道定理15、Tukey 引理16等,目前,对定理证明在教学中的应用研究较少,且都处于讨论和探索阶段.李沁17探讨了在计算机专业的数理逻辑课程中使用 Isabelle 辅助教学的可行性,江南等人18则比较了慕尼黑工业大学与国内高校有关逻辑与验证相关课程的开设情况,并呼吁计算机专业的理论课程和实践教学中需要设置更多的定理证明相关内容.据我们所知,本文是国内首次将交互式定理证明实际应用在面对数理逻辑初学者的课堂教学中.1.2 Coq交互式定理证明器 Coq 是一个交互式定理证明工具,具有强大的表达能力和优秀的扩展性,是国际上主流的证明助手之一,在数理逻辑、算法和高可靠性软件的形式化验证方面得到了
23、广泛应用.Coq 的理论基础是归纳构造演算,为用户提供归纳类型,比大多数函数式编程语言中的归纳类型更具表达力.用户可以在 Coq 中形式化定义数学概念、程序语言、逻辑系统等,并证明相关的性质和定理.在证明时,用户首先通过 Proof 指令开始证明,之后,应用一系列证明策略与 Coq 进行交互,证明策略会根据当前证明状态以及已经得到证明的定理、公理等将待证目标分解为数个更简单的子目标或者直接证明目标,而 Coq 证明检查器中的类型检查算法会根据归纳构造演算的性质机械化地进行检查.证明完成后,用户运行 Qed 指令退出证明.表 1 列出了 Coq 中的一些常用证明策略及其功能.表 1 Coq 常用
24、证明策略 Coq 证明策略功能 intros 引入待证目标中的条件 destruct 根据构造子进行分类讨论 induction 根据构造子进行结构归纳 apply 对待证目标应用一个假设或已证定理 eapply 应用时无需指定变元,推迟变元的实例化 pose proof 在条件中引入一个已证定理 assert 声明一个新的待证目标 assert by 声明新待证目标并由 by 后的策略直接解决rewrite 根据等式重写 congreunce 等式重写自动证明策略 reflexivity 自动比较待证目标等号两侧是否相同 tauto 直觉逻辑自动证明策略 Coq 允许用户通过 Ltac 语言
25、组合现有的证明策略构成新策略,简化证明过程,提高证明的自动化程度.本文所开发的自动证明策略就依赖 Ltac 语言实现,学生在使用中不需要学习 Coq 自带的证明指令语言,而只需要使用本文所开发的 7 条自动证明指令,其中一条与分离公理相关的证明策略没有出现在课程项目中,本文不做介绍.2 公理集合论证明器的设计框架 介绍 ZFC 定理证明器的实现框架之前,需要特别说明,该定理证明器是针对特定的数理逻辑教学场景开发的.教学的对象是已经掌握了命题逻辑的学生,并且当前阶段的教学重点是 sequent calclulus 式的逻辑系统中的 4 条量词推理规则以及 ZFC 公理集合论与日常数学之间的联系.
- 配套讲稿:
如PPT文件的首页显示word图标,表示该PPT已包含配套word讲稿。双击word图标可打开word文档。
- 特殊限制:
部分文档作品中含有的国旗、国徽等图片,仅作为作品整体效果示例展示,禁止商用。设计者仅对作品中独创性部分享有著作权。
- 关 键 词:
- 针对 教学 场景 ZFC 集合论 Coq 形式化
![提示](https://www.zixin.com.cn/images/bang_tan.gif)
1、咨信平台为文档C2C交易模式,即用户上传的文档直接被用户下载,收益归上传人(含作者)所有;本站仅是提供信息存储空间和展示预览,仅对用户上传内容的表现方式做保护处理,对上载内容不做任何修改或编辑。所展示的作品文档包括内容和图片全部来源于网络用户和作者上传投稿,我们不确定上传用户享有完全著作权,根据《信息网络传播权保护条例》,如果侵犯了您的版权、权益或隐私,请联系我们,核实后会尽快下架及时删除,并可随时和客服了解处理情况,尊重保护知识产权我们共同努力。
2、文档的总页数、文档格式和文档大小以系统显示为准(内容中显示的页数不一定正确),网站客服只以系统显示的页数、文件格式、文档大小作为仲裁依据,平台无法对文档的真实性、完整性、权威性、准确性、专业性及其观点立场做任何保证或承诺,下载前须认真查看,确认无误后再购买,务必慎重购买;若有违法违纪将进行移交司法处理,若涉侵权平台将进行基本处罚并下架。
3、本站所有内容均由用户上传,付费前请自行鉴别,如您付费,意味着您已接受本站规则且自行承担风险,本站不进行额外附加服务,虚拟产品一经售出概不退款(未进行购买下载可退充值款),文档一经付费(服务费)、不意味着购买了该文档的版权,仅供个人/单位学习、研究之用,不得用于商业用途,未经授权,严禁复制、发行、汇编、翻译或者网络传播等,侵权必究。
4、如你看到网页展示的文档有www.zixin.com.cn水印,是因预览和防盗链等技术需要对页面进行转换压缩成图而已,我们并不对上传的文档进行任何编辑或修改,文档下载后都不会有水印标识(原文档上传前个别存留的除外),下载后原文更清晰;试题试卷类文档,如果标题没有明确说明有答案则都视为没有答案,请知晓;PPT和DOC文档可被视为“模板”,允许上传人保留章节、目录结构的情况下删减部份的内容;PDF文档不管是原文档转换或图片扫描而得,本站不作要求视为允许,下载前自行私信或留言给上传者【自信****多点】。
5、本文档所展示的图片、画像、字体、音乐的版权可能需版权方额外授权,请谨慎使用;网站提供的党政主题相关内容(国旗、国徽、党徽--等)目的在于配合国家政策宣传,仅限个人学习分享使用,禁止用于任何广告和商用目的。
6、文档遇到问题,请及时私信或留言给本站上传会员【自信****多点】,需本站解决可联系【 微信客服】、【 QQ客服】,若有其他问题请点击或扫码反馈【 服务填表】;文档侵犯商业秘密、侵犯著作权、侵犯人身权等,请点击“【 版权申诉】”(推荐),意见反馈和侵权处理邮箱:1219186828@qq.com;也可以拔打客服电话:4008-655-100;投诉/维权电话:4009-655-100。