基于Coq的近世代数机器证明系统

rtificial intelligence research is one of the major scientific and technological development strategies in our country at present, and it is especially important to consolidate the theoretical basis of artificial intelligence.Mechanical theorem proving is a profound manifestation of the basic theory of artificial intelligence. Based on the interactive theorem proving tool Coq, this paper relizes the formalization of modern algebraic systems, including the formal description of basic algebraic structures such as group, additive group, ring, integral ring, division ring, domain, etc. On this basis, the machine proof of an important theorem in rings, the fundamental theorem of homomorphism of rings, is completed to verify the correctness of Coq description.All contents of this system are formalized and verified by Coq, which reflects the interactive and readable characteristics of Coq-based mathematical theorem machine proof, and the proof process is standardized, rigorous, and reliable. It is also the three main structures(ordered structure, algebraic structure, topological structure)of mathematics of theSchool of Bourbaki on mathematics an essential part of the formalization of algebraic structure.