各位网友们好，相信很多人对数学机械化的进展都不是特别的了解，因此呢，今天就来为大家分享下关于数学机械化的进展以及面向机器智能的数学机械化新方法的问题知识，还望可以帮助大家，解决大家的一些困惑，下面一起来看看吧！
本文目录一览
1、机器证明的发展现状
2、中国科学院系统科学研究所的数学机械化重点实验室
机器证明的发展现状
近20年来，几何定理机器证明的研究和实践有了很大的进展。从古 的梦想到惊人的突破 能否建立一个 的几何解题方法，成批地解决问题，以至万理一证，是历史上一些卓越科学家的梦想。为此，笛卡尔发明了坐标系；莱布尼兹设想过推理机器；希尔伯特在其名著（几何基础）中给出了一类几何命题的机械化定理。 计算机的出现推动了数学机械化。50年代，塔斯基用代数方法证明了初等几何的机械化的可能性。到60年代，斯拉格和莫色斯实现了符号积分，代数与分析计算问题的机械化已经初具规模，而几何定理的机器证明看来仍遥遥无期。接着， 等提出用逻辑方法建立几何推理机， 斯等改进了塔斯基的代数方法。直到1975年，仍找不到能用计算机判定非平凡几何命题的有效算法。正当这一领域的热情由于进展缓慢而趋于冷落之际，吴文俊方法的提出给定理机器证明的研究带来勃勃生机。用吴法可在微机上很快地证明困难的几何定理。周咸青发展了吴法并把它实现为有效的 程序，证明了512条非平凡定理，写成英文专著。这一进展是自动推理领域的一大突破，被国际同行誉为革命性的工作。从机器判定到可读证明的自动生成 吴法的成功使 冷落的几何定理机器证明研究活跃起来。用代数方法证明几何定理的方向受到重视。 代数方法接连出现。在国外，周咸青等提出了用Grobner基方法构作几何定理机器证明的算法和程序并获得成功。在国内，洪家威提出了单点例证方法的理论设想，但因复杂度太大不能实现。张景中、杨路则提出数值并行方法，在低档微机（甚至计算器）上实现了非平凡几何定理的机器证明和机器发明。数值并行方法的 是所需内存极小，且易于并行化。所有这些方法都属于代数方法。它们的提出和实现丰富了几何定理机器证明的研究。但与吴法相比，没有大的新突破。代数方法不能使人满意的是，它所给出的证明是关于大多项式的繁复的计算，人难于理解其几何意义,也难于检验其是否正确。能否让计算机生成人能理解和易于检验的简明巧妙的证明，即所谓可读证明，是对自动推理和人工智能领域的一个挑战性的课题。一些著名的科学家认为，机器证明的基本思想是以量的复杂取代质的困难，这就很难想象用机器生成可读证明。国外一些学者从60年代即致力于几何定理可读证明自动生成的研究，30多年来进展不大，未能给出哪怕是一小类非平凡几何定理的机器证明的有效算法和程序。作者以多年来所发展的几何新方法为基本工具，并提出了消点思想，和周咸青、高小山合作，于1992年突破了这一困难，实现了几何定理可读证明的自动生成。这一新方法既不以坐标为基础，也不同于传统的综合方法，而是一个以几何不变量为工具，把几何、代数、逻辑和人工智能方法结合起来所形成的开放系统。它选择几个基本的几何不变量 套作图规则，并且建立一系列与这些不变量和作图规则有关的消点公式。当命题的前提以作图语句的形式输入时，程序可调用 当的消点公式把结论中的约束点逐个消去，最后达到水落石出。消点的过程纪录与消点公式相结合，就是一个具有几何意义的证明。此算法对可构造等式型几何命题是完全的，但其应用范围不限于这一类命题。基于此法所编的程序，已在微机上对数以百计的困难的几何定理完全自动地生成了简短的可读证明，其效率也比其他方法为高。随所用的几何量的不同，它能生成面积法、向量法、复数法和全角法等多种风格的证明，也能用于立体几何。杨路、高小山、周咸青与作者合作，把消点法用于非欧几何可读证明的自动生成也获得成功，并得到一批非欧几何新定理。消点法也可用于几何计算和公式推导。基于几何量和消点思想的新原理的建立，像是打开了几何定理机器求解的一个矿床。它也使几何定理机器证明的成果在数学教育中的应用有了现实可能。这一成果被国际同行誉为使计算机能像处理算术那样处理几何的发展道路上的里程碑，是自动推理领域30年来最重要的工作。在多数情形下，消点法也可用笔纸证明不平凡的定理。它结束了两千年来几何证题无定法的局面，把初等几何解题法从四则杂题的层次推进到代数方程的阶段。机器证明与人工证明媲 新阶段 但是，比起人类在几千年间积累起来的丰富多彩的几何知识来，计算机目前所能做的仍是十分有限。应当把几何学家所 的方法更多地教给计算机，使计算机产生的解法可以与几何学家相比。为此,要分析几何学家有哪些解题方法，计算机已经学会了哪些，以确定下一步应当做什么和如何做。几何学家常用下列四种手段： W1.检验：对具体图形作观察和计算，以确信命题为真。W2.搜索：依据常用的引理和已知条件去找寻题图中更多的几何性质。这样做如达不到目的，得到的信息就是进一步工作的基础。W3.归约：从结论出发，利用已知信息消去依赖的几何量或几何元素，使结论的真假趋于显然或易于检验。W4.转化：改变命题的形式，如几何变换、反证法、辅助线等。手段W1的机器模拟已经实现。手段W3的机械化研究得到了最大的成功。吴法、GB法、面积法和向量法均属此类。手段W4充分体现了人的思维活动的灵活性与丰富性，尚难以机械化。手段W2，搜索，是传统几何证明活动中的常规方法，是归约的补充和转化的基础。我们基于前推模式设计并实现了一个几何信息搜索系统(GISS）。由于 当选择几何工具，合理组织数据和优化推理的过程，效果极好。文献中曾提出的用搜索法处理涉及圆的命题，以及找出所有可能推出的几何性质（达到推理不动点）的问题，均被我们的算法完满回答。我们的程序用C语言在NeXT工作站上实现，用于161个非平凡几何命题，均在合理的时间内达到不动点，并能发现新定理，证得其它方法不能证明的结果。程序已具有添加某些辅助线的功能。非线性代数方程组的研究 机器生成可读证明的实现并不使代数方法失去价值。一些特殊问题及代数曲线、曲面的几何问题仍需用代数方法求解。代数方法与非线性代数方程组的理论和符号求解密切相关，有广泛应用，是自动推理的一大热点。数学、物理和工程技术中的许多问题，归根结底要靠解代数方程组。线性方程组还好办，非线性方程组就成了难关。特别是非线性方程组的符号求解，更难，理论上也更重要。对非线性代数方程组的研究，19世纪就提出了各种结式方法。由于结式法涉及 列式的计算，算不动，研究就冷下来。本世纪有了计算机，人们又研究 算法。在60年代，国外提出GB法和Ritt法。GB方法是完全方法。Ritt方法经吴文俊先生改进后，也成了一种完全方法。叫Ritt-Wu方法,在中国简称吴法（把Ritt-Wu方法用于几何定理的机器证明，也叫吴法。国外 把机器证明的吴法叫Ritt-Wu方法，是不确切的。Ritt和几何定理机器证明没有关系。）。两个方法哪个更好，目前还没有定论。用于几何定理机器证明，吴法确实比GB法强。中国学者还用吴法解决了许多重要问题，涉及理论物理、微分方程、样条理论和 。虽已有了吴法、GB法等优秀的完全方法，但是道高一尺，魔高一丈，更难的问题要求更有力的新方法。近年来，国外一再提出 思路和算法，欧共体还投资数百万美元组织项目专门研究非线性代数方程组的解法，但均无突破性进展。最近，基于我们提出并加以完善的 理论和算法———结式矩阵法，符红光编写了代数方程组符号求解和机器证明的MAPLE程序。新算法的特点是： ⑴是非线性代数方程组符号求解和相容性判定的完全方法。⑵不依赖于多项式的因式分解。⑶用我们提出的弱非退化条件作零点分解，减少多余分支。⑷子结式计算与数值检验配合，进行大范围消元。⑸将所给方程组分解为三角列，便于机器证明和最终求解。经许多例子的演算，它比已知的各种方法有更好的效果。此法能在PC486机上解六变量循环方程，反解各种类型的六关节 问题，这是其它方法做不到的。非线性代数方程组研究的又一新进展是杨路等提出的实系数代数方程的判别式系统。这不但彻底解决了几世纪悬而未决的关于代数方程一个基本问题，也使几何不等式机器证明的难题得到了突破。杨路等最近所写的程序，能快速地证明许多几何不等式，根据已给条件推出几何不等式，并已改正和改进了国外一些关于几何不等式的结果。展望与建议 预计在未来十年中初等几何等式型问题的机器求解将基本完成，并进入实用阶段。在前述成果的基础上，会出现 热点：⑴在几何定理可读证明自动生成工作的影响下，用几何不变量为工具进行机器求解的研究会有 进展。例如几何作图的机器求解，几何推理数据库的研究及微分几何可读证明的研究。⑵几何不等式的机器求解，会随着实代数研究的进展而出现 突破。⑶非线性代数方程组的理论与算法，仍将是热点。结式法和插值方法等利于并行的算 得到更多重视。⑷微分多项式的机器推导研究将得到开展。⑸机器证明的成果，特别是非线性代数方程组理论与算法的研究成果，将在数学、物理和工程技术中得到更多的应用。目前,在几何定理机器证明方面，中国处于国际领先地位。在非线性代数方程组研究领域，竞争激烈，中国已进入先进行列，但还不能说领先。在数学机械化软件开发方面，由于起步晚、队伍小和资金不足等原因，中国远不及欧美先进 。我们不应满足于某些方向上的领先地位。在继续进行几何定理机器证明研究并保持领先的同时，要把力量集中到非线性代数方程组的方向上来，特别应加强对实用而有效的算法的研究。在数学机械化推广应用方面，也应投入力量，发挥我们在理论与算法方向的优势，在软件开发方面赶超先进。在几何定理机器证 果的基础上，开发高智能的教育软件和自主版权的符号演算数学软件，为中国科技、教育事业作出贡献。（此文是作者在中国计算机学会第九次全国学术会议上所作的特约报告的详细摘要）
中国科学院系统科学研究所的数学机械化重点实验室
“数学机械化”是中国数学家吴文俊先生在七十年代末开始倡导的一个研究领域，是脑力劳动机械化在数学科学的学术实践。数学机械化思想继承了中国古代数学的传统，它的着眼点在数学，但又具有明显的交叉性。 所谓机械化是指刻板化与规格化。十七世纪以来，以蒸气机为代表的工业革命是以机器代替人的体力劳动，数学机械化则是用计算机部分代替人类的脑力劳动。今天 计算机的飞速发展使得数学的机械化正在逐步成为现实。在数学发展过程中，可以看到演绎倾向与算法倾向的此消彼长。两种倾向总是交替地处于主导地位。值得注意的是，探询新算法可以导致数学的重大发现，如解析几何与微积分；而且构造性数学往往具有很高的实用价值。数学机械化研究的深入开展，不仅会进一步丰富数学科学的传统内容，也将进一步丰富其交叉性学科的内容，从而在总体上促进数学科学的发展。数学机械化不仅是数学研究的实质性进展，也为很多 技问题的解决提供了有力的工具。实验室的方法已在许多 技领域获得了一批理论成果，具备了解决尖端技术产业中实际问题的条件。包括曲面造型， 位置分析，几何设计，计算机视觉，智能CAD，信息安全和数字图象的高速高保真传输。通过进一步努力，这些理论研究成果有望能够实实在在地解决若干项技术问题为促进中国技术产业的发展做出积极的贡献。数学机械化研究又有明显的交叉性。除 技领域外，数学机械化的方法还被成功地用于解决其他领域的很多问题：理论物理中的杨振宁－Baxter方程求解，天体力学中共心多体问题， 平衡中的方程求解，小波构造的优化，命题逻辑与一阶谓词逻辑中的定理证明，非线性发展方程的行波解的算法等等。在国际上，计算机与数学的交叉正在成为数学研究 增长点,出现了计算代数、计算群论、计算几何、计算数论等 学科。符号计算是研究在计算机上进行准确的数学演算和与之相关的数学理论的学科，是数学机械化的主要工具。近年来一批专业化的学术机构已在世界各地纷纷成立。符号计算软件Maple，Mathematica已经在数学与工程领域被广泛使用。80年代以来，解（微分）代数多项式方程组是国际符号计算界的热点，其主要方法是Groebner基方法。90年代欧共体跨国研究项目POSSO(POlynomialSystemSOlving)及作为POSSO的延续项目FRISCO关注的问题，与我们开展数学机械化研究课题有许多相同之处。所不同的是，我们所用的是我国数学家自己发展起来的一套方法和理论。自动推理是与数学机械化密切相关的学科。自动推理源于人工智能，主要研究推理的自动化与机械化。国外主要以逻辑为基础开展自动推理研究，而吴方法的基础是代数几何。国际上自动推理界在注意发展新方法的同时，积极开展应用研究，如程序正确性验证,自动程序生成等。