可由用户持续发展的几何自动推理平台的推理算法

收稿日期:2011-01-26;修回日期:2011-03-19。

作者简介:郑焕（1981-），男，广东湛江人，博士研究生，主要研究方向：几何自动推理； 张景中（1936-），男，河南汝南人，研究员，博士生导师，中国科学院院士，主要研究方向：几何自动推理、动力系统。

文章编号:1001-9081（2011）08-02101-04doi:10.3724/SP.J.1087.2011.02101

（1.广州大学 计算机科学与教育软件学院,广州510006； 2.中国科学院 成都计算机应用研究所,成都610041）

（peterpeter2001@163.com）

摘 要:目前的几何定理证明器都不具有可持续性。提出一种结构具有一般性的知识表示和能够统一处理所有规则的推理算法，初步实现了可由用户持续发展的几何自动推理平台。该推理平台允许用户添加几何知识，如几何对象、谓词和规则，并可以综合使用多种推理算法，如前推搜索法和一部分面积法，它将更适合用于几何教学。

关键词:几何对象；谓词；规则；几何定理证明器；可持续性

中图分类号: TP181文献标志码:A

Reasoning algorithm of

geometry automatic reasoning platform with sustainable development by user

ZHENG Huan¹, ZHANG Jing-zhong^1,2

（1. School of Computer Science and Educational Software, Guangzhou University, Guangzhou Guangdong 510006, China;

2. Chengdu Institute of Computer Application, Chinese Academy of Sciences, Chengdu Sichuan 610041, China）

Abstract: All the available geometry theorem provers are not sustainable. A knowledge representation with the general structure and a reasoning algorithm which could deal with all the rules were proposed. According to these ideas, a geometry automatic reasoning platform that could be sustainably developed by the user had been initially implemented. This platform allows the user to add geometric knowledge such as geometric objects, predicates and rules, and provides multiple reasoning algorithms such as forward search method and a part of area method, so it will be more suitable for geometry teaching.

Key words: geometry object; predicate; rule; geometry theorem prover; sustainability

0 引言

五十多年来，随着几何定理机器证明研究领域的发展，人们推出的几何定理证明器已经能在几秒的时间内证明很难的几何定理，甚至能生成可读的证明^［1-8］。但目前所有的几何定理证明器都不具有可持续性，也就是用户不能对系统做任何的修改。例如，用户不能往系统中添加几何知识，并且每次只能选择一种推理方法进行推理。文献［9-10］提出一种算法来实现用户可添加推理规则，但却没有与文章相关的应用程序发布。

几何定理证明器与人一样需要不断地更新知识才能解决新的问题。封闭的系统如果遇到不能解决的问题，它就永远不能解决这个问题了。系统如果每次只能用一种推理方法进行推理，它的推理方式就会比较单调。这些显然不符合人们的学习习惯。针对几何定理证明器的这一情况，本文提出建立可由用户持续发展的几何自动推理平台（Sustainable Geometry Automated Reasoning Platform, SGARP）。在这个平台上，用户可以添加几何知识和实现多种推理方法的综合使用。

本文已经初步实现了SGARP，它由知识库、知识编辑器、信息库、推理引擎、解释器和作图系统等六部分组成。目前，用户在SGARP上可以添加几何对象、谓词和规则，也可以综合使用前推搜索法和一部分面积法。本文主要介绍SGARP的知识表示和推理算法。

1 知识表示

本文把推理所用到的信息统称为知识。在任何自动推理系统中，知识表示在很大程度上决定着推理的方式。

1.1 基本概念

在SGARP中用到以下概念。

定义1 构成几何图形的基本单元称为几何对象。

几何对象由一个或几个不同的点表示，例如，直线由它上面两个不同的点表示。

定义2 几何构形中出现的几个几何对象或数之间的一种关系称为谓词。

例如，“中点”是一点和一条线段的一种关系。谓词可以看成布尔值函数，函数的变元是几何对象。某些几何对象本身也可以看成是几个点之间的关系，从而这些几何对象可看作特殊的谓词，例如平行四边形可看成是四个点之间的一种关系。

