论文部分内容阅读
Mizar系统是从人工智能的一个分支——定理自动证明的发展过程中产生和发展起来的，是用来构建Mizar数学知识库的证明校验系统，是一个数学定理证明工具。Mizar系统由波兰华沙大学的Andrzej Trybulec教授组织的Mizar协会领导，其逻辑框架基于Ja(?)kowski自然演绎推理的古典逻辑。Mizar如今已经成为集逻辑证明、校验、排版功能于一体的数学知识处理的形式化系统，拥有自己的数据库MML，其中收录了波兰、日本、中国、加拿大等多个国家的教授学者和研究生完成的960多篇数学论文，几乎涵盖了数学的各个分支，尤其是在连续格的证明、Jordan曲线及Brouwer不动点等定理的证明中突显出Mizar语言系统的优越性。本文首先介绍了定理机器证明及Mizar系统的历史，其次对如何利用Mizar语言完成数学论文和进行自动推理校验给出了简要的说明。本文主要研究了以Mizar系统为平台，证明一类特殊函数的微分公式、函数的差分差商和实现任一实数的连分数形式。主要的创新点如下：1．将Mizar系统中的可微性判定及基本函数的性质定理应用于几类复合函数，实现了它们在Mizar系统中的自动推理证明；2．为了实现函数的差分与差商，在Mizar系统中首次定义了平移算子、向前差分算子、向后差分算子和中心差分算子，并由此定义了三种无穷差分序列forward_difference、backward_difference和central_difference，讨论了三者之间的相互关系，应用Mizar语言完成了相关定理的自动推理证明，并验证其正确性；3．首创性地在Mizar中定义了任一实数的连分数形式及其渐近分数，讨论了连分数及渐近分数分子、分母的有关性质，利用渐近分数的性质完成了任一实数的渐近分数的Mizar实现，并给出证明其渐近性质的机械化方法。以上结果都通过了Mizar系统的验证，均被收录到最新的Mizar数据库MML中，并发表于2005和2006年的Formalized Mathematics期刊。