论文部分内容阅读
当前，随着时代的进步，人们越来越不满足于落后的科学技术，正在研究怎样用高科技来解决一些复杂问题，以便从众多繁复的脑力劳动中解脱出来，在这种形势下，数学问题的计算机证明已经成为了世界各国数学家们积极研究的前沿领域。随着计算机技术的发展，人们已根据机械化方法创建了各种机器语言来编写程序，有些程序是专门为数学而打造的，能在计算机上给出相应数学问题的模型构建和机器证明。
本文介绍了差分和差商问题在Mizar语言系统下的实现，用Mizar语言系统对差商和差分不同问题给出相应的证明，主要工作如下：首先介绍了数学机械化及Mizar系统的历史和发展现状，其次简要说明如何利用Mizar语言完成数学论文的撰写和证明。在Mizar系统下给出了特殊函数的差分和差商的证明过程及差分和差商的部分性质，而后给出了零阶差分和多阶差分的定义及性质的证明过程。
以上结果已经通过Mizar语言系统的验证，部分相关内容已经在《FormalizedMathematics》中发表。