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

万新熠; 徐轲; 曹钦翔

首页> 中文期刊> 《软件学报》 >针对教学场景的ZFC集合论Coq形式化

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

开具论文收录证明 >>

期刊封面封底目录下载 >>

文献代查 >>

页面导航

摘要
著录项
相似文献
相关主题

摘要

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

著录项

来源
《软件学报》 |2023年第8期|3549-3573|共25页
作者
万新熠; 徐轲; 曹钦翔;
展开▼
作者单位

上海交通大学电子信息与电气工程学院;

展开▼
原文格式 PDF
正文语种 chi
中图分类程序设计、软件工程;
关键词
COQ; ZFC公理集合论; 一阶逻辑;

相似文献

中文文献
外文文献
专利

1. 基于Coq的逆矩阵运算的形式化 [J] . 沈楠 ,陈钢 . 计算机科学 . 2023,第期
2. 多旋翼飞控推进子系统的Coq形式化验证 [J] . 石正璞 ,崔敏 ,谢果君 . 软件学报 . 2022,第6期
3. 基于Coq的杨忠道定理形式化证明 [J] . 严升 ,郁文生 ,付尧顺 . 软件学报 . 2022,第6期
4. 基于Coq的分块矩阵运算的形式化 [J] . 麻莹莹 ,马振威 ,陈钢 . 软件学报 . 2021,第6期
5. 基于Coq的Paxos形式化建模与验证 [J] . 李亚男 ,邓玉欣 ,刘静 . 软件学报 . 2020,第8期
6. 离散数学中集合论部分证明方法的教学思考 [C] . 乐天 ,张威 . 浙江省高校计算机教学研究会2016学术年会 . 2016
7. 基于Coq的有限域GF(2^n)的形式化研究及应用 [A] . 范永乾 . 2020

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

摘要

著录项

相似文献

相关主题

期刊订阅