基于Coq的拓扑空间连通性形式化系统

发布时间：2023-11-15 18:39

　　人工智能研究是当前科技发展的前沿方向,夯实人工智能基础理论尤为重要,数学定理机器证明是人工智能基础理论研究的深刻体现.定理机器证明主要是指借助计算机技术实现数学定理的证明,从而在数学推理中实现脑力劳动的机械化.近年来随着计算机技术的发展,一些证明工具Coq、Isabelle及HOL等相继出现,数学定理的计算机形式化证明取得了长足进展.本文基于证明辅助工具Coq,给出集合、函数、拓扑等基本定义的形式化描述,为搭建拓扑空间连通性形式化系统做了必要准备.在此系统上,研究了拓扑空间中的拓扑不变性质,即连通性.完成拓扑空间连通性相关定理的形式化证明,全部定义的描述和定理的证明均使用Coq编译完成,充分体现了Coq交互性、严格性、智能性.

【文章页数】：40 页

【学位级别】：硕士

【文章目录】：
摘要
Abstract
第一章 绪论
    1.1 研究背景及意义
        1.1.1 研究背景
        1.1.2 研究意义
    1.2 Coq简介
    1.3 本文研究内容及结构安排
第二章 Coq基本知识
    2.1 Coq基本语法
    2.2 初等逻辑知识
    2.3 公理化集合论形式化系统
第三章 连通空间相关定义形式化
    3.1 拓扑空间相关定义
    3.2 连通空间形式化定义
第四章 连通空间相关定理形式化
    4.1 基本定理及引理
    4.2 拓扑空间连通性形式化
第五章 总结与展望
参考文献
致谢
作者简介
伊犁师范大学硕士研究生学位论文导师评阅表



本文编号：3864289