学位论文 > 优秀研究生学位论文题录展示

幂零群p-群若干性质的计算机证明

作　者: 李代鲁
导　师: 梁希泉
学　校: 青岛科技大学
专　业: 基础数学
关键词: 粗糙子群幂零群 p-群 p-交换群
分类号: O152.1
类　型: 硕士论文
年　份: 2010年
下　载: 21次
引　用: 0次
阅　读: 论文下载

内容摘要

当前,数学问题计算机证明的研究已成为世界各国积极研究的前沿领域。随着计算机技术的发展,人们已根据机械化方法创建了各种机器语言来编写程序,在计算机上给出相应数学问题的机器证明。本文介绍了数学问题计算机证明的Mizar语言系统,应用Mizar语言系统对有限群不同问题给出了相应的证明,主要工作如下：1.在某种意义下将群的子群与群的同余关系同等看待,在Mizar语言系统下定义了群的子集关于子群的上、下近似,证明了粗糙子集的若干性质；2.应用群的正规子群与群的同余关系一一对应关系,在Mizar语言系统下得出群的子群关于正规子群的上、下近似并进一步得到群的粗糙子群的理论；3.给出了幂零群Mizar语言系统下的定义,证明了幂零群的若干性质和幂零群的充要条件；4.给出了若干幂零群的充分条件,指明了幂零群与可解群的关系；5.给出了p-元素Mizar语言系统下的定义,证明了p-群的等价定义,讨论了p-群的若干性质；6.在p-群的基础上给出了p-交换群的定义,证明了p-交换群的若干性质。以上结果已经通过Mizar语言系统的验证,相关内容已经在Formalized Mathematics发表。

全文目录

摘要  3-4
英文摘要  4-7
1 绪论  7-11
  1.1 数学问题计算机证明的历史及发展现状  7
  1.2 Mizar系统的历史和发展现状  7-8
  1.3 课题研究的目的和意义  8-9
  1.4 课题研究的主要内容  9-11
2 Mizar语言  11-21
  2.1 Mizar文章结构  11-13
  2.2 Mizar语言系统的基本符号和语法词汇  13-14
  2.3 Mizar语言系统的证明方法  14-18
  2.4 Mizar语言系统中的定义  18-21
3 粗糙子群性质的计算机证明  21-37
  3.1 预备知识分析  21-22
  3.2 群的粗糙子集与粗糙子群性质的计算机证明  22-35
    3.2.1 群的子集关于子群的上、下近似的Mizar定义  22-24
    3.2.2 群的子集关于子群的上、下近似的性质  24-27
    3.2.3 群的子集关于子群的二重近似  27-30
    3.2.4 群的子群关于子群的上、下近似的计算机证明  30-34
    3.2.5 群的子群关于正规子群的二重近似  34-35
  3.3 最终实现的Mizar形式及成果出处的Mizar版本  35-37
4 幂零群性质的计算机证明  37-49
  4.1 预备知识分析  37-38
  4.2 幂零群性质的计算机证明  38-47
    4.2.1 环境部设置  38
    4.2.2 正文部分  38-47
  4.3 最终实现的Mizar形式及成果出处的Mizar版本  47-49
5 p-群性质的计算机证明  49-57
  5.1 预备知识分析  49
  5.2 p-群与p-交换群性质的计算机证明  49-55
    5.2.1 p-元素与p-群性质的计算机证明  49-52
    5.2.2 p-群幂指数的计算机证明  52-53
    5.2.3 p-交换群的计算机证明  53-55
  5.3 最终实现的Mizar形式及成果出处的Mizar版本  55-57
总结与展望  57-58
参考文献  58-61
致谢  61-62
攻读学位期间发表的学术论文目录  62-64

幂零群p-群若干性质的计算机证明

内容摘要

全文目录

相似论文