数学机械化自动推理计算机代数-上海海事大学课件.ppt

1、讲座2008-11-？讲座一、吴文俊简介 8787岁岁不能创新不能创新 http:/ 吴文俊院士开创了数学机械化研究领域。他所建立的“吴方法”，“吴消元法”及“吴有限核定理”已成为该领域的奠基性成果。运用数学机械化方法，本项研究解决了广义Stewart平台正解问题，这是对机器人运动学领域的一个主要贡献。以此为基础，研制成功我国第一台大型虚拟轴机床样机与集成电路制造装备关键子系统。二、脑力劳动能机械化吗？劳动=体力劳动+脑力劳动;?!脑力劳动的机械化是人类的追求,梦想 对脑力劳动的机械化，作为其灵魂或核心技术对脑力劳动的机械化，作为其灵魂或核心技术,数学的参与是不可缺少。数学的参与是不可缺少。三

2、、数学机械化 与自动推理 吴文俊：所谓机械化，无非是刻板化和吴文俊：所谓机械化，无非是刻板化和规格化。规格化。数学问题的机械化，就要求在运算或证明数学问题的机械化，就要求在运算或证明过程中，每前进一步之后，都有一个确定过程中，每前进一步之后，都有一个确定的、必须选择的下一步，这样沿着一条有的、必须选择的下一步，这样沿着一条有规律的、刻板的道路，一直达到结论。规律的、刻板的道路，一直达到结论。数学机械化数学机械化自动推理自动推理w机械化算法的计算机实现。w对某一个思维问题(脑力劳动)要设计机械化算法;算法是构造化的,能转化为计算机指令;计算机能接受并能按设计逻辑处理这些指令,推理出结论.这里要知

3、道两个关键点:w计算机能处理什么?w算法是构造性(机械化)?实现机械化和自动推理实现机械化和自动推理四、数学机械化的艰难历程 从设想到实现从设想到实现数学机械化：从设想到实现数学机械化：从设想到实现笛卡尔笛卡尔莱布尼茨莱布尼茨希尔伯特希尔伯特数学机械化：从设想到实现数学机械化：从设想到实现哥德尔哥德尔塔斯基塔斯基王浩王浩吴文俊吴文俊笛卡尔的设想笛卡尔的设想 17 世纪法国的数学家世纪法国的数学家 Descartes 曾有过一个伟大的设想：曾有过一个伟大的设想：“一切问题化为数学问题，一切数学问题化为代数问题，一一切问题化为数学问题，一切数学问题化为代数问题，一切代数问题化为代数方程求解问题。切

4、代数问题化为代数方程求解问题。”并并，Descartes 没有停留在空想，他所创立的解析几何，在没有停留在空想，他所创立的解析几何，在空间形式和数量关系之间架起了一座桥梁，空间形式和数量关系之间架起了一座桥梁，实现了初等几何实现了初等几何问题的代数化问题的代数化。但，但，Descartes 把问题想得太简单了，如果他的设想真能实把问题想得太简单了，如果他的设想真能实现，那就不仅是数学的机械化，而是现，那就不仅是数学的机械化，而是全部科学的机械化。全部科学的机械化。莱布尼兹之梦莱布尼兹之梦德国德国数学家数学家 Leibniz 曾有过曾有过“推理机器推理机器”的设想。他的设想。他研究过逻辑，设计并

5、制造出能做乘法的计算机，进研究过逻辑，设计并制造出能做乘法的计算机，进而萌发了而萌发了设计万能语言和造一台通用机器的构想。设计万能语言和造一台通用机器的构想。他的努力促进了他的努力促进了 Boole 代数、数理逻辑以及计算机代数、数理逻辑以及计算机科学的研究，正是沿着这一方向，经后人的努力，科学的研究，正是沿着这一方向，经后人的努力，形成了机器定理证明的逻辑方法。形成了机器定理证明的逻辑方法。希尔伯特的构想希尔伯特的构想 Hilbert在在几何基础几何基础中提出了从公理化走向中提出了从公理化走向机械化的数学构想。机械化的数学构想。Hilbert计划将数学知识纳入严计划将数学知识纳入严格的公理体

6、系中，并着力在公理化基础上寻找机械格的公理体系中，并着力在公理化基础上寻找机械化的方法判定命题是否成立。化的方法判定命题是否成立。Hilbert同时指出，定同时指出，定理的判定问题应当是分类解决的，解决方法要同时理的判定问题应当是分类解决的，解决方法要同时强调简单性和严格性。强调简单性和严格性。在在 Hilbert 的名著的名著几何基础几何基础一书中就提供了一书中就提供了一条可以对一类几何命题进行机械化判定的定理一条可以对一类几何命题进行机械化判定的定理 当然，在那个时代，不仅当然，在那个时代，不仅 Hilbert 本人，整个数学本人，整个数学界都没有意识到这一点。界都没有意识到这一点。哥德尔

