从吴文俊和吴方法谈起.ppt
《从吴文俊和吴方法谈起.ppt》由会员分享,可在线阅读,更多相关《从吴文俊和吴方法谈起.ppt(35页珍藏版)》请在三一办公上搜索。
1、1,从吴文俊和吴方法谈起,数学机械化的观点 数学文化课程组 李军,2,吴文俊 中国科学院院士 第三世界科学院院士 首届国家最高科技奖 国家第一届自然科学奖 最高奖一等奖 自动推理的最高奖Herbrand奖 2006邵逸夫数学奖,3,最近,著名数学家吴文俊荣获邵逸夫数学科学奖。邵逸夫数学科学奖是一项国际性大奖,它的评委是来自国际数学界的知名权威。吴文俊说:这次邵逸夫奖的评委都是国际上有影响的大家,他们宣布我获得邵逸夫奖,是因为我的数学机械化问题的研究,这实际上是国际数学界对数学机械化研究的承认与肯定,它比奖金重要得多。,数学机械化得到国际数学界承认,4,中央电视台大家栏目:吴文俊我的不等式片断,
2、5,什么是数学机械化,所谓机械化,无非是刻板化和规格化。数学问题的机械化,就要求在运算或证明过程中,每前进一步之后,都有一个确定的、必须选择的下一步,这样沿着一条有规律的、刻板的道路,一直达到结论。使用一种机械化方法证明一类定理,才真正体现了机械化定理证明。1977年,吴文俊给出了初等几何一类主要定理的机械化证明方法“吴方法”。,6,数学机械化:从设想到实现,笛卡尔 莱布尼茨 希尔伯特,7,数学机械化:从设想到实现,哥德尔 塔斯基 王浩 吴文俊,8,笛卡尔的设想,17 世纪法国的数学家 Descartes 曾有过一个伟大的设想:“一切问题化为数学问题,一切数学问题化为代数问题,一切代数问题化为
3、代数方程求解问题。”Descartes 把问题想得太简单了,如果他的设想真能实现,那就不仅是数学的机械化,而是全部科学的机械化。因为代数方程求解是可以机械化的。但 Descartes 没有停留在空想,他所创立的解析几何,在空间形式和数量关系之间架起了一座桥梁,实现了初等几何问题的代数化。,9,莱布尼兹之梦,德国数学家 Leibniz 曾有过“推理机器”的设想。他研究过逻辑,设计并制造出能做乘法的计算机,进而萌发了设计万能语言和造一台通用机器的构想。他的努力促进了 Boole 代数、数理逻辑以及计算机科学的研究,正是沿着这一方向,经后人的努力,形成了机器定理证明的逻辑方法。,10,希尔伯特的构想
4、,Hilbert在几何基础中提出了从公理化走向机械化的数学构想。Hilbert计划将数学知识纳入严格的公理体系中,并着力在公理化基础上寻找机械化的方法判定命题是否成立。Hilbert同时指出,定理的判定问题应当是分类解决的,解决方法要同时强调简单性和严格性。在 Hilbert 的名著几何基础一书中就提供了一条可以对一类几何命题进行判定的定理 当然,在那个时代,不仅 Hilbert 本人,整个数学界都没有意识到这一点。,11,哥德尔的著名结果,Gdel著名的不完全性定理指出一个不弱于初等数论的形式系统如果是无矛盾的,则是不完全的,即存在形式系统的一个命题,它和它的否定都不能由形式系统证明。因此,
5、Hilbert 的要求太高了。上述的Gdel不完全性定理断言:即使在初等数论的范围内,对所有命题进行判定的机械化方法也是不存在的!,12,塔斯基的判定法,波兰数学家 Tarski 在 1950 年推广了关于代数方程实根数目的 Sturm 法则,由此证明了一个引人注目的定理:“一切初等几何和初等代数范围的命题,都可以用机械方法判定。”Tarski得出的结论给定理证明机械化的研究带来了曙光。可惜他的方法太复杂,即使用高速计算机也证明不了稍难的几何定理。,13,王浩:迈向数学机械化,1959 年,王浩设计了一个程序,用计算机证明了 Russell、Whitehead 的巨著数学原理中的几百条有关命题
6、逻辑的定理,仅用了 9 分钟。王浩工作的意义在于宣告了用计算机进行定理证明的可能性。在1960年的IBM研究与发展年报(IBM Journal),王浩发表了迈向数学机械化(Toward Mechanical Mathematics),“数学机械化”一词即出自此处。,14,吴文俊:机器证明领域的新的一页,1977 年,吴文俊在中国科学上发表论文初 等几何判定问题与机械化问题。1984 年,吴文俊的学术专著几何定理机器证明的基本原理由科学出版社出版,这部专著着重阐明几何定理机械化证明的基本原理。1985 年,吴文俊的论文关于代数方程组的零点发表,具体讨论了多项式方程组所确定的零点集。与国际上流行的
7、代数理想论不同,明确提出了具有中国自己特色的、以多项式零点集为基本点的机械化方法。自此,“吴方法”宣告诞生,数学机械化研究揭开了新的一幕。,15,吴文俊我的不等式片断,16,三角形三条高线交于一点的代数证明,D是BC和CA上高线交点,17,定理的假设部分是,由吴方法,可得非退化条件是,.定理的结论是CO经过D点,.显然在非退化条件下定理成立。,18,Morley定理,任意三角形中,一个角的三等分线,与和它相邻的角的三等分线相交,交点组成正三角形。,19,机器方法容易证明Morley定理,任意三角形中,一个角的三等分线,与和它相邻的角的三等分线相交,按一定的规则选取交点,共可组成27个三角形,在
8、这27个三角形中,一定有18个是正三角形。用机器方法容易证明这个更一般的Morley定理。在证明过程中,多次出现关于12个变量的含有一千多项的多项式。,20,吴方法概要,定理的假设相当于一组多项式方程定理的结论相当于一个多项式方程上面的诸Fi称为假设多项式,G称为终结多项式。,21,吴方法概要(续),吴方法是给出了一个机械化方法,在有限步内给出一组非退化条件多项式D1,Dr 又根据这一机械化方法足以在有限步内,判定在非退化条件 D10,Dr 0 下,G=0是否可从F1=0,Fs=0推出。,22,对吴方法的评价,吴方法遵循中国传统数学中几何代数化的思想,与通常基于数理逻辑的方法根本不同,首次实现
- 配套讲稿:
如PPT文件的首页显示word图标,表示该PPT已包含配套word讲稿。双击word图标可打开word文档。
- 特殊限制:
部分文档作品中含有的国旗、国徽等图片,仅作为作品整体效果示例展示,禁止商用。设计者仅对作品中独创性部分享有著作权。
- 关 键 词:
- 吴文俊 方法 谈起
链接地址:https://www.31ppt.com/p-5766382.html