关键词：
Coq
近世代数
主理想环
唯一分解环
机器证明
摘要：
近世代数是现代科学的一个重要基础分支。简单地说,近世代数是研究代数系统(带有一些运算的集合)的学科,它以研究数字、文字和更一般元素的代数运算的规律及各种代数结构——群、环、域是其最基本的三种代数结构——的性质为中心问题。由于近世代数贯穿于各种科学理论与应用问题,也由于代数结构及其元素的一般性,近世代数学已成为当今数学、物理及计算机科学等多个科学领域的基本工具和语言。随着计算机科学的迅猛发展,特别是交互式定理证明辅助工具Coq的出现,近年来数学定理的形式化证明研究取得了长足的进展。近些年来越来越多的研究人员使用Coq来证明数学定理,Coq本身也由此迅速发展。本文的主要贡献如下:·利用交互式定理证明工具Coq构建了近世代数的基础理论。整个近世代数系统由朴素集合论出发,首先构建了集合、映射等一系列基础概念,并在集合上增加运算,引入了代数系统的概念,讨论群、环、域的性质,进而给出了整环的因式分解定理证明的Coq实现。·主理想环因式分解定理是近世代数中的重要内容,该定理由整环出发,阐述了整环和唯一分解环之间的关系,在很多领域都得到了深刻的应用。本文利用交互式定理证明工具Coq,给出近世代数中主理想环因式分解定理的机器证明,全部证明过程由Coq代码完成,体现了基于Coq的数学定理机器证明具有可读性、智能性的特点,其证明过程规范、严谨、可靠。
欢迎来到三峡大学图书馆！
详细信息
