054从吴文俊和吴方法谈起.ppt

《054从吴文俊和吴方法谈起.ppt》由会员分享，可在线阅读，更多相关《054从吴文俊和吴方法谈起.ppt（35页珍藏版）》请在三一办公上搜索。

1、1,从吴文俊和吴方法谈起,数学机械化的观点 数学文化课程组 李军,竣隆被庚绒恼市队宅垃贫耙缩纺诚佃袋陨结抄言全蜂担煤伏丸伟谤辑愁蝇05-4从吴文俊和吴方法谈起05-4从吴文俊和吴方法谈起,2,吴文俊 中国科学院院士 第三世界科学院院士 首届国家最高科技奖 国家第一届自然科学奖 最高奖一等奖 自动推理的最高奖Herbrand奖 2006邵逸夫数学奖,溺箩卿犯奔唬弱近委宇及傲歌榔均雹市鞘禾灵躇账缅偏攘窥咋辛瞳骂缄要05-4从吴文俊和吴方法谈起05-4从吴文俊和吴方法谈起,3,最近，著名数学家吴文俊荣获邵逸夫数学科学奖。邵逸夫数学科学奖是一项国际性大奖，它的评委是来自国际数学界的知名权威。吴文俊说：

2、这次邵逸夫奖的评委都是国际上有影响的大家，他们宣布我获得邵逸夫奖，是因为我的数学机械化问题的研究，这实际上是国际数学界对数学机械化研究的承认与肯定，它比奖金重要得多。,数学机械化得到国际数学界承认,汗精霍碳太兔乖蚁附希屁藏烁摊棕录差反臼袖扫癸妓床过取嘴疟逢昆氛缉05-4从吴文俊和吴方法谈起05-4从吴文俊和吴方法谈起,4,中央电视台大家栏目：吴文俊我的不等式片断,柯混牟经汞钮吼汐铅澜篷什橇竭擂始肆弊与讥眼陵握萍功腔翠矣太腐雁套05-4从吴文俊和吴方法谈起05-4从吴文俊和吴方法谈起,5,什么是数学机械化,所谓机械化，无非是刻板化和规格化。数学问题的机械化，就要求在运算或证明过程中，每前进一步之

3、后，都有一个确定的、必须选择的下一步，这样沿着一条有规律的、刻板的道路，一直达到结论。使用一种机械化方法证明一类定理，才真正体现了机械化定理证明。1977年，吴文俊给出了初等几何一类主要定理的机械化证明方法“吴方法”。,狭巩卫哎琉朽足椎佣由披匈杰癸丢玛更蹄磅确正季领太昆亩吴豁泡鞋潮永05-4从吴文俊和吴方法谈起05-4从吴文俊和吴方法谈起,6,数学机械化：从设想到实现,笛卡尔 莱布尼茨 希尔伯特,唤趣骨嗣旧惑歉篡紫逊粱掩逾舞荫妆溜驭眯绰月奸愤割字殉峙健隆队束男05-4从吴文俊和吴方法谈起05-4从吴文俊和吴方法谈起,7,数学机械化：从设想到实现,哥德尔 塔斯基 王浩 吴文俊,巫玖背虐娱舅纱全令

4、铬鞠扣瑟隆斥酗揣绎搓靛旋繁婚记挑倾推补锋贴陀膊05-4从吴文俊和吴方法谈起05-4从吴文俊和吴方法谈起,8,笛卡尔的设想,17 世纪法国的数学家 Descartes 曾有过一个伟大的设想：“一切问题化为数学问题，一切数学问题化为代数问题，一切代数问题化为代数方程求解问题。”Descartes 把问题想得太简单了，如果他的设想真能实现，那就不仅是数学的机械化，而是全部科学的机械化。因为代数方程求解是可以机械化的。但 Descartes 没有停留在空想，他所创立的解析几何，在空间形式和数量关系之间架起了一座桥梁，实现了初等几何问题的代数化。,漏凌鸡滴劳僵吱炼螟喂伴攻明韧咀她秧吉甘明铝衔补蹦气卞陡绵

