如何实现自动推理.pptxVIP

如何实现自动推理 --简明介绍数学机械化与吴方法;讲座; 吴文俊院士是中国科学院数学与系统科学研究院的研究员，我国著名的数学家。他于上世纪50年代对数学的主要领域—拓扑学做出了杰出贡献。70年代后期，吴文俊开创了崭新的数学机械化领域。他建立了用计算机证明几何定理的“吴方法”。实现了高效几何定理自动证明；吴方法应用于计算机图形学、机器人、机构设计、全局优化、化学平衡、天体运行……等领域。 ;/detail2.asp?project_id=122type_id=22;吴文俊的虚拟轴机床——数学机械化方法及其在并联机构中的应用 吴文俊院士开创了数学机械化研究领域。他所建立的“吴方法”， “吴消元法”及“吴有限核定理”已成为该领域的奠基性成果。运用 数学机械化方法，本项研究解决了广义Stewart平台正解问题，这是对机 器人运动学领域的一个主要贡献。以此为基础，研制成功我国第一 台大型虚拟轴机床样机与集成电路制造装备关键子系统。;二、脑力劳动能机械化吗？;劳动=体力劳动+脑力劳动;; 脑力劳动的彻底机械化是不可能，但部分机械化是完全可能，并且随着人类智慧的提高这个机械化程度越来越高。; ;三、数学机械化 与自动推理; 吴文俊：所谓机械化，无非是刻板化和规格化。 数学问题的机械化，就要求在运算或证明过程中，每前进一步之后，都有一个确定的、必须选择的下一步，这样沿着一条有规律的、刻板的道路，一直达到结论。;自动推理;实现机械化和自动推理需要两个发展： 构造性数学的发展（脑子）； 计算机的发展（肢体）。;四、数学机械化的艰难历程 ——从设想到实现;数学机械化：从设想到实现;数学机械化：从设想到实现;笛卡尔的设想;莱布尼兹之梦;希尔伯特的构想;哥德尔的著名结果;塔斯基的判定法;王浩：迈向数学机械化; 其他人 与王浩同一时期，A. Newell和 H. A. Simon也做了与王浩类似的工作。 1965年Robinson归结原理的提出是用逻辑方法进行机器证明的又一重要进展。 1976年K.I.Appel和W.Haken在高速电子计算机上用1200小时的计算时间，证明了??名的四色定理，使数学家们100多年来未能解决的这个难题得到了肯定的回答（机械化证明）。;数学大师们的坚持不懈地追求,表明数学机械化思想重要而深刻。 但数学机械化历程漫长而艰难，发展缓慢。 70年代末，在中国得到突破！ ; 五、数学机械化的突破 ——吴方法的出现;吴文俊： 数学机械化（机器证明）领域的新的一页 ;1977 年，吴文俊在《中国科学》上发表论文《初等几何判定问题与机械化问题》。 1984 年，吴文俊的学术专著《几何定理机器证明的基本原理》由科学出版社出版，这部专著着重阐明几何定理机械化证明的基本原理。 1985 年，吴文俊的论文《关于代数方程组的零点》发表，具体讨论了多项式方程组所确定的零点集。与国际上流行的代数理想论不同，明确提出了具有中国自己特色的、以多项式零点集为基本点的机械化方法。自此，“吴方法”宣告诞生，数学机械化研究揭开了新的一幕。 ; 六、吴方法的介绍; 所谓定理的机械化证明，就是对一类定理（这类定理可能成千上万）提供一种统一的方法，使得该类定理中每个定理，都可依此方法给出证明。在证明过程中，每前进一步，都有章可循地确定下一步该做什么和如何做。 从“一理一证”到“－类一证”，是数学的认识和实践的飞跃。;吴方法的基本思想是十分朴素的: 把几何命题化成代数形式加以处理。 化成什么形式? 如何处理? 整个过程是什么样? 主要思想是什么? ; ; 为了简便，可以将△ABC的外接圆中心O取为Descartes 坐标原点，将圆半径取为单位长，并设各点的坐标为 A(x1,y1)，B(x2,y2)， C(x3,y3)， R(x4,y4)，S(x5,y5)，T(x6,y6)，P(1,0) 于是，定理的假设部分可以改写成代数等式的形式。;条件（2）可以写成 ：;条件（3）可以写成 ：;至此,我们已经完成了用吴方法证明几何定理的第一步：用解析几何方法将几何问题代数化。当然，也可以用其他方法,如三角方法。 所得代数形式的问题就是，在假设一组多元多项式组为0的条件下，求证另一多项式为0。即，定理的等价代数表示为; 等价地, 用多项式的零点集（集合论）描述上述定理：需要证明;;对现在的问题，如果能实现;第二步 整序;;;的推导;;;吴方法的第二步至此完成。我们得到了一个三角化组(升列)：;现将;从这