Formalization Of The Basic Framework Of Ring And Field Theory Based Of Coq

Artificial intelligence technology is one of the country’s major scientific and technological development strategies and a very important branch in the development of computer science.With the computerization of modern society and the increasing level of intelligence,various system failures related to computers will often cause huge economic losses in modern society,and what’s more,they will endanger the safety of human life.Therefore,consolidating the basic theory of artificial intelligence is particularly important for modern intelligent society.Theorem machine proof can establish more strict correctness for programs,thus establishing high credibility of the system,which is a profound manifestation of the basic theory of artificial intelligence.The interactive theorem proving tool Coq is a powerful tool for machine proving mathematical theorems.The order structure,algebraic structure and topological structure of Burbage school are the foundation of modern mathematics.These three structures blend with each other and form the main content of modern mathematics.The formal system of these three structures can be completely constructed by using Coq,a computer-aided proof tool.Due to the generality of algebraic elements,algebraic structures are used as basic tools and languages in many fields.Algebraic systems,that is,sets with operations,are the basic objects of algebraic research.Modern algebra is a discipline that studies algebraic systems and has important applications in other branches of mathematics and many departments of natural science.In modern science,some of its achievements have been directly applied to the research of some emerging technologies,such as cryptography,etc.Rings and fields are the most basic algebraic systems in modern algebra.Based on the interactive theorem proving aid Coq,this paper formalizes the basic theoretical framework of rings and fields in modern algebra.The main work is as follows:(1)Using the interactive theorem prove tool Coq,starting from the mathematical basic concepts such as set and mapping,the formalization of the basic concepts needed to construct algebraic systems is realized.The formalization of these basic concepts has high reusability,and can be used to construct a variety of algebraic systems,as well as other mathematical systems that need to use these concepts,such as sequential structures,topological structures,calculus,etc.(2)Formalize the two algebraic systems of ring and domain in modern algebra,and complete the theorem proving of the basic properties of these two algebraic systems.(3)The fundamental theorem of ring homomorphism is an important content in modern algebra and is the most effective tool to compare two algebraic systems.It can be used to concretize the problems of abstract algebraic systems.In this paper,the interactive theorem proving tool Coq is used to give the machine proof of the fundamental theorem of ring homomorphism.The whole proving process is completed by Coq code,which reflects the readability and intelligence of the mechanical proof of mathematical theorem based on Coq.The proving process is standard,rigorous and reliable.