2010级信息与计算科学专业导论

《2010级信息与计算科学专业导论》由会员上传分享，免费在线阅读，更多相关内容在教育资源-天天文库。

1、信息与计算科学专业导论学号姓名成绩数学机械化一、数学机械化简介证明定理：古希腊：欧几里德几何学数学活动解方程：古代中国数学二、什么是数学机械化？所谓机械化，无非是刻板化和规格化。数学问题的机械化就要求在运算或证明过程中，每前进一步之后，都有一个确定的、必须选择的下一步，这样沿着一条有规律的、刻板的道路，一直达到结论。数学机械化—从设想到实现从笛卡尔、莱布尼兹、希尔伯特、塔斯基、王浩、吴文俊等数学家的思想来看一下数学机械化从设想到实现的简要历史。1．Descartes的设想首先，把任一问题转化为数学问题第二,将任一数学问题转化为代数问题第三，将任一代数问题转化为单个方程求解评价：笛卡尔的

2、计划失败了，但它人不失为一个伟大的计划，而且即使失败了，它对数学的影响也超过了偶尔获得成功的千万个计划。2．Leibniz之梦德国数学家Leibniz曾有过“推理机器”的设想。他研究过逻辑，设计并制造出能做乘法的计算机，进而萌发了设计万能语言和造一台通用机器的构想。他的努力促进了Boole代数、数理逻辑以及计算机科学的研究，正是沿着这一方向，经后人的努力，形成了机器定理证明的逻辑方法。3．Hilbert的《几何基础》Hilbert在《几何基础》中提出了从公理化走向机械化的数学构想。Hilbert计划将数学知识纳入严格的公理体系中，并着力在公理化基础上寻找机械化的方法判定命题是否成立。在

3、书中就提供了一条可以对一类几何命题进行判定的定理—当然，在那个时代，不仅Hilbert本人，整个数学界都没有意识到这一点。4.Tarski的定理波兰数学家Tarski在1950年推广了关于代数方程实根数目的Sturm法则，由此证明了一个引人注目的定理：“一切初等几何和初等代数范围的命题，都可以用机械方法判定。”Tarski得出的结论给定理证明机械化的研究带来了曙光。可惜他的方法太复杂，即使用高速计算机也证明不了稍难的几何定理。5．王浩的定理机器证明程序1959年，王浩设计了一个程序，用计算机证明了Russell、Whitehead的巨著《数学原理》中的几百条有关命题逻辑的定理，仅用了9

4、分钟。王浩工作的意义在于宣告了用计算机进行定理证明的可能性。6．吴方法的产生1977年，吴文俊在《中国科学》上发表论文《初等几何判定问题与机械化问题》。1984年，吴文俊出版学术专著《几何定理机器证明的基本原理》。这部专著着重阐明几何定理机械化证明的基本原理，与国际上流行的代数理想论不同，明确提出了具有中国自己特色的、以多项式零点集为基本点的机械化方法。自此，“吴方法”宣告诞生，数学机械化研究揭开了新的一幕。吴方法遵循中国传统数学中几何代数化的思想，首次实现了高效的几何定理自动证明，显现了无比的优越性。他的工作被称为自动推理领域的先驱性工作，并于1997年获“Herbrand自动推理杰

5、出成就奖”。在授奖辞中对他的工作给了这样的评价:“几何定理自动证明首先由赫伯特·格兰特于50年代开始研究。虽然得到一些有意义的结果，但在吴方法出现之前的20年里，这一领域进展甚微。在不多的自动推理领域中，这种被动局面是由一个人完全扭转的。吴文俊很明显是这样一个人。他将几何定理证明从一个不太成功的领域变为最成功的领域之一。”一、数学机械化或机器证明方面：从初等几何着手，在计算机上证明了一类高难度的定理，同时也发现了一些新定理，进一步探讨了微分几何的定理证明。提出了利用机器证明与发现几何定理的新方法。这项工作为数学研究开辟了一个新的领域，将对数学的革命产生深远的影响。1978年获全国科学大

6、会重大科技成果奖。二、中国数学史方面：吴文俊认为中国古代数学的特点是：从实际问题出发，经过分析提高，再抽象出一般的原理、原则和方法，最终达到解决一大类问题的目的。他对中国古代数学在数论、代数、几何等方面的成就也提出了精辟的见解。三、主要参考书目1.数学机械化，吴文俊著，科学出版社，20032.方程求解与机器证明，高小山等，科学出版社，2003六、主要软件1.（数学机械化平台)http://www.mmrc.iss.ac.cn/mmp2.DISCOVERERhttp://www.is.pku.edu.cn/~xbc/software.html