定义3 以基本几何对象作为参数的若干指定的函数叫做几何量。

例如，三角形的面积S_ABC、共线或平行线段比AB/MN是两个基本的几何量。

定义4 通常的几何公理、定理、引理等称为规则。

一个规则一般由条件和结论两部分组成，形式为：

P₁（X₁）∧P₂（X₂）∧…∧P_n（X_n）→Q（X₀）

其中：P_i（i1,2,…,n）和Q是谓词，X_k（k0,1,2,…,n）是一组几何对象。

定义5 一个几何图形中包含的几何对象、几何量等式和用谓词表达的几何关系统称为该图形的几何信息。

1.2 各种知识的表示形式

SGARP的知识库用于存储各种几何知识的表示形式，它由几何对象集、谓词集和规则集等三部分组成。下面是这三种知识在知识库中的表示形式。

1）几何对象：（name points）,（code₁）…（coden）。

几何对象的表示形式由两部分组成：第一部分包括几何对象的名称和组成几何对象的点；第二部分是一组编码。在识别几何对象时，人们根据经验就可以知道线段AB和BA表示的是同一条线段，但计算机本身没有这种经验，所以很多几何定理证明器对这一情况采取归一化处理，也就是对表示点的字母按字母表的顺序进行排序，使得每个对象在系统中只有一种写法。在SGARP中，每个几何对象赋有一组编码，使得计算机能够自动识别这些几何对象的等价写法。例如，直线的表示形式为：（line AB）, （1 0）。如果把A和B这两个字符存储在一个数组中，则第一个元素A的下标为0，第二个元素B的下标为1，所以用（1 0）表示BA。这里实际上省略了编码（0 1），因为（0 1）对应的是AB本身。从而利用编码，系统就可以判断（line AB）与（line BA）是同一条直线。

2）谓词：（name object₁ … objectm）, （code₁） … （coden）。

谓词的表示形式也由两部分组成：第一部分包括谓词的名称和相应的几何对象或数；第二部分是一组编码。其中编码的意义也是让计算机知道该谓词的等价写法。例如，两直线平行的表示形式为：（parallel（line AB） （line CD））,（1 0），其中编码（1 0）表示（line AB）和（line CD）可以互换位置。并不是所有谓词都需要编码，例如线段中点（midpoint（point M）（segment AB））这一谓词，可以规定点的位置在线段前面，从而（point M）和（segment AB）不能互换，所以线段中点这一谓词的编码为空。一般相同类型的几何对象在谓词中才有互换位置的可能。

利用谓词的编码和谓词中包含的几何对象的编码，就可以让系统自动生成谓词的所有等价写法。例如，对于（parallel（line AB） （line CD）），利用parallel的编码（1 0）就得到另一种等价的写法：（parallel（line CD） （line AB））。再利用parallel中第一个几何对象line的编码（1 0），就可以对已有的2种等价写法中的第一个几何对象作变换，得到该谓词的另外2种等价的写法：（parallel （line BA） （line CD））和（parallel（line DC） （line AB））。最后利用parallel中第二个几何对象line的编码（1 0），就可以对已有的4种等价写法中的第二个几何对象作变换，又得到4种等价的写法，所以一共有8种等价的写法。

上面的知识表示结构是具有一般性的，这种结构不但可以表示几何对象和谓词，还可以表示几何量和几何量等式。例如，用户可以添加三角形的面积这一几何量，表示形式为（area ABC）, （1 2 0）, （2 0 1）, （0 2 1）, （2 1 0）, （1 0 2）。如果用户定义三角形的面积是带号面积^［11-12］，则三角形的带号面积只有三种等价的写法，也就是只需前面两个编码。几何量可根据情况分别添加到几何对象集和谓词集中，例如三角形的面积可归到几何对象集中。利用添加的几何量，就可以添加一些简单的几何量等式，例如，线段比等于面积比：PM/QMS_PAB/S_QAB，这个等式可以表示为（EqlRatio（segment PM）（segment QM）（area PAB）（area QAB））,（1 0 3 2）。可以把几何量等式归到谓词集中。