7、的著名结果哥德尔的著名结果 Gdel著名的不完全性定理指出一个不弱于初等数论的形式系统如果是无矛盾的，则是不完全的，即存在形式系统的一个命题，它和它的否定都不能由形式系统证明。因此，Hilbert 的要求太高了。上述的Gdel不完全性定理断言：即使在初等数论的范围内，对所有命题进行判定的机械化方法也是不存在的！塔斯基的判定法塔斯基的判定法 波兰数学家波兰数学家 Tarski 在在 1950 年推广了关于代年推广了关于代数方程实根数目的数方程实根数目的 Sturm 法则，由此证明了法则，由此证明了一个引人注目的定理：一个引人注目的定理：“一切初等几何和初一切初等几何和初等代数范围的命题，都可以用

8、机械方法判等代数范围的命题，都可以用机械方法判定定。”Tarski得出的结论给定理证明机械化的研究得出的结论给定理证明机械化的研究带来了曙光。可惜他的方法太复杂，即使用带来了曙光。可惜他的方法太复杂，即使用高速计算机也证明不了稍难的几何定理。高速计算机也证明不了稍难的几何定理。王浩：迈向数学机械化王浩：迈向数学机械化 1959 年，王浩设计了一个程序，用计算机证年，王浩设计了一个程序，用计算机证明了明了 Russell、Whitehead 的巨著的巨著数学数学原理原理中的几百条有关命题逻辑的定理，仅中的几百条有关命题逻辑的定理，仅用了用了 9 分钟。分钟。王浩工作的意义在于宣告了用王浩工作的意

9、义在于宣告了用计算机进行定理证明的可能性计算机进行定理证明的可能性。在在1960年的年的IBM研究与发展年报研究与发展年报（IBM Journal）上，王浩发表了）上，王浩发表了迈向数学机械化迈向数学机械化（Toward Mechanical Mathematics）的文）的文章。章。“数学机械化数学机械化”一词即出自此处。一词即出自此处。五、数学机械化的突破 吴方法的出现吴方法的出现吴文俊：吴文俊：数学机械化（机器证明）领域的新的一页 1977 年，吴文俊在年，吴文俊在中国科学中国科学上发表论文上发表论文初初等几何判定问题与机械化问题等几何判定问题与机械化问题。1984 年，吴文俊的学术专著

10、年，吴文俊的学术专著几何定理机器证明几何定理机器证明的基本原理的基本原理由科学出版社出版，这部专著着重阐由科学出版社出版，这部专著着重阐明几何定理机械化证明的基本原理。明几何定理机械化证明的基本原理。1985 年，吴文俊的论文年，吴文俊的论文关于代数方程组的零点关于代数方程组的零点发表，具体讨论了多项式方程组所确定的零点集。发表，具体讨论了多项式方程组所确定的零点集。与国际上流行的代数理想论不同，明确提出了具有与国际上流行的代数理想论不同，明确提出了具有中国自己特色的、以多项式零点集为基本点的机械中国自己特色的、以多项式零点集为基本点的机械化方法。自此，化方法。自此，“吴方法吴方法”宣告诞生，

