Odd Function And Even Function And Periodic Funtion In Mizar

The main objective of mathematics mechanization is to use computers to deduce and prove mathematical propositions and theorems. Presently, many organizations are taking active part in the study of formalized mathematics. There are many kinds of machine languages system which are used to prove mathematical theorems, and several of them are recognized such as Mizar, PVS, Coq etc. However, Mizar language system has developed rapidly, and accepted broad attention in the world. Nowdays, Mizar has already developed the mathematic knowledge treatment system including a lot of function. Mizar Mathematical Library has included more than 1090 articles and almost contains all branches of mathematics, especially in the formalization of topology theorem and Functional Analysis theorems.Firstly this paper describes the history of Mizar system and the way to write Mizar articles. Then the definitions of odd function, even function and periodic function are given with the Mizar system,and the properties of odd function, even function and periodic function are presented and proved with Mizar. The main work of this paper as follows:1.the definitions of quasi odd function,quasi even function,odd function and even function are presented through Mizar system.2. periodic function is defined in Mizar system for the first time.3. proofs of odd function, even function and periodic function properties are completed with the Mizar system.4.proved properties of some functions based on Mizar, such as triangle function,absolute function,sign function.5.defined sign function and showed its properties in Mizar system.All of the above contribution has passed the check of Mizar system,and published in the journal of Formalized Mathematics, and included by the MML(Mizar Mathematical Library).