人工智能研究是當(dāng)前科技發(fā)展的前沿方向,夯實(shí)人工智能基礎(chǔ)理論尤為重要,數(shù)學(xué)定理機(jī)器證明是人工智能基礎(chǔ)理論研究的深刻體現(xiàn).定理機(jī)器證明主要是指借助計(jì)算機(jī)技術(shù)實(shí)現(xiàn)數(shù)學(xué)定理的證明,從而在數(shù)學(xué)推理中實(shí)現(xiàn)腦力勞動的機(jī)械化.近年來隨著計(jì)算機(jī)技術(shù)的發(fā)展,一些證明工具Coq、Isabelle及HOL等相繼出現(xiàn),數(shù)學(xué)定理的計(jì)算機(jī)形式化證明取得了長足進(jìn)展.本文基于證明輔助工具Coq,給出集合、函數(shù)、拓?fù)涞然径x的形式化描述,為搭建拓?fù)淇臻g連通性形式化系統(tǒng)做了必要準(zhǔn)備.在此系統(tǒng)上,研究了拓?fù)淇臻g中的拓?fù)洳蛔冃再|(zhì),即連通性.完成拓?fù)淇臻g連通性相關(guān)定理的形式化證明,全部定義的描述和定理的證明均使用Coq編譯完成,充分體現(xiàn)了Coq交互性、嚴(yán)格性、智能性.

【文章頁數(shù)】：40 頁

【學(xué)位級別】：碩士

【文章目錄】：
摘要
Abstract
第一章 緒論
    1.1 研究背景及意義
        1.1.1 研究背景
        1.1.2 研究意義
    1.2 Coq簡介
    1.3 本文研究內(nèi)容及結(jié)構(gòu)安排
第二章 Coq基本知識
    2.1 Coq基本語法
    2.2 初等邏輯知識
    2.3 公理化集合論形式化系統(tǒng)
第三章 連通空間相關(guān)定義形式化
    3.1 拓?fù)淇臻g相關(guān)定義
    3.2 連通空間形式化定義
第四章 連通空間相關(guān)定理形式化
    4.1 基本定理及引理
    4.2 拓?fù)淇臻g連通性形式化
第五章 總結(jié)與展望
參考文獻(xiàn)
致謝
作者簡介
伊犁師范大學(xué)碩士研究生學(xué)位論文導(dǎo)師評閱表



本文編號：3864289