数学问题机械化是指用计算机推理、证明、计算数学问题和定理。目前，世界各国都在积极地进行数学问题机械化的研究，比较著名的数学定理证明系统有Mizar、PVS、Coq等，而Mizar语言系统凭借其庞大的MML数据库和其优越的功能，得以快速发展，深受世界各国的重视。Mizar语言系统已经发展成为集众多功能于一体的数学知识处理系统，目前MML数据库已经收录1090多篇数学论文，其内容几乎涵盖了数学的各个分支，尤其是在拓扑学及泛函分析学等学科的定理证明中更突显出Mizar语言系统的优越性。　　 本文首先介绍了Mizar系统的发展历史，接着给出了奇函数、偶函数及周期函数的Mizar定义，同时完成了奇函数、偶函数及周期函数的性质在Mizar系统下的实现和论证。本文主要工作如下：　　 1.给出了拟奇函数及拟偶函数的Mizar系统下的定义，同时，在复数域上给出奇函数及偶函数的定义，将分析学中奇偶函数的定义加以推广并在Mizar系统下实现；　　 2.在Mizar系统下给出了周期函数及周期的定义；　　 3.基于Mizar系统论证了奇函数、偶函数及周期函数的性质以及某些复合函数的奇偶性及周期性；　　 4.在Mizar系统下，证明了一些初等函数的奇偶性及周期性，例如：常函数、符号函数、绝对值函数及某些三角函数；　　 5.进一步完善了Mizar系统下符号函数的定义及性质的论证。　　 以上结果都通过了Mizar系统的验证，均被收录到最新的Mizar数据库MML中并发表在Formalized Mathematics期刊。