The Abstract Algebra Thesis Based On Coq

Abstract algebra,also known as modern algebra,is an important basic branch of modern science.Generally speaking,abstract algebra is a discipline that studies algebraic systems.Its central problem is.studying the laws of numbers,words and more general elements’ algebraic operations and the properties of various algebraic structures-group,ring,domain,which are the most basic algebraic structures.Because of the algebraic structure and the generality of its elements,it has become the basic tool and language of many scientific fields such as mathematics,physics and computer science.With the rapid development of computer science,especially the emergence of interactive theorem proving tools Coq,the formal proof of mathematical theorem has made great progress in recent years.more and more researcher use Coq to prove the theorems recently years.Coq itself is also rapidly developed.This thesis makes the following contributions:For the first time,we use the interactive theorem proving tool Coq to define the basic theory of modern algebra.The whole system starts with naive set theory.First of all,a series of basic conceptions,such as set and map,are constructed.Then we add operations on the set and introduce the conception of algebraic system.Finally we discuss the characteristics of group、ring and domain.The machine proving of the Factorization Theorem of Principal Ideal Domain is given.The Factorization Theorem of Principle Ideal Domain is pretty important in the abstract algebra.The theorem starts with the integral domain.The relationship between the integral domain and the unique factorization ring is introduced.The theorem has been applied in many fields.The complete machine proving of the Factorization Theorem of Principal Ideal Domain in the abstract algebra is given by using the interactive theorem proving tool Coq.The proof process is completed by using Coq,which fully embodies the Coq-based mathematics theorem machine proving system are readable and intelligent.The machine proving progress is rigorous and reliable.