11、数学机械化宣告诞生，数学机械化研究揭开了新的一幕。研究揭开了新的一幕。六、吴方法的介绍 数学数学(脑力劳动脑力劳动)机械化的典范机械化的典范Simson ABC Simson：O 0121211yxF(A在圆在圆O上上)；0122222yxF(B在圆在圆O上上)；0123233yxF(C在圆在圆O上上)；O定理：定理：(1)A,B,C,P在同一圆上在同一圆上;条件：条件：(2)R,S,T分别在直线分别在直线 BC,CA,AB上上;(3)PRBC,PTAB,PSAC 结论结论:R,S,T 共线。共线。;0)()(242324234xxyyyyxxF;0)()(151315135xxyyyyxxF

12、;0)()(262126216xxyyyyxxF(R在在BC上上)(S在在AC上上)(T在在AB上上)O 定理：定理：(1)A,B,C,P在同一圆上在同一圆上;条件：条件：(2)R,S,T分别在直线分别在直线 BC,CA,AB上上;(3)PRBC,PTAB,PSAC 结论结论:R,S,T 共线。共线。0)()(1(3243247yyyxxxF)(BCPR0)()(1(3251358yyyxxxF)(ACPS 0)()(1(2162169yyyxxxF)(ABPT 0)()(54656554yyxxyyxxG(R,S,T)O 定理：定理：(1)A,B,C,P在同一圆上在同一圆上;条件：条件：(2

13、)R,S,T分别在直线分别在直线 BC,CA,AB上上;(3)PRBC,PTAB,PSAC 结论结论:R,S,T 共线。共线。0)()(54656554yyxxyyxxG(R,S,T)(AO上)(BO上)(CO上)(RBC)(SAC)(TAB)(BCPR)(ACPS 0121211yxF0122222yxF0123233yxF0)()(242324234xxyyyyxxF0)()(151315135xxyyyyxxF0)()(262126216xxyyyyxxF0)()(1(3243247yyyxxxF0)()(1(3251358yyyxxxF0)()(1(2162169yyyxxxF)(AB

14、PT O0)(|)(xfKxfZeroO 定理：定理：(1)A,B,C,P在同一圆上在同一圆上;条件：条件：(2)R,S,T分别在直线分别在直线 BC,CA,AB上上;(3)PRBC,PTAB,PSAC 结论结论:R,S,T 共线。共线。)(),(921GZeroFFFZero),()()()(xrxgxqxf).,(),(rgZerogfZero.0)(,0)(.0)(,0)(xrxgxgxf)(xr)(xg),(),(xgxf,0)(xr).()()()()(xgxqxffZerogZero)(992211FAFAFAG)(),(921GZeroFFFZero 321,yyy321,yyy

15、6611,yxyx332211,yuyuyu44321yxxxx6655yxyx921,FFF9*2*1,FFF9*2*1,FFF921,FFFO;,;,;,;,;,;,;,;,;,321662193215531832144327321662163215531532144324321321332121232111uuuyxxxFuuuyxxxFuuuyxxxFuuuyxxxFuuuyxxxFuuuyxxxFuuuxxxFuuuxxFuuuxF无规律无规律(AO上)(BO上)(CO上)(RBC)(SAC)(TAB)(BCPR)(ACPS 0121211yxF0122222yxF0123233yx

16、F0)()(242324234xxyyyyxxF0)()(151315135xxyyyyxxF0)()(262126216xxyyyyxxF0)()(1(3243247yyyxxxF0)()(1(3251358yyyxxxF0)()(1(2162169yyyxxxF)(ABPT O已知已知0921FFF0921FFF;,;,;,;,;,;,;,;,;,321665554321932165554321832155543217321544321632144321532143214321321332121232111uuuyxyxyxxxxFuuuxyxyxxxxFuuuyxyxxxxFuuuxyx

17、xxxFuuuyxxxxFuuuxxxxFuuuxxxFuuuxxFuuuxF有规律有规律O*4F)()()()()()(323223242322327324324*xuuuxxxuuxxFxxFuuF利用 简化后得21,FF)()()1(2233232232432324xuxuuuxxxuuxxF3*32*21*1,FFFFFF(AO上)(BO上)(CO上)(RBC)(SAC)(TAB)(BCPR)(ACPS 0121211yxF0122222yxF0123233yxF0)()(242324234xxyyyyxxF0)()(151315135xxyyyyxxF0)()(262126216xx

18、yyyyxxF0)()(1(3243247yyyxxxF0)()(1(3251358yyyxxxF0)()(1(2162169yyyxxxF)(ABPT O用 消 ，令4y74FF 和).)(1()(),)()()1(2),)(1()(),)()()1(2),)(1()(),)()()1(2,1,1,1216621912212122162121813551373113132135313163244325233232232432324232333222222212111xxxyuuFxuxuuuxxxuuxxFxxxyuuFxuxuuuxxxuuxxFxxxyuuFxuxuuuxxxuuxxFu

19、xFFuxFFuxFF)/,(),(*9*2*1921IFFFZeroFFFZero)(),(921GZeroFFFZero)()/,(*92*1GZeroIFFFZero),(921FFFZero)/,(*9*2*1IFFFZero=921,FFF )()(56464554654yxyxyxyxyxxGG.8R)(1()(2166219xxxyuuF9F6y9F).)()(1)(),(Pr215646455421654698uuyxyxyxyxxxxxxyFGemR021uu 09F),)()(1(212166uuxxxyG。9F6y9F8R6x).)()()()(4554212154654

20、2154218yxyxuuxxxxxxxxxyyuuR 8F6x8R7R也看成也看成,8F),(Pr6887xFRemR),)()()1(2)()()()(4554212154212112212122154215421yxyxuuxxxxuuxxxuxuuuxxxxxxyyuu7R7F5y7F7R6R。;55*66RxFR的伪余式对关于求;44*55RyFR的伪余式对关于求;34*44RxFR的伪余式对关于求;23*33RxFR的伪余式对关于求;12*22RxFR的伪余式对关于求;01*33RxFR的伪余式对关于求0I).1)(1)(1)()()(323231312121313221uuxxu

21、uxxuuxxuuuuuuI0I)()/,(*92*1GZeroIFFFZero992211FAFAFAGI*92*1,FFF4x*3*2*1,FFF*4F)1(23232uuxx0)1(23232uuxx O 2O七，总结为什么能机械化？八、对吴方法的评价吴方法遵循中国传统数学中几何代数化的思想，与通吴方法遵循中国传统数学中几何代数化的思想，与通常基于数理逻辑的方法根本不同，常基于数理逻辑的方法根本不同，首次实现了高效首次实现了高效的几何定理自动证明的几何定理自动证明，显现了无比的优越性。他的，显现了无比的优越性。他的工作被称为自动推理领域的先驱性工作，并于工作被称为自动推理领域的先驱性工作

22、，并于19971997年获得年获得“HerbrandHerbrand自动推理杰出成就奖自动推理杰出成就奖”。在授奖。在授奖辞中对他的工作给了这样的介绍与评价辞中对他的工作给了这样的介绍与评价:“几何定理自动证明首先由赫伯特几何定理自动证明首先由赫伯特格兰特格兰特(H.(H.Gerlenter)Gerlenter)于于5050年代开始研究。虽然得到一些年代开始研究。虽然得到一些有意义的结果，但在吴方法出现之前的有意义的结果，但在吴方法出现之前的2020年里，年里，这一领域进展甚微。在不多的自动推理领域中，这一领域进展甚微。在不多的自动推理领域中，这种被动局面是由一个人完全扭转的。吴文俊很这种被动

23、局面是由一个人完全扭转的。吴文俊很明显是这样一个人。他将几何定理证明从一个不明显是这样一个人。他将几何定理证明从一个不太成功的领域变为最成功的领域之一。太成功的领域变为最成功的领域之一。”九、吴方法的广泛应用 控制论、曲面拼接问题、机构设计、化学平衡问题、平面天体运行的中心构形等，还建立了解决全局优化问题的新方法。吴方法还被用于若干高科技领域，得到一系列国际领先的成果，包括曲面造型、机器人结构的位置分析、智能计算机辅助设计(CAD)、信息传输中的图像压缩等。从开普勒定律到牛顿定律 开普勒定律为（1）行星绕太阳以椭圆轨道运行，太阳为一焦点（2）太阳到行星的向量在相同的时间扫过相同的 面积 牛顿定

24、律为（3）行星的加速度与太阳到行星的距离的平方成反比 利用吴方法在微分域上的推广，可以从开普勒经验公式自动推导出牛顿定律。微分几何定理机器证明 微分几何离不开函数和微分，从表面上看似乎不能使用计算机进行证明，但事实上并非如此。在微分几何中出现的那种函数与导数完全可以形式地来对待，因此，存在着通过有限次的构造步骤借助于计算机来进行微分几何定理证明的可能性。微分多项式组的整序算法已经应用于微分几何的一些定理的机器证明与一些几何关系或公式的自动发现和推导。机器人与连杆机构的运动分析 如图，绿色的平台是活动平台，下面的平台是固定的，六根连杆长度可变，求连杆长度变化时平台上一点的 轨迹。机器人与连杆机构

25、的运动分析 已知连杆机构的构成，求该机构上某一点的轨迹及该点的位置与连杆机构的关系，这类问题称为机械设计中的正解问题。前面的例子就是一个正解问题。反过来，求解连杆机构的参数使得连杆机构上一点恰好位于空间指定位置的问题称为机械设计中的逆解问题。这两类问题都可以看成方程求解问题。吴文俊用特征集方法解决了一般PUMA型机器人的逆解问题，研究了四连杆的设计问题。曲面连接问题 在几何设计中，有一大类问题要确定一给定次数的 代数曲面按一定要求连接已给的若干代数曲面。这类问题可以用吴方法解决。左图是一个连接左图是一个连接三根管道的例子。三根管道的例子。杨-Baxter方程与量子群 应用吴方法，采用人机对话的方式，运用多种技巧，成功地求出二维杨-Baxter方程的全部解。在二维情形下，这组方程有16个未知数，由64个三次多项式方程组成。相应于杨-Baxter方程的解，可得到量子群。但具体计算对应的量子群并不容易。从吴方法出发，可给出依据杨-Baxter方程的解直接计算相应量子群的机械化方法。结束语是思想是思想是方法是方法是技术是技术数学数学谢 谢