| With the development of artificial intelligence technology,mathematical mechanization has increasingly significant influence on the cross field of computer and mathematics.As one of the important research directions of mathematical mechanization,machine proving means completing proof of theorems by computer and auxiliary proof software.Coq is a current international auxiliary proof software,which is based on the theory of inductive construction calculus and is rigorous and reliable.At the same time,the interactive proof environment of Coq enhances the readability of the code.Currently,Coq is widely applied to machine proving of various mathematical problems,especially the computer proving of the famous "four color theorem" in Coq by Gonthier and Werner in 2005,which enhanced Coq's influence on academia.Inequality is an important research topic in the field of mathematics,and almost all branches of mathematics are inseparable from inequality.The research on the machine proving of inequality has great application value.New results have been emerging in recent years.Some inequalities have been proved by general programs,which is based on Mathmatica and Maple.By means of Coq,Isabelle,HOL Light and so on,the machine proving for several fundamental applied inequalities has been also successfully implemented.In this paper,we implement the machine proving for seven fundamental applied inequalities by Coq.These inequalities include arithmetic-geometric-harmonic inequality,Cauchy inequality,arrangement inequality,Chebyshev inequality,Bernouli inequality,triangle inequality and Jensen inequality.It should be pointed out that the traditional mathematical proof methods of these inequalities and their equivalent propositions are found in many literatures.The innovation point of this paper is to use the interactive auxiliary proof software Coq,and give the formal machine proving of these propositions.The proving process embodies the reliability and interactivity of the machine proving by Coq. |
PDF Full Text Request