在一般的几何定理证明器中，几何对象和谓词的表示方式基本上由名称和所包含的点这两部分组成，例如DC∥AB表示为（parallel D C A B）。系统对这一几何信息做归一化处理时，首先要对C、D与A、B进行总体上排序，再分别对A、B和C、D排序，得到（parallel A B C D）。不同的对象一般对应不同的归一化处理方式。知识的这种表示方式和归一化处理方法导致系统必须预先知道每个对象的结构和相应的归一化处理方式。所以几何对象和谓词必须在开发系统时就写好，不能由用户添加。本文建立的系统则突破了这个局限。

3）规则的表示由6部分组成：名称（Name）、条件（Premise）、结论（Conclusion）、约束条件（Order/Ndg）、规则的条件中包含不同的点的个数（DiffPointNumber）、文字描述（Description）。用户可以用已添加的谓词来描述规则的条件、结论和约束条件。例如，下面是三角形中位线定理的表示形式：

Name: MidLine

Premise: （midpoint D AB）

（midpoint E AC）

Conclusion: （parallel DE BC）

Order/Ndg: （NotCollinear A B C）

DiffPointNumber: 5

Description: 三角形中位线定理

其中约束条件用来说明几何图形中的点的位置关系，包括几何图形的序关系和非退化条件。例如，（NotCollinear A B C）表示A、B、C三点不共线。

要求用户输入规则的条件中包含不同的点的个数，是因为在推理的过程中可以根据这个点数迅速排除许多无效的信息，从而提高推理效率。当然规则的条件中包含不同的点的个数可以是一个范围，例如两个全等三角形，由于有公共顶点的情况，它们可能包含4至6个不同的点。

本文在表示规则时并没有在谓词里写上几何对象的名称，例如（parallel DE BC）没有写成（parallel（line DE）（line BC）），这是因为本文已经在知识库中把谓词parallel表示成（parallel（line AB）（line CD）），当系统在别的地方看到（parallel DE BC）时，会根据谓词名称parallel到知识库的谓词集中查找该谓词的具体表示形式，从而知道DE和BC都是直线（line）。本文在表示信息库中的几何信息时也采取这种表示方式。

在添加规则的时候，用户只需输入或选择上面所列出的六部分信息，系统会根据推理的需要，从规则的条件中分析出其他所需的信息。例如，系统把规则的条件中所用到的点依次排成一列，构成一个字符串，本文称之为条件字符串，在上面的三角形中位线定理中，条件字符串为“DABEAC”。然后再分析字符串中相同字符的位置并记录下来，在字符串“DABEAC”中，索引位置1和4的字符相同（都是A，在字符串中索引号是从0开始的），所以把它们的索引号（1,4）记录下来。系统把分析得到的字符串和索引号也储存在相应的规则对象中。

在一般的几何定理证明器中，系统对几何信息采取归一化处理，或者说几何信息约定了标准的形式，但在使用规则时，却经常要用到非标准的形式。例如三角形中位线定理的条件表示为（（midpoint D AB）（midpoint E AC）），这组标准形式的几何信息（（midpoint M DE）（midpoint N CD））显然符合定理的条件，但这组信息与条件的形式不同（这组信息中重复的字符D的位置与条件中重复的字符A的位置不同），系统不能直接比较。所以只能在系统中为每一条规则写一个推理函数来分析和协调这种不一致性，并且不同的规则对应不同的推理函数。若往几何定理证明器中添加规则，就必须用开发该证明器的计算机语言编写一个相应的推理函数。在证明器的实际应用过程中，一般用户显然无法添加规则。本文建立的系统则突破了这个局限。

用户在添加以上知识的时候，SGARP都提供了相应的对话框，用户只需输入对象的名称和选择相关的选项，系统就会自动生成以上形式的文本。

