Nilpotent Groups P-groups In Computer

Currently, the Mathematics problems on a computer that has become actively research frontier in the world. With the development of computer technology, people under various mechanized method to create a machine language program, and on the computer to the math problem proving.This paper describes the history of Mizar system and the method of proveing and automatic identification. Firstly in order to carry out the calculator of mathematics problem,we should give the method of mathmatic deduction and calculator which can be identified and identificated by computer,prove some properties of finite groups under this systerm. The author's main work as follows:1. reviewed the subgroup of a group as congruence relations equally in a certain sense, the definition of subsets on subgroups of a group approximation are given, some properties of rough subsets are proved;2. normal subgroups of group and congruence relations one-to-one relationships, subgroups on normal subgroups of group approximation and the theory of rough subgroups are given;3. the definition of nilpotent group is given in Mizar, some properties of nilpotent group are proved and the necessary and sufficient conditions of nilpotent group are proved;4. some nilpotent sufficient conditions are given, and the relation nilpotent and solvable groups is indicated;5. the definition of p-element is given,the equivalent definitions of p-groups are proved as well as some properties of p-groups are discussed;6. the definition of p-commutative groups is given on the basis of p-groups,and some properties of p-commutative groups are proved.These results have been verified by the Mizar,and relevant content has been published in Formalized Mathematics.