基于交互式定理证明工具Coq的素数无限定理证明

论文摘要

随着人工智能技术的飞速发展,人工智能与数学领域的结合愈加密切,数学机械化的发展对数学领域与人工智能领域产生了深远影响。机器证明作为数学机械化的核心,成为数学机械化领域最为重要的研究课题之一,而机器证明的核心理念就是借助计算机辅助证明工具理解检验数学定理正确性,完成数学定理的证明。目前,国内以及国际数学机械化领域中,存在着许多形式化辅助证明工具,Coq是当前主流辅助证明工具之一。Coq作为一个基于归纳构造演算的辅助证明工具,具备了严谨性与可靠性,且辅助证明工具Coq集成开发环境友好,令证明更具可读性。至今为止,Coq证明工具在数学机械化领域得到广泛应用并极具成效,取得了许多代表性成果,在2005年,Gonthier和Werner使用辅助证明工具Coq完成了“四色定理”的数学机械化证明,在学术界引起了深远的影响。众所周知,数论是数学系统的重要分支,而素数在数论中有着举足轻重的地位,数学界对于素数的学术研究从未间断,有关素数性质的第一个定理便是素数无限定理,对素数无限定理机器证明的研究,具有极为重要的理论意义及应用价值。素数无限定理的机器证明,连接了计算机领域与数论领域的桥梁,且数论是现代数学的一大分支,所以这也是数学机械化在机器证明领域发展的一步迈进。本文通过数学辅助证明工具Coq,对素数无限定理进行了数学机械化证明,其中包括欧几里德证明,基于费马数的证明,本文对两种方法逐一给出了机器证明。本文的创新点在于利用交互式定理证明辅助工具Coq给出这些证明的机器证明方法,且素数领域的数学机械化证明仍处于空白,素数无限定理的机器证明是推动数学领域与人工智能领域结合的一次尝试。

论文目录

• 摘要
• ABSTRACT
• 第一章 绪论
•   1.1 数学机械化与人工智能
•   1.2 形式化证明辅助工具Coq
•     1.2.1 Coq的发展
•     1.2.2 Coq的特性
•     1.2.3 Coq的成果
•   1.3 素数无限定理
•   1.4 文章结构安排
• 第二章 Coq的基础语法
•   2.1 Coq预备知识
•     2.1.1 初等逻辑概念
•     2.1.2 基础Coq术语
•   2.2 Coq中的项与项的基础语法
•     2.2.1 Coq中的项
•     2.2.2 Coq中的表达式
•     2.2.3 Coq中的类型
•     2.2.4 Coq中的声明与定义
•   2.3 Coq中的量词与命题描述
•     2.3.1 Coq中的量词和依赖积
•     2.3.2 Coq中的命题描述语法
•   2.4 Coq中的命题证明
• 第三章 定理证明策略及Coq基础定义和性质
•   3.1 素数无限定理证明策略
•     3.1.1 欧几里德证明方法
•     3.1.2 基于费马数的证明方法
•   3.2 基于Coq的基础定义和性质
•     3.2.1 基于Coq的基础定义
•     3.2.2 基于Coq的基础性质
• 第四章 素数无限定理的Coq证明
•   4.1 欧几里德方法的Coq证明
•   4.2 基于费马数的Coq证明
• 第五章 总结与展望
•   5.1 全文总结
•   5.2 研究展望
• 参考文献
• 致谢

文章来源

类型: 硕士论文

作者: 柴干

导师: 郁文生

关键词: 素数无限定理,数学机械化,欧几里德证明,基于费马数的证明

来源: 北京邮电大学

年度: 2019

分类: 基础科学,信息科技

专业: 数学,自动化技术

单位: 北京邮电大学

分类号: TP18;O156.4

总页数: 68

文件大小: 3389K

下载量: 60