几何自动推理系统发展研究

□刘颖奇，黄 勇

( 广州大学计算机科学与教育软件学院，广东 广州 510006)

自动推理是用某种方法剖析推理问题的各个方面，让计算机完全或接近完全的得出推理结果。几何自动推理系统是将自动推理中定理机器证明的研究成果的应用在几何软件中的产物，目前主要应用在数学教育方面，它能使教师深入研究几何问题并辅助几何教学，创新试题启发与调动学生发散思维，创设自主学习环境，在几何教学中有重要作用。回顾几何自动推理与几何软件的发展历史，结合当前数学教育的实际要求和软件技术的发展方向，探讨未来的发展趋势，可以促进几何自动推理、几何自动推理系统的发展。

一、几何自动推理的历史和现状

1899年希尔伯特出版了名著《几何基础》，其中提供了对一类几何命题进行检验的定理。1948年Tariski发表了著名的结论：一切初等几何和初等范围内的命题，都可以用机械化的方法判定其是否成立。1959年王浩教授设计了一个程序，用计算机证明了《数学原理》中的几百条定理，总共仅用9分钟。但此后20多年间由于方法过于复杂，初等几何定理的机器证明并未取得预期的进展。

直到1977年吴文俊院士发表了机器证明领域里程碑式的文章，利用吴方法可以在几分钟甚至几秒钟证出很不简单的定理。吴方法实际是一种坐标方法，其主要思想是把命题涉及的几何构形中的点坐标化，把命题的条件和结论表示为坐标的多项式方程组，然后检查条件方程组的解是否满足结论方程组。以吴方法为首的坐标方法只能够告诉人们命题的真假，其计算过程复杂且不易看懂，其证明过程是“不可读”的。

几何定理的可读证明直到1992年才取得突破，张景中院士将多年研究的面积法作为基础，提出了消点算法。张院士和周咸青、高小山合作，编制的程序在Next微机上产生了478条非平凡的几何定理的可读证明。消点法包括一组作图规则, 一组几何量和关于这些规则和几何量的一组消点公式。对于一个给定的几何命题，先按作图规则作出图来。在作图过程中产生一组点的等式型约束条件。把命题结论表示为图中的几何量的一个等式。证明的过程是利用消点公式，按与作图时的相反的顺序将结论等式中的点一个个逐步消去。

消点法的证明和传统的证明表达方式还是有差异，1996年张景中院士、高小山研究员、周咸青教授在文中提出了基于前推的“几何信息搜索系统(GISS)”。该系统对平面欧式几何实现了几何信息搜索。GISS系统由于采用了“全角”这个常人并不熟悉的概念，所以与传统的人工证明相比还是有差距。1999年在张景中院士的指导下，黄勇博士完成了博士论文，研制的系统能在合理时间内产生完全传统方式的几何定理的(直接和间接)证明，其中直接证明采用的是搜索法，间接证明使用的是同一法，这也是同一法首次在几何定理机器证明中实现。

最近几年，几何自动推理研究获得了一系列成果。例如，郭四稳博士实现了用户可自添加规则的几何自动推理系统；江建国博士将人工神经网络用于几何自动推理。

从以上论述可看出，几何定理的机器证明目前已经有了稳固的理论基石与切实可行的算法。该领域目前主要的研究集中在如何才能使推理更快速，更人性化。

二、几何软件的历史和现状

现在所指的几何软件一般是具有动态几何功能的几何软件，称为动态几何软件。最早的是上世纪80年代诞生的The Geometer's Sketchpad。根据文献显示，国外的平面几何软件工具多达30余种。其中名气最大的是The Geometer's Sketchpad与Cabri，前者的4.0版本1996年被人民教育出版社引进汉化后出版，即大家所熟知的《几何画板》。

遗憾的是The Geometer's Sketchpad至今都没有自动推理的功能，Cabri在Cabri I中有概率证明，在Cabri II Plus中部分实现了交互推理，但也没有自动推理。在国外的几何软件中具有自动推理功能的主要有GCLC、GeoProof、Geometrix。其中GCLC中可以使用面积法、吴方法、GrÖbner 基法，GeoProof中可以使用吴方法、GrÖbner 基法。GCLC并没有提供交互的作图，需要通过文本的方式键入作图指令，其定理的证明也是采取文本键入命令的方式执行。Geometrix是通过外部插件的方式实现符号演算。GCLC、GeoProof和Geometrix都只能在单机使用和显示。随着网络的发展，国外的一些几何软件通过插件实现了在浏览器中显示由单机软件完成的图形。例如Cabri Java、Java SketchPad。但这些插件只能显示已经完成的文件，不是一个创作工具，没有自动推理功能。

