A Study Of Formalization And Validation Of Group Theory Problem

In the paper,a typical formal method,the logical method,is used as the research direction,that is,how to apply the computer program to prove the mathematical theorem.Specifically,how to formalize the reasoning process of the human brain through a set of symbolic systems and then is transformed into a series of reasoning proof processes that can be implemented automatically on a computer.It is an important task of the theorem prover to represent the mathematical theorem and the proof process for using the formal language(logical language),so that the expression of the mathematical theorem and each step of the theorem proof process can be verified by the computer program.We must use the formal language with strict grammatical rules and explicit semantics to express mathematical objects,including definitions,propositions and proofs.In this paper,the first-order logic language is used to formalize the Group theory in mathematics,and the theorem proving system Prover9 is used for formal verification.Some achievements are listed as follows:1.Based on two aspects of the formal method-formal description and formal verification,the basic steps of formalization process of Group theory are given.2.Based on some formalized conclusions of Group theory in TPTP,this paper presents the formal description methods of Group operation closeness,identity element,inverse element,combination law,elimination law,exchange law,identity element uniqueness and inverse element uniqueness,a set of satisfying certain condition.Thus this paper completes the formal description of missing definitions about the Group in TPTP,namely the Abelian group,the Normal subgroup,the normalizer and centralizer.Then some related propositions and theorems are formal described.And the correctness of the formal description is verified by the theorem Prover9.3.An open problem in Group theory is chosen.This problem is tried to formalized and solved.According to the formal method used in this paper,the solution to this problem is advanced.