动态几何系统是SGARP的一部分，当选择画图工具作图时，系统会自动把相应的几何信息添加到信息库中。推理平台也提供了对话框给用户输入画图工具不能表达的几何信息，例如两个角相等。

2 推理算法

本文把规则的条件字符串中相同字母的位置称为规则的条件模式，例如三角形中位线定理的条件模式为（1,4）。对于某条规则的条件模式，如果一组几何信息中的点组成的字符串在相应的位置上字母也相同，则称这组几何信息符合这条规则的条件模式。本文推理的依据是：如果一组几何信息符合规则的条件，则这组几何信息必存在一种等价的写法符合该规则的条件模式；如果根据规则的条件从信息库中提取出来的一组几何信息符合规则的条件模式，则这组几何信息要么满足规则的条件，要么这组几何信息构成该规则的退化形式，或几何信息中的点所构成的图形的序关系与规则所对应的图形不一致。对于第二种情形，可以通过规则的约束条件来排除。下面是SGARP的推理算法。

输入 用画图工具作图和通过对话框添加辅助条件。

输出 几何图形中包含的几何信息。

步骤1 从知识库的规则集中读取规则，如果规则集为空，则结束推理，没有新几何信息产生；否则将指针指向第一条规则。

步骤2 读取指针指向的规则，然后把指针移到下一条规则。

步骤3 根据规则的条件中所用到的谓词，从信息库相应的信息类（SGARP的信息库由各个信息类组成，每个已添加的谓词对应一个信息类，信息类用于存储同一类信息,这样可以消除提取信息的盲目性）中提取几何信息进行组合，排除已经被这条规则检验过的信息组合。如果没有新的信息组合，则转到步骤8；否则转到步骤4。

步骤4 逐一检验提取出来的信息组合。用Data表示正在被检验的一组几何信息。首先检验Data中包含不同的点的个数是否符合该规则的要求，如果符合，则转到步骤5；否则检验下一组几何信息。如果所有的信息组合已经检验完毕，则把已检验过的信息组合记录在该规则中，转到步骤8。

步骤5 生成Data的所有等价写法：Data₁，…，Datan，其中Data₁Data。依次检验这些等价写法是否符合规则的条件模式。假设Datai（1≤i≤n）是正在被检验的等价写法，如果Datai符合规则的条件模式，则把规则的条件字符串记为str1，把Datai对应的字符串记为str2，得到一组匹配的字符串（str1,str2），然后转到步骤6；否则检验下一个等价写法Data_i+1。如果Data的所有等价写法已经检验完毕，则转到步骤4检验下一组几何信息。

步骤6 如果规则有约束条件，则根据（str1,str2），把规则的约束条件所包含的点用str2中对应的字母代替，得到实际的约束条件。然后调用实际约束条件中的点的坐标，通过数值计算来检验约束条件。如果约束条件不成立，则转到步骤5，验证Data_i+1。如果约束条件成立或规则没有约束条件，则转到步骤7。

步骤7 根据（str1,str2），把规则的结论所包含的点用str2中对应的字母代替，得到这条规则推出的几何信息，检验推出的几何信息在信息库中是否是新信息，如果是新信息则把它加入到信息库中，并记录信息库中的信息量；否则不添加信息。转到步骤4验证下一组几何信息。

步骤8 如果指针的指向不为空，则转到步骤2；否则说明刚才检验的是规则集的最后一条规则，也就是已经完成了一轮推理（从规则集的第一条规则到最后一条规则的推理称之为一轮推理）。检验在这一轮推理中信息库的信息量是否发生了变化，如果信息量发生变化，则转到步骤1；否则推理已经达到不动点，结束推理并显示信息库中的全部几何信息。

因为一个几何图形的几何信息是有限的，所以推理不动点总是可以达到的。

下面以三角形中线定理这条规则为例说明算法中步骤3～7的具体工作方式。

步骤3 因为三角形中线定理的条件由两个中点谓词（midpoint）组成，所以从信息库的中点信息类（midpoint）中提取几何信息进行两两组合。

