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