最近几年国外基于浏览器的几何软件逐渐兴起。已知的有Dynamic geometry、GeometryEditor。前者是基于sliverlight开发的一个在浏览器中运行的动态几何软件。后者是美国肯特州立大学正在研究中的一个项目，基于SVG技术开发。这两者都没有自动推理功能。我国的几何软件是伴随着定理机器证明的发展，一直致力于将定理机器证明的成果应用到几何软件中。国内的几何软件的开发始于上世纪90年代，有先后出现的《几何专家》、《平面几何》、《超级画板》等几何软件。上面提到的几个软件均有自动推理的功能。其中《几何专家》使用面积法、吴方法、GrÖbner 基法；《平面几何》中使用了搜索法、同一法；《超级画板》中使用几何信息搜索系统。《几何专家》没有输出为网络格式的功能，只能在单机使用和显示。《平面几何》和《超级画板》可以将图形输出为HTML格式，安装插件后，可以在浏览器中打开文件演示动态几何、作图、修改等，但此时不能保存且没有自动推理功能。目前中科院系统所和美国维奇塔大学正在合作开发《JAVA几何专家》，这是一个可以完全基于浏览器的动态几何软件，具有自动推理的功能。它推理使用的是吴方法、全角法、GrÖbner 基法还有演绎数据库法。《JAVA几何专家》实质上也是通过将软件下载到本地在浏览器中调用执行的，其动态几何命令的处理以及推理运算都是在本地机器执行，文件只能保存在本地，不能通过网络共享，还是类似于单机软件。

三、研究展望

从前面的论述中可以看出，目前几何自动推理的单机软件已经发展的比较成熟，而几何软件的网络化已经兴起，但仍处在起步阶段。一部分软件具有网络功能，但仅仅提供了在浏览器中显示或可以简单修改由单机软件创作的几何图形。只有《JAVA几何专家》是完全的可在浏览器中运行的具有动态几何与自动推理功能的软件。但它并没有体现出网络应用的优势，实质还是一个在浏览器中使用的“单机软件”。

如今互联网成为人们生活的一部分，越来越多的软件走向了网络平台。网络软件不需要本地安装，用户只需要打开浏览器，就可使用，其使用便捷、没有盗版困扰、可以更合理地利用资源。软件向网络化发展是目前的大势所趋。

在几何自动推理的理论研究已经日渐成熟的今天，单纯的通过算法的改进来提高推理的速度和可行性已经日渐困难，而网络计算提供了强大的计算能力，我们可以使用网络计算来增强推理的效率，例如一个问题在单机上也许需要10分钟的时间才能推出来，那么利用网络计算的强大计算能力，加快推理速度，让推理的结果在用户满意的时间内得出。同时构建基于网络运行的几何自动推理系统，也将大大地方便用户之间的交流协作，共享数据。在教育领域，现今涌现出了大量的CMS系统，这些网络教学平台促进了协作交流，获得了快速的发展。但CMS针对的是所有的学科，在专业性方面还是存在很多不足的，所以发展基于网络的几何自动推理平台，其专业性可以保证更好地完成几何教学方面的课后交流协作与探讨研究。

基于网络构架的动态几何与自动推理平台还在研究的起步阶段，如何利用网络构架的优势，更好地进行推理，研制更方便用户使用，方便几何教学与研究的网络几何软件平台的研究鲜有人涉足。几何自动推理在不改进现有的算法的情况下可以利用网络计算来增强推理能力，同时几何自动推理系统也应该向网络化发展。

参考文献：

[1]Tariski A, A decision method for elementary algebra and geometry. The RAND Corporarion,Santa Monic, 1948.

[2]黄勇.基于前推能产生传统证明的几何自动解题系统[M].成都：四川大学博士论文，1999.

[3]吴文俊.初等几何判定问题与证明机械化[J].中国科学,1977，(6).

[4]张景中,高小山,周咸青.基于前推法的几何信息搜索系统[J].计算机学报,1996, (10).

[5]郭四稳.基于用户自添加规则的自动推理程序[J].计算机应用与软件,2007,(9).

[6]江建国.iGeo:智能几何软件的定理证明器[M].北京：中国科学院博士论文，2006.

[7]List of interactive geometry software http://en.wikipedia.org/wiki/Interactive_geometry_software 2009-04-07.