论文部分内容阅读
数学问题的计算机证明也称数学机械化，是指用计算机证明、推理计算数学问题。Mizar语言系统是由波兰华沙大学的AndrzejTrybulec教授为首的数学家和计算机专家在上世纪八十年代开创的集逻辑证明、校验、排版功能于一体的计算机语言系统。该系统如今拥有自己的数据库MML，其中收录了几乎涵盖了数学各个分支的1000多篇数学论文，并且还解决了像连续格的证明、Jordan曲线及Brouwer不动点等定理，这类人们用手无法计算和证明的复杂问题。同时，它在自动化控制、声音和图像识别等研究领域也有着广泛的应用。
本文首先介绍了Mizar语言系统的发展历史，其次给出了在该系统下证明和自动校验数学命题的方法，在此基础上针对一元函数高阶导数的不同问题，给出了相应的Mizar算法。作者的主要工作如下：
1.在Mizar语言系统下给出了几类一元函数高阶导数公式的实现方法；
2.实现了广义指数函数的Mizar语言定义方法，证明了其复合函数的可微性定理并推导了其高阶导数公式；
3.给出了推导初等函数、超越函数和复合函数n阶导数公式的Mizar语言算法，并给出了应用说明；
4.验证了函数高阶导数的运算法则及其定理的Mizar语言实现方法，并给出了简要的应用说明。
以上结果均已通过Mizar语言系统的验证，被收录在Mizar数据库MML中。