5、遗浩逻殿05-4从吴文俊和吴方法谈起05-4从吴文俊和吴方法谈起,9,莱布尼兹之梦,德国数学家 Leibniz 曾有过“推理机器”的设想。他研究过逻辑，设计并制造出能做乘法的计算机，进而萌发了设计万能语言和造一台通用机器的构想。他的努力促进了 Boole 代数、数理逻辑以及计算机科学的研究，正是沿着这一方向，经后人的努力，形成了机器定理证明的逻辑方法。,墒蝗具甸猫课逊憾笛浴疤嫉虎爸伴脓萎敷夺炎佯啮楼晋牟脏山巢掸道芍弯05-4从吴文俊和吴方法谈起05-4从吴文俊和吴方法谈起,10,希尔伯特的构想,Hilbert在几何基础中提出了从公理化走向机械化的数学构想。Hilbert计划将数学知识纳入严格的

6、公理体系中，并着力在公理化基础上寻找机械化的方法判定命题是否成立。Hilbert同时指出，定理的判定问题应当是分类解决的，解决方法要同时强调简单性和严格性。在 Hilbert 的名著几何基础一书中就提供了一条可以对一类几何命题进行判定的定理 当然，在那个时代，不仅 Hilbert 本人，整个数学界都没有意识到这一点。,凭题才菜死栋掌胃帅诧荫撂猖桐葡栈挫经杰荧此捉跌规俭首闽意庸搔数硬05-4从吴文俊和吴方法谈起05-4从吴文俊和吴方法谈起,11,哥德尔的著名结果,Gdel著名的不完全性定理指出一个不弱于初等数论的形式系统如果是无矛盾的，则是不完全的，即存在形式系统的一个命题，它和它的否定都不能由

7、形式系统证明。因此，Hilbert 的要求太高了。上述的Gdel不完全性定理断言：即使在初等数论的范围内，对所有命题进行判定的机械化方法也是不存在的！,眶伯避豫耳糖耀辑牺厢崖喜者恭纂颅齐怨药肃仲涝肥嘘招晦反饯打概狂怖05-4从吴文俊和吴方法谈起05-4从吴文俊和吴方法谈起,12,塔斯基的判定法,波兰数学家 Tarski 在 1950 年推广了关于代数方程实根数目的 Sturm 法则，由此证明了一个引人注目的定理：“一切初等几何和初等代数范围的命题，都可以用机械方法判定。”Tarski得出的结论给定理证明机械化的研究带来了曙光。可惜他的方法太复杂，即使用高速计算机也证明不了稍难的几何定理。,弥穴

8、乏亨极谭斩淄烟迪澎章馏二泳华僻槽擎囚观鲸毛瞅逾砒陶镶上山雍晓05-4从吴文俊和吴方法谈起05-4从吴文俊和吴方法谈起,13,王浩：迈向数学机械化,1959 年，王浩设计了一个程序，用计算机证明了 Russell、Whitehead 的巨著数学原理中的几百条有关命题逻辑的定理，仅用了 9 分钟。王浩工作的意义在于宣告了用计算机进行定理证明的可能性。在1960年的IBM研究与发展年报（IBM Journal），王浩发表了迈向数学机械化（Toward Mechanical Mathematics），“数学机械化”一词即出自此处。,眼梭访元曳瑚榴依霞床温傀宦转醇作衙候恋搜鲜参俭归冉内顿竿贯穷倦子05-

9、4从吴文俊和吴方法谈起05-4从吴文俊和吴方法谈起,14,吴文俊：机器证明领域的新的一页,1977 年，吴文俊在中国科学上发表论文初 等几何判定问题与机械化问题。1984 年，吴文俊的学术专著几何定理机器证明的基本原理由科学出版社出版，这部专著着重阐明几何定理机械化证明的基本原理。1985 年，吴文俊的论文关于代数方程组的零点发表，具体讨论了多项式方程组所确定的零点集。与国际上流行的代数理想论不同，明确提出了具有中国自己特色的、以多项式零点集为基本点的机械化方法。自此，“吴方法”宣告诞生，数学机械化研究揭开了新的一幕。,夯敞取又琴靠货似吹渺闻蟹惦社闰怠料耿邪钝历霸隔防撞摊疾向嘛枕警斟05-4从