步骤4 假设Data（（midpoint M ED）（midpoint N DF））。Data中包含5个不同的点，符合规则的要求，转到步骤5。

步骤5 由于Data中所包含的两个谓词名称都为midpoint，到知识库的谓词集中查找midpoint的具体表示形式，得到midpoint的编码为空，并且它包含几何对象point和segment；再到知识库的几何对象集中查找point和segment的编码，得到point的编码为空，segment的编码为（1 0）。然后根据查到的编码生成Data的4种等价的写法：Data₁（（（midpoint M ED） （midpoint N DF）），Data₂（（midpoint M DE） （midpoint N DF）），Data₃（（midpoint M ED） （midpoint N FD）），Data₄（（midpoint M DE） （midpoint N FD））。检验Data_i（i1，2，3，4）对应的字符串，可以发现Data₂的字符串“MDENDF”符合规则的条件模式，所以得到一组匹配的字符串（“DABEAC”,“MDENDF”）。

步骤6 由于该规则有约束条件（NotCollinear A B C），所以根据（“DABEAC”,“MDENDF”）中的点的对应关系，替换约束条件中的点得到实际的约束条件（NotCollinear D E F）。在检验这个约束条件时，系统首先调用点D、E和F的坐标（这些点的坐标在画图的时候已经记录在动态几何系统中），再利用坐标来计算这三点是否共线。如果点D、E和F不共线，则转到步骤7。

步骤7 根据（“DABEAC”,“MDENDF”）替换规则的结论中的点，得到该规则推出的几何信息（parallel MN EF）。在判断信息库中是否已经存在该信息时，首先生成（parallel MN EF）的8种等价写法，逐一检验每种写法是否已经在信息库中，如果都不存在，则把（parallel MN EF）添加到信息库中；否则不添加这条几何信息。这样的添加方式可以保证信息库中不会出现重复的几何信息，所以本文不需要对几何信息做归一化处理。

由推理的过程可以看出知识库中的几何对象和谓词在推理中的作用只是提供相应的编码，让系统生成几何信息的等价写法，从而几何对象和谓词是可以由用户添加的。规则的表示形式也是比较直观的，并且与一般的几何定理的表述非常接近，除了在添加规则的时候系统会自动生成规则的条件字符串和字符串中相同字母的索引号，在推理的过程中并没有改变规则的表示形式，从而推理平台中的规则是容易被用户理解的，也是方便用户添加的。由上面的讨论可以看出SGARP主要是基于前推搜索法的，因为SGARP允许添加几何量和表达式，所以用户也可以在SGARP上添加一部分面积法的消点公式（例如共边定理）来实现面积法推理。

3 运行实例

下面举例说明上面算法的执行情况。

例 设ABCD是任意四边形。四边AB、BC、CD和DA的中点顺次为E、F、G、H。求证：EFGH是平行四边形。

在这个例子中，本文先向知识库中添加以下两条规则，括号中是它们在SGARP中的名称：

1）三角形中位线定理（MidLine）；

2）平行线的传递性（Transfer）。

运行结果如图1所示（在图的下方调出SGARP中查看规则的对话框，这时知识库的规则集中只有刚才添加的两条规则），其中树型图的根节点分别对应信息库中的信息类，每个子节点对应一条几何信息，几何信息前面的中括号中是推出这条几何信息的规则名称。由三角形中位线定理的表示形式可以看出，并不需要连接AC，也能推出EF∥AC。根据刚才添加的两条规则一共推出6条平行信息。但信息库中并没有平行四边形信息，说明根据这两条规则还不能推出EFGH是平行四边形。

图1 SGARP的运行结果一

虽然利用前面的两条规则还不能推出EFGH是平行四边形，但是由它们推出的平行信息，可以发现只需再添加“两组对边平行的四边形是平行四边形”（PlgmDet）这条规则即可。添加这条规则后，运行结果如图2所示，几何信息所在的节点的子节点是推出这条几何信息所用到的条件。

