基于Coq的几何学定理的形式化证明特例研究 ——杨路定理的形式化证明

论文摘要

人工智能是一门研究模拟和延伸人的智能的一门新技术科学[1]。它作为计算机科学的一个分支,旨在了解智能的实质,并生产出一种新的能模拟人类智能的方式进行思考并作出决策行动的智能机器,该领域的研究包括机器人、语言识别、图像识别、自然语言处理和专家系统等。人工智能从诞生以来,其理论和技术日益成熟,应用领域也不断扩大。人工智能在数学机械化领域的突出体现就是机器证明。机器证明是通过计算机和辅助证明工具实现定理证明的一门学科。目前的辅助证明工具有Coq、Isabelle、HOL Light等。Coq是目前国际上最主流的辅助证明工具之一,它起源于法国,其核心是归纳构造演算,这也使得Coq拥有了很强的严谨性与可靠性。不仅如此,Coq交互式的证明环境也给使用者带来了极大的便利。目前,人们利用Coq已经证明了许多著名的数学定理,其中最有影响力的是Gonthier和Werner在2005年完成的“四色定理”的机器证明。在这之后,2012年Gonthier又给出了有限单群分类定理的机器验证,到了 2015年Hales等人又完成了 Kepler猜想的计算机证明。这些成果使得辅助证明工具Coq在学术界的影响日益增强。初等几何是数学领域的一个重要研究课题,自从欧几里得创立初等几何以来,几何学的发展就离不开初等几何,之后的射影几何、非欧几何等都是在初等几何的基础上发展过来的。杨路定理是由我国著名数学家杨路先生提出的一个初等几何定理,杨路定理作为开普勒定理的一个扩展,现已被收录进日本岩田志康先生所编纂的《几何学大辞典》中,是非常具有代表性的一个定理,在海外也拥有着不俗的影响。在对杨路定理进行形式化证明的前期准备中,我们不仅可以构建出一系列初等几何的概念,还可以引入坐标、向量等解析几何的概念,最后我们通过构建出来的概念和性质等对杨路定理进行描述和证明。本文借助辅助证明工具Coq,完成了点、线、面、角等初等几何概念和向量、坐标的构建。最后我们给出了杨路定理的完整描述与机器证明。本文的创新点在于利用交互式辅助证明工具Coq进行机器证明,并且这是杨路定理的首次形式化,是对于初等几何体系形式化搭建的一次尝试,将来我们可以在此基础上进行更多的尝试,发展出更多不同的几何体系。

论文目录

• 摘要
• abstract
• 第一章 绪论
•   1.1. 研究的背景和意义
•     1.1.1. 数学机械化
•     1.1.2. 形式化方法
•     1.1.3. 辅助证明工具Coq
•     1.1.4. Coq取得的成果
•     1.1.5. 杨路定理
•   1.2. 研究意义
•   1.3. 本文的结构安排
• 第二章 辅助证明工具Coq的基础语法
•   2.1. Coq中的项
•     2.1.1. 类型
•     2.1.2. 表达式
•   2.2. 项的声明与定义
•     2.2.1. 全局声明和定义
•     2.2.2. 局部声明和定义
•   2.3. 环境和上下文
•   2.4. Coq中的命题描述
•     2.4.1. 量词
•     2.4.2. 依赖积
•     2.4.3. 命题描述语法
•   2.5. Coq中命题的证明策略
• 第三章 证明的前期准备
•   3.1. 点的构建
•   3.2. 线段的长度
•   3.3. 向量的构建
•   3.4. 角度的构建
•   3.5. 平行与垂直
•   3.6. 面的构建
•   3.7. 四边形
•   3.8. 等腰三角形
•   3.9. 等边三角形
•   3.10. 三角形面积
•   3.11. 连加
•   3.12. 平均中心
• 第四章 杨路定理的证明
•   4.1. 杨路定理的人工证明
•   4.2. 杨路定理的Coq实现
• 第五章 总结与展望
•   5.1. 工作总结
•   5.2. 研究展望
• 参考文献
• 致谢

文章来源

类型: 硕士论文

作者: 傅凡

导师: 郁文生

关键词: 机器证明,初等几何,杨路定理

来源: 北京邮电大学

年度: 2019

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

专业: 数学,自动化技术

单位: 北京邮电大学

分类号: O18;TP18

总页数: 67

文件大小: 3740K

下载量: 46