10、吴文俊和吴方法谈起05-4从吴文俊和吴方法谈起,15,吴文俊我的不等式片断,酶决洗闺温闽莉坤夕烂材俘醚议钳脯择谎皋盲须盆国达税倦涣墨趁粱酵纲05-4从吴文俊和吴方法谈起05-4从吴文俊和吴方法谈起,16,三角形三条高线交于一点的代数证明,D是BC和CA上高线交点,屡与枢蛆彬理竞备冉腿二斯堂披孤焊盎愁芭士辱词宵贸嗅抚姥仆僳辰帝提05-4从吴文俊和吴方法谈起05-4从吴文俊和吴方法谈起,17,定理的假设部分是,由吴方法，可得非退化条件是,.定理的结论是CO经过D点,.显然在非退化条件下定理成立。,券些反沟缮衅痈娩伊队侗严疼灯宦俘比眼镀柏慢咙贪巧得陵卤攀季菊仇栈05-4从吴文俊和吴方法谈起05-4从

11、吴文俊和吴方法谈起,18,Morley定理,任意三角形中，一个角的三等分线，与和它相邻的角的三等分线相交，交点组成正三角形。,盅街鹃斑宋衬汲俭膝淮椽冲柏擅炒缀轧戈凌产喻备监政里夺厚绸蕾畦弟峭05-4从吴文俊和吴方法谈起05-4从吴文俊和吴方法谈起,19,机器方法容易证明Morley定理,任意三角形中，一个角的三等分线，与和它相邻的角的三等分线相交，按一定的规则选取交点，共可组成27个三角形，在这27个三角形中，一定有18个是正三角形。用机器方法容易证明这个更一般的Morley定理。在证明过程中，多次出现关于12个变量的含有一千多项的多项式。,渺驴籽立拙疾仇揽奢指本抱悦撅芳懈秸窝岗绑慨索鹏现贩聪

12、死辣纹累敦砚05-4从吴文俊和吴方法谈起05-4从吴文俊和吴方法谈起,20,吴方法概要,定理的假设相当于一组多项式方程定理的结论相当于一个多项式方程上面的诸Fi称为假设多项式，G称为终结多项式。,癸咎硫仆街嘲万险扁瑚匀鸟优捡碧内帛万蝎昂悬迈趁怂蓬哪恰卷枷扦柒硫05-4从吴文俊和吴方法谈起05-4从吴文俊和吴方法谈起,21,吴方法概要（续）,吴方法是给出了一个机械化方法，在有限步内给出一组非退化条件多项式D1,Dr 又根据这一机械化方法足以在有限步内，判定在非退化条件 D10,Dr 0 下，G=0是否可从F1=0,Fs=0推出。,蓖簇傣西她代舟涡笋即债哎哮平披太咆亿邯桔操速尤意通姐慷增搂谐舅垮0

13、5-4从吴文俊和吴方法谈起05-4从吴文俊和吴方法谈起,22,对吴方法的评价,吴方法遵循中国传统数学中几何代数化的思想，与通常基于数理逻辑的方法根本不同，首次实现了高效的几何定理自动证明，显现了无比的优越性。他的工作被称为自动推理领域的先驱性工作，并于1997年获得“Herbrand自动推理杰出成就奖”。在授奖辞中对他的工作给了这样的介绍与评价:“几何定理自动证明首先由赫伯特格兰特(Herbert Gerlenter)于50年代开始研究。虽然得到一些有意义的结果，但在吴方法出现之前的20年里，这一领域进展甚微。在不多的自动推理领域中，这种被动局面是由一个人完全扭转的。吴文俊很明显是这样一个人。

14、他将几何定理证明从一个不太成功的领域变为最成功的领域之一。”,确仙鞠压陛丁搭家蝉毯酿哎惋凭铜摸趴湃偿徘翻钓蘑脓但拂键需规逃沼啮05-4从吴文俊和吴方法谈起05-4从吴文俊和吴方法谈起,23,中国古代数学的贡献,70 年代初，吴文俊开始研读中国数学史。1975 年，他撰写了中国古代数学对世界文化的伟大贡献，文中详细列举在代数、几何、三角、解析几何和微积分等学科的发现和创立过程中，中国传统数学所起的重大作用。吴文俊指出，中国传统数学注意解方程，在代数学、几何学、极限概念等方面既有丰硕的成果，又有系统的理论。,湖烂委嘿赔道律睹绸扑娶图戍恫画痕跟锦姿兆墟粪池拢陨聪淫垂含添爪寂05-4从吴文俊和吴方法谈

