Integration Of Some Special Functions And Reduced Residue System In Mizar

The Mizar system is a computer language system which is created and developde with the development of formalize mathematics,used for proving and calculating mathematical problems.Mizar is a proof checker which is used in building Mizar Mathematical Library. Mizar was created to describe mathematical concepts and theorems by checking them with a Mizar proof checker on a IBM-PC for Mizar library registration. Mizar has a Mizar Mathematical Library containning 1126 articles , more than 2 million math concepts, and more than 40 million theorem, almost covering all branches of mathematics. It is also applied in many fields such as autocontrol,voice,image identification etc,and sets a good foundation to mathematics and the related major.This dissertation describes the history and the present domestic and overseas condition of formalize mathematics and the Mizar system. Based on the research of mathematic mechanization and the Mizar system, the author makes a discussion on some problems which integration of some special functions and the reduced residue system in the number theory, and provides the corresponding proof and calculation methods in Mizar system. The main contents are summarized as follows:1. Integration formula of some special functions is formalized concisely in Mizar system, including rational function, irrational function,triangle function,anti-trigonometric function, exponential function, logarithmic function,composite function.2. For the first time a singular point inside integrate interval of improper integral and two singular points are the right and left endpoints of integrate interval is formalized in Mizar system , the interrelated operation formulas and theorems are also given.3. The reduced residue system is defined and its fundamental properties are proved with Mizar system.4. The basic properties of the exponent function are formalized concisely in Mizar system .Base on the definition of the reduced residue system, primitive root is defined,and the reduced residue system in terms of geometrical series is formalized according to the relationship of the reduced residue system and primitive root for the first time.The automatic reasoning and proving process, which are related to the above aspects, have been completed in Mizar system.