Formalization and Verification of Cyclic Group

At present, the formal method is an important system design verification method, which effectively compensates the “incomplete” problem of the traditional methods such as simulation and testing in the system design verification. Since the logical method as a typical formal method is our research direction, we naturally choose the first-order logic language in the logical method to formalize Group theory in the field of mathematics. Based on some formalized conclusions of Group theory in TPTP, this paper completes the formal description of missing definitions about the Group in TPTP, namely the order of element in group, nth-order cyclic group and Klein four-group. Some propositions and theorems related to these definitions are further formal described, and the correctness of these descriptions is verified by the theorem tool Prover9.