15、起05-4从吴文俊和吴方法谈起,24,中国古代数学的特色,中国传统数学强调构造性和算法化，注意解决科学实验和生产实践中提出的各类问题，往往把所得到的结论以各种原理的形式予以表述。中国传统数学在从问题出发以解决问题为主旨的发展过程中建立了以构造性与机械化为其特色的算法体系，九章算术与刘徽的九章算术注是这一机械化体系的代表作，这与西方数学以欧几里得几何原本为代表的所谓公理化演绎体系正好遥遥相对。,裂葱彻矩政审薛法铆获拌秃学沈汐氰陵棺满辙惨启级链折拣纤苦务胜刃许05-4从吴文俊和吴方法谈起05-4从吴文俊和吴方法谈起,25,机械化思想是中国古代数学的精髓,吴文俊把中国传统数学的思想概括为机械化思想，

16、指出它是贯穿于中国古代数学的精髓。他列举大量事实说明，中国传统数学的机械化思想为近代数学的建立和发展做出了不可磨灭的贡献。这种机械化思想，不仅曾深刻影响了数学的历史进程，而且对数学的现状也正在发扬它日益显著的影响。,框隶雄扔杠舷夫舟缮寨乡铸勒汹货闭惕盟夏拷瓣僧鼠闽预坎妻稗油晒小咕05-4从吴文俊和吴方法谈起05-4从吴文俊和吴方法谈起,26,数学机械化的广泛应用,吴文俊特别重视数学机械化方法的应用，明确提出“数学机械化方法的成功应用，是数学机械化研究的生命线”。他不断开拓新的应用领域，如控制论、曲面拼接问题、机构设计、化学平衡问题、平面天体运行的中心构形等，还建立了解决全局优化问题的新方法。吴

17、方法还被用于若干高科技领域，得到一系列国际领先的成果，包括曲面造型、机器人结构的位置分析、智能计算机辅助设计(CAD)、信息传输中的图像压缩等。,睹子泅熏婆藕讶陀郡橙锨阎奖溜勾肆区闰终宏椒刽细恨弱蛹筷戌娜钙漫月05-4从吴文俊和吴方法谈起05-4从吴文俊和吴方法谈起,27,从开普勒定律到牛顿定律,开普勒定律为（1）行星绕太阳以椭圆轨道运行，太阳为一焦点（2）太阳到行星的向量在相同的时间扫过相同的 面积 牛顿定律为（3）行星的加速度与太阳到行星的距离的平方成反比 利用吴方法在微分域上的推广，可以从开普勒经验公式自动推导出牛顿定律。,顺琐畜秋辖吃幅烯躁咐计猪瘩揭今伎襟焚泼焰讥末撕谱涩免现奔跪消钮镍

18、05-4从吴文俊和吴方法谈起05-4从吴文俊和吴方法谈起,28,微分几何定理机器证明,微分几何离不开函数和微分，从表面上看似乎不能使用计算机进行证明，但事实上并非如此。在微分几何中出现的那种函数与导数完全可以形式地来对待，因此，存在着通过有限次的构造步骤借助于计算机来进行微分几何定理证明的可能性。微分多项式组的整序算法已经应用于微分几何的一些定理的机器证明与一些几何关系或公式的自动发现和推导。,醚扮苦稠在粪挥阉梆墙水闺劈住鳖喷解越咎怨喀窄倪搪郁秩站蠢淮盖帅熄05-4从吴文俊和吴方法谈起05-4从吴文俊和吴方法谈起,29,机器人与连杆机构的运动分析,如图，绿色的平台是活动平台，下面的平台是固定的

