-
题名基于Coq的杨忠道定理形式化证明
被引量：1
- 1
-
-
作者
严升
郁文生
付尧顺
-
机构
天地互联与融合北京市重点实验室(北京邮电大学电子工程学院)
-
出处
《软件学报》
EI
CSCD
北大核心
2022年第6期2208-2223,共16页
-
基金
国家自然科学基金(61936008)。
-
文摘
实现拓扑学定理的机器证明,是吴文俊院士生前的宿愿.杨忠道定理涉及一般拓扑学中的诸多基本概念,对深刻理解拓扑空间的本质有重要意义.该定理表明,拓扑空间中每一个子集的导集为闭集当且仅当此空间中的每一个单点集的导集为闭集,是一般拓扑学中的一个重要定理.基于定理证明辅助工具Coq,从公理化集合论机器证明系统出发,对一般拓扑学中的开集、闭集、邻域、凝聚点和导集等拓扑基本概念进行形式化描述,给出这些概念基本性质的形式化验证,建立了拓扑空间的形式化框架.在此基础上,实现基于Coq的杨忠道定理形式化证明.全部引理、定理和推论均完整给出Coq的形式化描述和机器证明代码,并在计算机上运行通过,体现了基于Coq的数学定理机器证明具有可读性、交互性和智能性的特点,其证明过程规范、严谨、可靠.杨忠道定理的形式化证明是一般拓扑学形式化内容的一个深刻体现.
-
关键词
cOQ
形式化证明
公理化集合论
一般拓扑
拓扑空间
杨忠道定理
-
Keywords
coq
formal proof
axiomatic set theory
general topology
topological space
c.T.yang’s theorem
-
分类号
TP311
[自动化与计算机技术—计算机软件与理论]
-
-
题名I-fuzzy拓扑中的杨忠道定理
被引量：1
- 2
-
-
作者
王瑞英
韩刚
李南南
-
机构
内蒙古师范大学数学科学学院
-
出处
《模糊系统与数学》
CSCD
北大核心
2013年第2期98-103,共6页
-
基金
内蒙古自然科学基金资助项目(2012MS0121
2010MS0118)
+1 种基金
内蒙古自治区高等学校科学技术研究项目(NJZY11033)
内蒙古师范大学研究生科研创新基金资助项目(CXJJS12030)
-
文摘
用L-ukasiewicz逻辑语义的方法在I-fuzzy拓扑中引入了I-fuzzy导集的概念,且研究了它的一些性质,进一步在I-fuzzy拓扑空间框架下证明了关于所提出导集的杨忠道定理。
-
关键词
Lukasiewicz逻辑
I-fuzzy拓扑
拟差
导集
杨忠道定理
-
Keywords
Lukasiewicz Logic
I-fuzzy Topology
Quasi-difference
Derived Set
c. T. yang＇ s theorem
-
分类号
O189
[理学—数学]
-
-
题名点集拓扑学之杨忠道定理的一个机械化证明
被引量：1
- 3
-
-
作者
曾振柄
王建林
杨争峰
小林英恒
-
机构
上海大学数学系
河南大学计算机与信息工程学院
华东师范大学上海市高可信计算重点实验室
Department of Mathematics
-
出处
《中国科学：数学》
CSCD
北大核心
2021年第1期257-288,共32页
-
基金
国家自然科学基金(批准号:11471209和61772203)资助项目。
-
文摘
本文给出一种用高阶逻辑自动证明语言Isabelle在计算机中表示拓扑空间中开集、闭集、邻域和导集等基本概念的方法,在此基础上证明点集拓扑学中著名的杨忠道定理,即一拓扑空间的任意单点集的导集为闭集,则其任意子集的导集亦为闭集.
-
关键词
拓扑空间
开集
闭集
导集
杨忠道定理
机器证明
-
Keywords
topological space
open set
closed set
derived set
c.T.yang's theorem
machine proof
-
分类号
O189.11
[理学—数学]
-
-
题名直觉I-Fuzzy拓扑空间的杨忠道定理
- 4
-
-
作者
张春芝
王瑞英
姚尧
-
机构
内蒙古师范大学数学科学学院
-
出处
《数学的实践与认识》
北大核心
2016年第7期228-234,共7页
-
基金
内蒙古自然科学基金(2012MS0121)
-
文摘
以L＊-格值上Lukasiewicz蕴含算子为工具引入了直觉I-Fuzzy拓扑空间中导集概念，接着给出它的一些性质，最后证明了直觉I-Fuzzy拓扑空间中导集的杨忠道定理．
-
关键词
L*-格值逻辑
直觉I-Fuzzy拓扑空间
拟差
导集
杨忠道定理
-
Keywords
L＊-lattice Valued Logic
intuitionistic I-fuzzy topological space
quasi-difference
derived Set
c.T.yang＇s theorem
-
分类号
O189.11
[理学—数学]
-
-
题名杨忠道定理在L-不分明化拓扑中的推广
被引量：1
- 5
-
-
作者
邹祥福
-
机构
五邑大学数学物理系
-
出处
《模糊系统与数学》
CSCD
北大核心
2009年第2期59-63,共5页
-
基金
广东省自然科学基金资助项目(5013321)
江门市科技攻关项目
-
文摘
将L-不分明化拓扑中的L-不分明化闭包运算的概念扩充到模糊集合上;并把杨忠道定理推广到L-不分明化拓扑中。
-
关键词
非经典逻辑
拓扑
L-不分明化拓扑空间
杨忠道定理
-
Keywords
Non-classical Logic
Topology L-fuzzifying Topology c. T. yang＇ s theorem
-
分类号
O141
[理学—数学]
O189
[理学—基础数学]
-
