张景中机械证明 机器证明简史 张景中
1.艰难的历程 历史上一些大师级的数学家,曾在几何定理机器证明这条路上艰辛地探索过。 为了用统一的方法处理千变万化的几何问题,笛卡尔(Descartes)发明了坐标方法,创立了解析几何。
这是科学史上的一件大事。在解析几何的基础上,发展了用计算机解决几何问题的多种有力的方法。 莱布尼兹(Leibniz),微积分的发明人之一,曾有过推理机器的设想。
它还提出了现代计算机上所用的二进位记数法。它的这些工作促进了数理逻辑的早期研究。 跨19世纪、20世纪的大数学家希尔伯特(Hilbert),在它的名著《几何基础》中,曾给出了一类几何问题的机械化解题方法。
我国科学家用的面积消点的方法,对这类问题作了更简明、更易于理解的机械化处理。 电子计算机的出现,大大加快了数学机械化研究的进程,也促进了几何问题求解的机械化研究。
一个基本的理论问题是,千变万化的几何问题,是否能够纳入机械化处理的统一的轨道? 1948年,塔斯基(Tarski)发表了一条引人注目的定理:"一切初等几何和初等代数命题构成的命题类,是可判定的"。
什么叫初等几和初等代数命题?什么叫可判定?这需要解释。 命题是一个具有前提和结论的判断句。
如果命题的前提和结论都可以用有限个整系数多项式的等式或不等式来表达,它就叫做初等几何和初等代数命题。 如果有一套机械的方法,对于某个命题类的任一个命题,都能用这套方法经有限步的操作而确定命题的真假,就说这个命题类是可判定的。
塔斯基定理的证明是构造性的。也就是说,他确实提出了一套能判定任一个初等几何或初等代数命题的机械化方法。可是这方法的计算复杂度太大了。
即使用快速的计算机,也不能在合理的时间内(比如说几小时或几天)证明稍微难点的几何定理(如许多中学生就知道的几何事实,像西姆松定理)。 塔斯基的方法是:先利用笛卡尔坐标把几何问题化为代数问题,再用代数方法来解决问题。
沿这条路线,发展了几何问题机器证明的代数方法。 1975年,考林斯(Collins)提出"柱面代数分解方法",比塔斯基的方法效率提高了很多,但在计算机上仍只能解决个别的稍微难点的几何问题。
笛卡尔——塔斯基——考林斯,这是用代数方法寻求几何问题机械求解的一条线。
另一条路线,是企图把解决几何问题的传统综合方法机械化。这条路线是格兰特(Gelernter)在1959年发表的一篇论文中提出来的。格兰特实际上只用了丰富多彩的传统综合方法的技巧中的一种:从结论出发进行倒退推理的方法,通常叫做后推搜索法。
1975年,奈文斯又提出了更有效的前推搜索法。这类方法常被叫做逻辑方法,或叫做人工智能方法。其优点是能产生出传统风格的证明。
但由于搜索空间过大等问题,未能形成有效的算法。 在几何问题求解机械化研究举步维艰的20多年间,数学机械化的研究和应用在总体上有了长足的进展。计算机本来是只会计算数值的。到了20世纪60年代种,用它也能作符号计算了。
有理式的四则运算,多项式的因式分解,求最小公倍式和最大公因式,甚至还能计算符号微积分。强有力的数学软件开始在学校和科学技术工作人员中广泛应用。 数学机械化发展的有力的大环境,促进几何解题机械化出现突破。
2.重要的突破 这突破来自中国。 1977年,我国著名的数学家吴文俊院士在《中国科学》杂志上发表了题为"初等几何判定问题与机械化证明"的论文,提出了一个证明等式型初等几何定理的新的代数方法。这个方法虽然不能证明几何不等式,但在证明等式型几何定理时效率比以前的方法高得多。1984