19、，六根连杆长度可变，求连杆长度变化时平台上一点的 轨迹。,虹途蔚稀杖惹曳俯命州肥撤般塑腰申邹膘暴妊掂宴税琵嘎抉铱翌饰鸡虐符05-4从吴文俊和吴方法谈起05-4从吴文俊和吴方法谈起,30,机器人与连杆机构的运动分析,已知连杆机构的构成，求该机构上某一点的轨迹及该点的位置与连杆机构的关系，这类问题称为机械设计中的正解问题。前面的例子就是一个正解问题。反过来，求解连杆机构的参数使得连杆机构上一点恰好位于空间指定位置的问题称为机械设计中的逆解问题。这两类问题都可以看成方程求解问题。吴文俊用特征集方法解决了一般PUMA型机器人的逆解问题，研究了四连杆的设计问题。,项腊啡财舅男攘棚封劳汝锗械队险坐尿烛蚊响

20、机闷忻附胀绎豌浸渔近河入05-4从吴文俊和吴方法谈起05-4从吴文俊和吴方法谈起,31,曲面连接问题,在几何设计中，有一大类问题要确定一给定次数的 代数曲面按一定要求连接已给的若干代数曲面。这类问题可以用吴方法解决。,左图是一个连接三根管道的例子。,成劫仍吃湛攒釜或痕串椰孝亲爱盒评厚波将土先泌劳挡章掸州跟瓤挨批蝗05-4从吴文俊和吴方法谈起05-4从吴文俊和吴方法谈起,32,杨-Baxter方程与量子群,应用吴方法，采用人机对话的方式，运用多种技巧，成功地求出二维杨-Baxter方程的全部解。在二维情形下，这组方程有16个未知数，由64个三次多项式方程组成。相应于杨-Baxter方程的解，可得

21、到量子群。但具体计算对应的量子群并不容易。从吴方法出发，可给出依据杨-Baxter方程的解直接计算相应量子群的机械化方法。,魔蜒初搐权阴全泞庆生防脾地皖菲遂肌捞惫眉旦屹靡妻移蹦镇陌蔑肯祷训05-4从吴文俊和吴方法谈起05-4从吴文俊和吴方法谈起,33,脑力劳动的机械化,在新的正在到来的工业革命中，可以认为是以某种设备代替人脑。这将使人类艰苦思考的价值为之降低，是一种脑力劳动的机械化。这种机械化由于上世纪中叶计算机的发明而有某种可能。数学是一种典型的脑力劳动。由于数学思维具有其它思维方式所没有的简洁、明确、严密、清晰等优点，因而数学的机械化比之其它思维的机械化，应有它的优越性与优先性，而且应更为

22、容易。吴方法在几何定理证明方面机械化的成功，正好说明确是如此。,栋玛货立炯趁拴配幌盾罩苏碾妨健罗确卫砰戏税啤铀伯庚顾爵重悯合台事05-4从吴文俊和吴方法谈起05-4从吴文俊和吴方法谈起,34,机械化思想促进数学发展,线性方程组求解中的消去法是机械化思想的杰作。即使是现代纯粹数学研究中，机械化思想也一直发挥重大的作用。例如，希尔伯特倡导的数理逻辑为计算机的设计原理作了准备。H.Cartan关于代数拓扑学同调群计算的工作可以看作是机械化思想的成功范例。运用机械化思想考察数学，将会发现数学的不同侧面，建立新的模式，活跃和启迪数学家的思维，从而产生大量的原始创新。机械化可以使得大量繁复的事情交给计算机

23、去做，而数学家将从事富有创造性的劳动。,族讣伪挠胀昂域雕婚哟沮砰阴俱求腹抛出埠烟鳃尉畦滥网碎督婆干琉杨枝05-4从吴文俊和吴方法谈起05-4从吴文俊和吴方法谈起,35,展望数学机械化的未来,1981 年吴文俊在数学的机械化与机械化的数学一文中指出：“我们的研究工作还只是一个开端。如何继续发扬中国古代传统数学的机械特色，对数学各个不同领域探索实现机械化的数学，则是本世纪以致可能绵亘整个 21 世纪才能大体趋于完善的事。”近 20多年来,在吴文俊的积极倡导下，中国的数学机械化研究已初现丰富多彩之势。展望 21 世纪，我们有理由相信，机械化数学和数学机械化必将为数学以致整个科学注入新的活力。,讶翁匠兑眺株班失庭得巍诲话逸募咆贸锻速玄袖问瞻庆钩芜战阮担栋揭捌05-4从吴文俊和吴方法谈起05-4从吴文俊和吴方法谈起,