图2中展开的节点是这道命题的证明过程。如果用数学语言代替SGARP中几何信息的表示方式，则这个证明过程如下：

1）EF∥AC（由E是AB的中点、F是BC的中点及三角形中位线定理）；

2）GH∥AC（由G是CD的中点、H是AD的中点及三角形中位线定理）；

3）EF∥GH（由1）、2）及平行线的传递性）；

4）EH∥BD（由E是AB的中点、H是AD的中点及三角形中位线定理）；

5）FG∥BD（由F是BC的中点、G是CD的中点及三角形中位线定理）；

6）EH∥FG（由4）、5）及平行线的传递性）；

7）EFGH是平行四边形（由3）、6）及平行四边形的判断法则）。

图2 SGARP的运行结果二

4 结语

在一般的几何定理证明器中，知识与控制机制没有分离开来，也就是知识表示与推理机制互相渗透（例如：规则表示为推理函数），用户一般看不到知识在系统中的表示形式，所以几何定理机器证明对于许多人来说有一种神秘感。如果用户可以管理证明器的知识库，那么理解几何定理机器证明就不难了。

在SGARP中，知识与控制机制是分离的，这使得SGARP具有可持续性。这种把知识与控制机制分开维护使用户可以更自然地表示知识。例如，“如果……那么……”形式的规则比底层的计算机代码更接近人类描述问题求解技巧的方式。

在SGARP上，用户可以按照自己的学习进度建构知识，还可以不断地修改已添加的知识，所以SGARP的知识结构可以做到因人而异，求解问题的过程可能会更加符合用户对问题的理解。用户也可以在SGARP上发展不同的推理方法，并实现多种推理方法的综合使用，而不是一次只能用一种推理方法。从而与一般的几何定理证明器相比，SGARP将会更适合用于教学。

在一般的几何定理证明器中，用户不能对系统做任何的修改，所以当别人开发的证明器不能满足自己要求时，他只有按照自己的想法重新开发自己的证明器。这里就有大量的重复编程劳动。对于研究几何定理机器证明的学者，有了SGARP，他们不必自己从头开始编写程序，可以集中精力于方法的创新。这对几何机器证明的理论与算法的发展的推动意义是不言而喻的。

参考文献:

[1] 张景中,高小山,周咸青.基于前推法的几何信息搜索系统［J］.计算机学报,1996,19（10）:721-727.

［2］ GELERNTER H. Realization of a geometry theorem proving machine ［M］// Computers and Thought. Cambridge, USA: MIT Press, 1995:134-152.

［3］ NEVINS A J. Plane geometry theorem proving using forward chaining ［J］. Artificial Intelligence, 1975, 6（1）: 1-23.

［4］ 张景中,李永彬.几何定理机器证明三十年［J］.系统科学与数学,2009,29（9）:1155-1168.

［5］ 江建国. iGeo_智能几何软件的定理证明器［D］.成都:中国科学院成都计算机应用研究所,2006.

［6］ 罗慧敏.基于消点法的几何自动推理系统实现［J］.计算机应用,2008,28（11）:2984-2986.

［7］ YE ZHENG, CHOU S C, GAO XIAO-SHAN. Visually dynamic presentation of proofs in plane geometry ［J］. Journal of Automated Reasoning, 2010, 45（3）: 243-266.

［8］ 邹宇,郑焕,张景中.仿射质点几何的可读机器证明［J］.计算机应用,2010,30（7）:1899-1901.

［9］ 郭四稳.基于用户自添加规则的自动推理程序［J］.计算机应用与软件,2007,24（9）:48-50.

［10］ 郭四稳.基于用户自添加规则的自动推理程序Ⅱ［J］.计算机与信息技术,2006,23（8）:67-71.

［11］ CHOU S C, GAO XIAN-SHAN, ZHANG JING-ZHONG. Machine proofs in geometry: Automated production of readable proofs for geometry theorems ［M］. Singapore: World Scientific, 1994.

［12］ 张景中.计算机怎样解几何题［M］.广州 :暨南大学出版社,2000.