机械化方法

17机械化方法

整个数学发展历史过程中有两个中心思想:一是公理化思想;二是机械化思想。中学数学是这两种思想的混合物。平面几何是公理化思想的代表;代数则有丰富的机械化思想成分。如解线性联立方程组所用的各种消去法就是典型的机械化方法，解析几何则是几何与代数结合在一起，两种成分都有。

公理化的思想源出于古希腊，机械化思想则穿串于整个中国古代数学。《九章算术》是具有这一思想的代表作，线性联立方程组的解法及有关正负数概念与移项法则最早就见于此书。该书一直影响中国数学的发展。

一般说来，机械化就是一种程序化。数学的主要形式是数值计算和定理证明。中国古代数学突出一个“算”字，即数学问题的机械化，即按程序办，在运算和证明过程中，每前进一步后，都有有限多个确定的可供选择的下一步。这样，总能沿着一个程序达到目的。

在当今计算机广泛应用的情况下，数学机械化含义有两层:一是利用计算机从事数学研究;二是把数学的理论成果，通过计算机这一媒介，转变成工程技术和其他学科可以直接应用的结果。显然，数学中的计算问题容易做到机械化。一般说来有:

计算:易，繁，刻板，枯燥。

证明:难，简，灵活，美妙。

把巧而难的证明问题转变成虽繁却易的计算问题，是定理机器证明最为关键的一步。这一证明机械化的思想，早在17世纪的莱布尼兹就具有。中国古代数学通过筹算而引入相当于变元的概念并采用消元的方法，在宋元时期已出现。因此，如果真能做到将证明问题转变为计算问题，即做到寓理于算，问题即得到解决。几何定理证明关键是找到一条正确而有效的寓理于算的途径。有两条道路:一是逻辑方法;另一是代数方法。莱布尼兹的是逻辑的方法。笛卡儿(R．Descartes，1596—1650，法国数学家)从一开始就赋予了更多的使命。他设想一切问题都可以转变成数学问题;一切数学问题都可以转变成解方程的问题;一切解方程问题都可以转变成代数方程组的求解问题;最后又能转变为求解一个变元的代数方程问题。他创立的解析几何在空间形式和数量关系之间架起了一座划时代的桥梁。

1959年王浩设计了一个机械化方法，并用计算机证明了罗素的《数学原理》中的几百条定理，仅用了几分钟。这说明用计算机进行定理证明的可能性。他还提出了“走向数学的机械化”。这是逻辑的方法。

用代数学方法机械化的成功例子是1976年美国的哈肯等宣布，他们借助电子计算机，花了1 200小时，证明了100多年来未证明的世界难题——四色定理。这一成果轰动了科学界。这证明，存在一种算法，可以证明相当的一类数学定理。

与此同时，我国的吴文俊(1919年生，中国数学家)也从事定理机器证明的研究工作。他对中国古代数学很有研究。他采用代数方法，引进坐标，将几何定理的叙述用代数方程的形式重新表达，进而对代数方程组求解，提出了一套完整的符号解法。几何问题的代数化并无实质困难。但代数化过程，坐标点的选取和方程引进的次序都可能影响到以后的证明结果，即影响到证明的速度，甚至由于技术条件的限制影响到证明是否可能完成。吴文俊借用了有些学者的工作，将中国古代数学的思想融于自己的工作中，发展了一套数学机械化研究的代数方程组的求解方法。吴文俊方法是机械化证明的重大突破。

吴文俊方法主要有两部分:一是几何问题的代数化;二是代数方程的消元解法。

吴文俊用他自己设计的计算机程序，成功地完成了从开普勒定律推导牛顿定律的自动推导工作。此方法还可以用于机器人学和非线性规划的问题的计算方法，并且于1989年解决了一个取自化学平衡的困难的非线性规划问题。后来，他又成功地将其方法用于机器人学设计中逆运动方程求解问题，并给出了普导马型机器人的逆运动方程的解。

在几何定理证明方面，出现了例证法和数值并行法的工作。在吴方法用于数学研究中，出现了因式分解新方法，微分方程定性理论分析，多项式判别式系统和根的分离等工作。在其他应用方面，出现了线性控制系统的极点配置，斯图尔特平台问题，机器视觉和曲线与曲面表达形式的相互转化等工作。

吴文俊的开创性工作，使我国在这方面走在世界前列。