基于Coq的有标集族相关定理的机器证明  

Machine Proving of Correlation Theorem of Standard Set Family Based on Coq

作　　者：刘佳 吕红伟 付尧顺 郁文生 Liu Jia;Lv Hongwei;Fu Yaoshun;YuWensheng(College of Mathematics and Statistics,Yili Normal University,Yining,Xinjiang 835000,China;School of Electronic Engineering,Beijing University of Posts and Telecommunications,Beijing 100876,China)

机构地区：[1]伊犁师范大学数学与统计学院,新疆伊宁835000 [2]北京邮电大学电子工程学院,北京100876

出　　处：《伊犁师范学院学报（自然科学版）》2020年第2期13-22,共10页Journal of Yili Normal University：Natural Science Edition

基　　金：新疆维吾尔自治区自然科学基金项目(2018D01C008).

摘　　要：基于计算机证明辅助工具Coq,参考“公理化集合论”形式化系统,实现朴素集合论形式化系统,并在此基础上给出有标集族及其交和并的形式化,完成有标集族相关定理的Coq描述及机器证明代码,所有形式化过程已被Coq验证,并在计算机上运行通过,体现了Coq的规范、严谨、可靠.为构建完整的点集拓扑理论打下基础,在此系统下,有望实现拓扑空间相关性质的形式化系统.Based on the proof assistant Coq,referring to the axiomatic set theory formal system,we realize a naive set theory formal system.Furthermore a set of labeled sets and their intersections are formalized.The Coq description and machine proof code of the related theorem of the standard set family have been verified by Coq,and run on the computer,which reflects Coq's standard,rigorous and reliable.This article lays the foundation for constructing a complete point set topology theory.Under this system,it is expected to realize a formal system of topological space related properties.

关 键 词：COQ 机器证明 公理化集合论 有标集族 

分 类 号：O212.1[理学—概率论与数理统计]