- 1 -
中国科技论文在线
基于向量的几何可读自动证明#
葛强1,2，陈矛1**
基金项目：国家自然科学基金（60903023）；高校博士点新教师课题基金（200805111011）
作者简介：葛强，男，（1977-），博士研究生，主要从事机器证明的研究。
通信联系人：陈矛，男，（1975-），副教授，主要从事自动推理和算法研究。
（1. 华中师范大学国家数字化学习工程技术研究中心，武汉 430079；
2. 河南大学数据与知识工程研究所，河南 开封 475001） 5
摘要：几何定理机器证明已经成功发展了多种新方法，但其中对中学几何中向量的机器证明
研究没有抓住其回路的基本特征．本文以向量的回路为出发点，提出了基于回路的向量可读
证明新方法，开发了机器证明新程序．本程序对常见的构造类型欧氏几何题目能快速作图，
依据题目类型的不同，分别用不同的向量方法对其进行自动推理，证明结果简短可读．由于
向量法为中学课本内容，这种自动证明方法可用于教学实践．经过多个实例测试，证明向量10
用于自动推理是可行的，几何证明在效率和可读性方面得到了提高。
关键词：机器证明；可读证明；前推法；向量；回路
中图分类号：TP181
Automated Geometry Readable Proving Based on Vector 15
Ge Qiang1,2, Chen Mao1
(1. National Engineering Research Center for E-Learning, Huazhong Normal University,
WuHan 430079;
2. Institute of Data and Knowledge Engineering, Henan University, HeNan KaiFeng 475001)
Abstract: The field of automated geometry theorem proving has developed many new methods 20
successfully; however, all of them have not utilized the loop of vectors. In the paper, the authors
have proposed a new approach based loop of vectors, implemented a machine proof program,
which emphasis loop of vectors. This program can construct most common constructive geometry
drawings quickly, do automated reasoning with various methods in according to types of
constructions, and the proofs are concise and readable. The prover with vectors has been used to 25
produce short and elegant proofs in middle schools; this approach could be applied into education.
With many instances test, it denoted automated reasoning with vectors is available, it have
enhanced the efficiency and readability.
Keywords: machine prove; readable proof; forward chaining; vector; vector loop
30
0 引言
几何学作为具有严密逻辑思维的一门科学已经诞生了二千多年．它借助于巧妙的论证技
巧能解决大量丰富的几何命题．近几百年来，陆续有学者希望用统一的手段来处理千变万化
的几何问题，如，笛卡尔(1596-1650)，莱布尼兹(1646-1716)．直到希尔伯特(1862-1943)，应
用笛卡尔发明的坐标法，对只涉及点和直线的关联性质的一类几何命题才给出了一种机械判35
定算法．自从计算机成功发明后，几何定理机器证明研究领域的才逐渐形成．
几何定理的机器证明在自动推理的研究中占有重要的地位．自吴法发表至今 30 年，几
何定理机器证明的研究和实践有了很大的进展[1, 2]．代数方法、数值方法均能有效地判定
给几何定理的真假，现在的研究趋势是使证明结果可读，有背景知识的人可以轻松地看出结
果是否正确，形式是否优美．可读的推理结果不仅可以用于科学研究，更可以用于教育教40
学．张景中先生提出了基于不变量的机器证明方法[3]，面积法(消点法)[4]，加速了可读证明
研究的步伐．众所周知，搜索法更能生成其可读的证明，为几何证明机械化提出了新的方法
[5-8]．这些不同的方法能够解决不同的几何题目，显示了算法的多样性和几何的丰富多彩性．
- 2 -
中国科技论文在线
上面所述的各种机器推理证明方法，各有优点．他们研究的共同对象是欧氏几何，这是
中小学数学学科的必学内容，因此教育是自动推理成果应用得最广泛的领域．学生们对上面45
研究方法产生的证明过程并不容易看懂，还需要另外学习很多其它辅助知识，增加了应用于
教育的难度．另一方面，中学新引入的向量知识简单易懂，虽然高小山[9]和 Stifter[10]研究
过，但他们的证明过程也不是普通的综合证明形式，不容易看懂．因此，有必要研究一种新
的向量机器证明方法，能够抓住向量的本质特征，这种方法可以产生优美的可读证明．
尽管几何学已经出现了二千多年，但对其研究随着计算机的发展仍然在进行．已经有研50
究者研究了几何向量的公理系统[11]和几何对象的语义表示问[12]。这些研究扩大了机器证
明的范围，为向量应用于机器证明提供了思路．一般这样认为，对于平面上的有向线段 AB
JJG
，
当我们只考虑其大小和方向而不管其位置时，就把它叫做向量． 高小山，Stifter 等研究者
已经研究了使用向量进行机器证明．高小山提出基于向量内积和外积计算的消点方法，可以
证明一些结论为等式型的构造型几何命题。Stifter 则采用向量空间中的 Grönber Bases 方法，55
来证明那些几何关系能够形式化为点之间代数运算的几何题目。这两种方法各具特色，然而
可读性不强，而且忽略了向量能够构成回路的直观性．
为此，基于向量回路的特点，我们提出采用回路等式来展开向量进行等价代换，进行相
关的简单运算和判断．使用回路的向量法非常直观，抓住了向量加减法的特点．为使其证明
过程可读，整体上采用搜索法．根据不同的题目，分别采用前推法和后推法，这样使得证明60
结果可读，简单易懂．这样的解题方法用于中学教学会更受到欢迎．这项研究成果将来可以
开发成教育软件，将会增加机器证明的新方法，开拓学生的解题思路．
1 欧几里得几何学的向量公理系统
每个几何系统都可用许多（等价的）公理系统来刻划．两个等价的公理系统可以建立在
不同的无定义项集合上，而在某一公理系统中的无定义项可以在一个等价的公理系统中由另65
外的概念来定义．因此，在十九世纪末和二十世纪初期出现了欧几里得几何学的好些等价公
理系统．希尔伯特（ 1862-1943）提出的平面几何公理系统采用“点和直线”作为
无定义项．差不多与此同时,意大利数学家皮利（ 1860-1913）提出的欧几里得几何
学公理系统是建立在无定义项“点与运动”之上的，大约也那时，俄国几何学家卡冈（
Kagan l860-1953）阐述的公理系统却是建立在“点与距离”概念之上的． 70
近几十年提出的（平面和空间）欧几里得几何学公理系统通常是建立在无定义项“点和
向量”基础上的．欧几里得平面几何学的公理系统也可以是向量的，并且包括五组公理，包
括 I向量的加法公理，II数乘公理，III维数公理，IV数量积公理和V点-向量关系的公理[11].
我们的无定义项是点和向量，并认为实数是己给定的．要求向量构成一个向量空间，即
向量加法是可交换，可结合的．向量数乘是可结合的，对于数的加法是可分配的，对向量加75
法也是可分配的．I 和 II 组公理蕴含着零向量0 以及一个给定向量a的加法逆元a' = -a的
唯一性．
我们正在研究的平面几何学（或二维几何学）由下列 III 维数公理，IV 数量积公理及 V
点-向量关系的公理所定义．在本文中使用最重要的是应用 III 维数公理:
III1：对于任意三个向量a,b,c，存在不全为零的三个数，使得 80
αa + βb + γc = 0
III2：存在两个向量a,b，使得
- 3 -
中国科技论文在线
αa + βb = 0仅当 0 0α = β =且
通常，维数公理的阐述包含着向量线性相关的概念．我们说向量 1 2 ka ,a , ...a 是线性相
关的，如果存在不全为零的数 1 2, ,... kα α α ，使得 ... kα α α+ + + =1 2 ka a a1 2 0 ．反之，伐85
们就说向量 1 2 ka ,a , ...a 是线性无关的．
为了使公理 I，II 和 III 所决定的二维向量空间（向量平面）成为欧几里得向量空间，
我们还必须在连结着向量和（实）数的无定义关系中添入一个二元运算，叫做向量的数量
积．它把一对向量a,b结合到一个数α ,叫做a与 b 的数量积，记为ab．向量的数量积是
可交换的，对于向量的数乘运算是可结合的，对向量加法是可分配的，数量积是半正定的． 90
在两个无定义项-点和向量-以及 I、II、III、IV 和 V 组公理基础上展开欧几里得几何学
是很方便的．然而，在绝大多数科学文献中，这个题目的阐述都只依赖于一个无定义项：向
量．这样表述时，省略去第 V 组公理，并且将点与向量视为同一．
向量公理系统的建立，为几何对象及几何关系的表示奠定了理论基础．由于向量是结合
了图形与代数的表示，因此，向量法的证明过程是与图形紧密联系的．虽然，其可读性不依95
赖于图形，但可以借助于图形更好地理解其向量的回路．
2 基于搜索法的向量法可读证明
本章介绍几何推理引擎用前推法进行几何定理证明的原理，重点描述介绍量推理规则的
构造．几何推理引擎是指在几何定理机器证明中，根据输入的几何信息，调用相应的推理规
则，得到更多的几何信息的应用程序模块．一般地，几何推理引擎存在着一个推理不动点，100
是判断推理引擎是否停止工作的标志，即信息总体数量不会再增加时，几何推理引擎达到了
推理不动点．
推理引擎的数据源
注意数形结合，灵活选择回路，利用共线线段成比例性质和向量维数公理，必要时辅以
向量的内积，这就是用向量法解几何题的基本思路．在本文中，几何推理引擎主要使用的是105
前推法来实现这个基本思路．在一些目标明确的向量法规则中可以局部地应用后推法[13]．
推理引擎的数据源是构造型几何图形．它根据几何图形关系进行信息提取，作为输入数
据．再根据已有信息的特点，调用各个向量推理算法，全部算法调用结束后查询信息库中信
息的数量，如果有变化，再继续循环，没有则结束．
推理引擎在数据驱动的基础上进行算法调配．由于各种算法都有相应输入数据作为驱110
动，那么各种数据就会对应有各种算法，根据一种或多种信息的组合，推理引擎调用其对应
的算法，算法执行得到的结果被存储到相应的信息库．
几何关系的向量表示形式与欧氏几何表示形式不同，其实是等价的，只是欧氏几何在生
活中更为常用，流传更广．因此，向量法证明结论有时需要转换成欧氏几何表示法．向量法
会得出一些普通前推法不能得到的数据信息，将其转化为对应的欧氏几何表示方法，存储入115
信息库，方便读取和显示，为下一步推理提供了更多的数据．
向量是中学的教学内容，向量推理算法是已有机器证明方法的必要补充．它的出现不仅
丰富了几何关系的表示形式，也进一步丰富了机器证明方法．普通的几何推理引擎加上了向
量法之后，可以提高其推理能力和效率．
- 4 -
中国科技论文在线
平面几何与向量的相互表示 120
平面上任意一个几何对象或几何关系，如，线段，多点共线，线段平行，垂直，相等，
平行四边形等，都有相应的向量表示形式．为了统一表示几何信息，对向量形式的证明结论
要用欧氏几何方法来表示．下表仅列出了本文需要用到的一些表示形式．
表 1 平面几何与向量的相互表示 125
Representation of geometry and corresponding vector
平面几何表示形式 向量表示形式 说明
线段 AB ABJJJG 同一条线段的不同表示
点 C在线段 AB上 AC k AB= ⋅JJJG JJJG 0k ≠ ，k为 AC与 AB长度之比
AB//CD CD k AB= ⋅
JJG JJG
0k ≠ ,AB,CD是同向
AB CD⊥ 0AB CD⋅ =
JJG JJG
两线段垂直，向量内积为 0
平行四边形 ABCD AB DC=
JJG JJG
平行四边形两组对边分别为相等向量
正方形 ABCD AB DC=
JJG JJG
, 0AB BC⋅ =
JJG JJG
正方形的对边向量相等，相邻向量垂直
基于向量法的推理算法
向量的推理算法抓住了向量运算的特点，利用向量直观的优势，对于一些交点类构造型
题目可以生成简短的证明过程[14]． 130
向量法证明工具
［1］ 基本回路法
所谓回路，就是从向量的一个端点出发，通过一个封闭的图形又到达终点的那个通路，
这个通路与原向量的效果是等价的，是对向量加法的应用．最简单的回路就是
AC AB BC= +
JJG JG JJG
135
在向量运算中，经常要用表示一个回路的多项式来代替一个向量．这样，就可以引入后续的
交点或是数量信息，方便可以进行后续代换，得到关于求证结论的关系表达式．
［2］ 向量数乘的运用
利用向量数乘公理，可以表示更多的向量．实数 k 与向量a的积也是一个向量，记作
kaG．当 0>k 时，ka的方向与a的方向相同；当 0k < 时，ka的方向与a的方向相反；当140
0k = 时， k =a 0，方向是任意的．
显然，向量数乘满足交换律、结合律与分配律．
［3］ 向量内积的运用
已知两个非零向量 1 1{ , }x y=a 与 2 2{ , }x y=b ，它们的夹角为 (0 )θ θ π≤ < 则
cosθ⋅ =a b a b 叫做a与 b 的数量积或内积． 145
数量积的几何意义： ⋅a b等于aG的长度与b 在a方向上的投影的乘积．
如果a与 b 的夹角为
2
π ，则称a与 b 垂直，记作 ⊥a b．两个非零向量垂直的充要
条件： 0⊥ ⇔ ⋅ =a b a b 1 2 1 2 0x x y y⇔ + = ．这将会用在向量垂直的性质表示中．
［4］ 向量维数公理的运用
如果 1e ， 2e 是一个平面内不共线的两个向量，那么对这一平面内的任一向量a，有且150
只有一对实数 1λ ， 2λ 使得 1 1 2 2λ λ= +a e e ，其中不共线的向量 1e ， 2e 叫做表示这一平面
- 5 -
中国科技论文在线
内 所 有 向 量 的 一 组 基 底 ． 换 句 话 来 说 ， 若 1 1 2 2 1 1 2 2k kλ λ= + = +a e e e e ， 即
1 1 1 2 2 2( ) ( )k kλ λ− = −e e ，而 1e ， 2e 是不共线，必有 1 1 2 2,k kλ λ= = ．这是对向量维数公
理的应用，也是向量法解题之基本工具．这种运用表明，选好基底后，平面上任意一点都
可以用一个二维数组 1 2( , )λ λ 表示，这和选好直角坐标系后，平面上任意一点都可以用一155
个二维数组 ( , )a b 表示，本质上是一致的．从这条基本定理可知，如果四个向量之间有等
式 a b c d+ = + ,并且 a 和 c 共线， b 和 d 共线，但 a 和 b 不共线，立刻可以推得
,a c b d= = ．这个方法在后面的例子中多次使用．
［5］ 中位线法则
中位线一般出现在三角形和四边形中，四边形中位线的形式也包含了三角形中位线的160
表示形式．四边形中位线的向量形式：任意四边形 ABCD中（这四点无需在同一平面上），
M，N分别是 AD，BC中点，则 2MN AB DC= +
JJG JJG JJG
．
证明：
2 ( ) ( )MN MD DC CN MA AB BN= + + + + +
JJG JJG JJG JJG JJG JJG JJG
( ) ( ) ( )MD MA BN CN AB DC AB DC= + + + + + = +
JJG JJG JJG JJG JG JJG JG JJG
此结论相当重要，它包括下面的几种特例，在以后的证明中会直接用到．这几种特例，165
也是大家所熟悉的．
（1）如果 A，D两点重合， 2AN AB AC= +
JJG JJG JJG
，此即三角形中线的向量形式；
（2）如果 C，D两点重合， 2MN AB=
JJG JG
，此即三角形中位线定理；
（3）如果 AB//CD，此时四边形为梯形， // //AB CD MN ， 2MN AB DC= +
JJG JG JJG
表示梯形的
中位线定理． 170
（4）如果 AB//CD，且 C、D 两点错位，此时四边形为梯形， // //AB CD MN ，
2MN AB DC= −
JJG JJG JJG
表示梯形两对角线的中点的连线平行于底边且等于两底差的一半．
典型的向量机器证明算法
在交点类几何习题中最后出现的点，我们称其为终结点．能够保持几何图形中某种几何
关系不变的点叫做约束点．终结点一般也是约束点． 175
向量法可以处理涉及交点的问题，其诀窍在于首先构造一个涉及解题目标的回路等式，
然后利用题设条件和回路表达式等价代换，尽量把等式中的向量都转移到相交的线段上，最
后应用向量维数公理获取结论信息．以上思想，应用在下面的几种主要的算法当中．下面是
对这些算法的简要描述．
［1］ 从相等向量出发的证明方法 180
本算法的适用条件是，在图形中有一个或一个以上的中点，利用中点将线段平分成两个
相等向量的特点，构造一个向量等式进行搜索与代换，求解的结果为向量相等或是两个向量
为定比．
算法 1：相等向量算法
输入：含中点的几何图形 185
输出：向量之间的比例
S1.查询是否存在两个已知相等的向量，如果不存在，则转 S8；如果存在，则分别从两
个相等的两个向量出发，分别进行“首尾相连法”回路搜索，将路径最短的回路表达式
MinLoop 返回，构造等式表达式 EqualExpr．在路径长度相等的情况下，优先返回含终结点
- 6 -
中国科技论文在线
的表达式． 190
S2.在 EqualExpr 中，约去条件中相等的向量．
S3.运用向量维数公理，得出新的向量表达式．如果成功，转 S7，否则进行下一步．
S4.将等式中两个向量端点互异的向量进行移项，整理表达式．
S5.对不含终结点的向量再次进行回路搜索与代换新的 MinLoop．
S6.再次运用向量维数公理，得出新的向量表达式．如果成功，进行下一步，否则，转195
S8．
S7.将向量表达式转换成欧氏几何形式，存储入 InfoList 中，算法执行过程存储入
ReasonList 中．
S8.结束．
回路选择的原则方法： 200
在 S1 中，要注意采用约束点所在的回路．其中一边则采用终结点所在的回路，以使用
其不对称性，以便突出最终点．如果是平行四边形问题，则对回路大于 3的优先等量代换，
换成对边相关的向量．在 S5 中，则要对非终结点的再次执行回路搜索，此次采用终结点所
在的回路，这样等式两边都含有终结点，可以运用向量维数公理．
［2］ 证明向量垂直的算法 205
证明向量垂直的算法适用于习题中已有两个垂直条件，或是只有一个垂直条件，使用前
推法经过有限几步就能证明出第二个垂直关系．题目要求证明的是存在第三个垂直关系，这
是习题的难点所在．
在向量推理过程，主要用到以下五种形式化的表达式，为叙述方便，称为这五种形式的
表达式分别为： 210
a + b （A）
×a b （B）
×1 2 n(a + a + ...+ a ) b（C）
× 1 2 na (b + b + ...+ b )（D）
2 ...× + × + + ×1 1 2 n na b a b a b （E） 215
( ) ( )×1 2 n 1 2 na + a + ...+ a b + b + ...+ b （F）
n>=1, 在本算法中，取值为 2即可满足需要．
如果（A）型表达式的值为 0，也称为 0值表达式．
两条线段 1 2,l l 互相垂直，用向量来表示分别是a与 b ，这两个向量数量积为 0．即：
1 2 0l l⊥ => ⋅ =a b （G） 220
其逆命题显然也是成立的，即：
1 20 l l⋅ = => ⊥a b （H）
因此，用向量法证明垂直关系的思路就是，根据规则（H），利用已知条件，应用后推
法思想，寻找回路，展开式中各项的乘积，最后验证结果为 0，表明两向量垂直，结束推理．
算法 2：向量垂直算法 225
输入：含垂直关系的几何图形
- 7 -
中国科技论文在线
输出：向量数量积
S1.初始化，将题目中的已知信息向量化表示．构造两个垂直向量的乘积为 B型表达式．
S2.初步扩展表达式，将（B）型表达式扩展为（C）或（D）型表达式．把有一组回路的
向量代换成其回路和的形式，即（B）型表达式；若两个向量回路数量均不为一，则查询回230
路数量为 0的向量，用其和等式将此向量代换为等价的（B）型表达式．至此，（B）型表达
式转换为了（C）或（D）型表达式．
S3.再次扩展表达式，上步结果乘积式中的尚未代换的向量项出现了两次，分别用两组
回路和（A）型表达式代换，展开即为（E）型．这样，上一步的等式化为四项的表达式，在
（E）中，n=4．或是将两个（B）型等式代换其等价的（B）型表达式代替，成为（E）型表235
达式，n=2．
S4.查询 VectorProductList 中的各个乘积项，能否找出其中两项乘积式之值为 0，则
上步结果表达式余下为两个乘积式之和．
S5.判断这两个乘积式之和是否为 0．若为 0，则转 S7；否则，结果不为 0，进行下一步．
S6.代换上述表达式中的（B）型表达式向量，再次形成（E）型表达式．如果余式中两240
向量式为互为逆反项或为 0，进行下一步 S7；否则转入 S5．
S7.结果为 0，表明结论成立，记录本次推理过程 Proof．
S8.结论暂不成立，退出．
证明向量垂直的算法中，需要查询一些乘积式，它们是在习题初始化中，由前推法根据
一些普通的规则而得到，保存在乘积信息库中．通过乘积式的代换和计算，得到两个向量的245
数量积结果为 0，表明这两个向量是垂直的．
［3］ 涉及定比分点的证明算法
有不少的向量题目涉及到了定比分点．定比分点将所在线段分成两段，其长度比值固
定．根据长度比值的不同，常见的有二等分点，即中点，比值为 1；三等分点，比值为 1/2
或 2，四等分点比值为 1/3 或 3，n 等分点即为 1/n或 n． 250
应用定比分点方法解题的核心在于利用等式左边的代数式系数等于等式右边的代数式
系数之和这个特点，构造一个方程式，其解即为所设的定比．利用定比可进行代数式的变换，
从而进行以后的处理．定比分点在解题过程中，如果需要消去某个交点，即可以使用定比分
点的向量形式进行代换，从而消去此点．这也是一种消点方法．根据交点成的线段与公共点
所构成的向量是否有等价表示形式，等式代换可分为两种情况．一种是线段端点与公共点之255
一存在有中点，或都有已知定比分点的情况，这样的向量有显式的等价式；另一种是找不到
等价式，从而代换成另一条与定比分点共线的另外一点，即第二定比分点，利用比例向量的
形式，进行代换．这样，共线上两个向量就可以相互表示．通过进行等式代换，从而创造出
此交点的第二个定比分点表达式．定比分点或是第二定比分点，分其父对象线段成固定比例，
从而得到新的向量比例或线段．在进行定比分点的计算过程中，一般先设其为变量 m，代表260
其固定比值， 0m ≠ ．
算法 3：定比分点算法
输入：含定比分点的几何图形
输出：向量之间的比例
使用定比分点方法进行证明的算法如下： 265
S1.设置图形中的最高约束点，它定义为两条线段的交点，记入 MostPointSet．这样的
- 8 -
中国科技论文在线
最高约束点可能不止一个，它的父对象是相交两条线段的四个端点，记入 MostPointSet．最
高约束点不能是线段的端点．
S2.如果 MostPointSet 为空，转 S12；如果不为空，则依次取出 MostPointSet 中的每
个元素作为当前对象，执行下面的步聚． 270
S3.取出当前最高约束点所在两条线段的四个端点，记入集合 ParentSet．
S4.对 ParentSet 中的四个端点前后错位组合，判断是否能组成两条不平行的向量，且
这两条向量相交于一个公共点，找出这个公共点，记为 CommonPoint．
S5.根据向量的加法，构造第一个定比分点表达式，成为以公共点和交点为端点的向量
的表示形式，如 (1 - )= +OP OA m OB
JJG JJG JJG
． 275
S6.对第一个表达式右边的两个向量进行等价代换，搜索向量乘积信息库，选择含有公
共点 CommonPoint 的等价式进行代换．
S7.整理这个新的表达式，计算各项的系数．取出表达式两侧各个项的系数，构造一个
含有定比 m的方程式 Equation，左边的系数等于右边的系数之和．
S8.解上式方程 Equation，由于只含有一个未知变量，解出 m的值，即为定比值． 280
S9.将 m 代入第一个表达式，得出最高约束点所在向量由其所分的向量比例信息，交点
分所在向量的比与第一个定比分点表达式右边两条向量前的系数对应成反比．
S10.将得到的定比信息进行欧氏几何形式的转化，转化为可能存在的二等分，三等分点，
并以欧氏几何的形式记录下来．
S11.从 MostPointSet 中移除当前 MostPoint, 转 S2． 285
S12.结束．
由以上算法可以看出，运用向量法解平面几何题的方法可以总结为三个步骤：
（1）向量表示,把几何问题中的点、直线、平面和几何关系等元素用向量表示；
（2）向量运算,针对几何问题的特点，调用相关的向量机器证明算法进行向量运算；
（3）回归几何，对向量运算结果作出几何意义上的解释，并保存起来． 290
3 程序实现
根据向量表示的公理体系，本文设计一个具有动态几何作图功能的机器证明软件．这个
软件除了可以完成一般的平面几何作图功能外，主要完成以向量法机器证明为主的推理功
能．本程序可以对一些涉及中点或定比分点的习题做出向量推理．
总体结构 295
向量法机器证明在是遵循前推法的思想指导下进行的．动态几何，向量法推理，可读证
明有机地结合在一起，实现基于向量法的几何机器证明程序系统．
- 9 -
中国科技论文在线
图 1 总体结构图
The frame structure 300
整个程序系统可以分为三个部分：（1）动态几何，包括了动态几何图形的绘制，及图
形数据结构的获取．（2）最主要的部分，是基于向量回路的推理，根据不同的图形特点，
可以进行结论为相等向量，垂直向量或定比分点等关系的推理．（3）可读证明，要生成各
种推理的推理链，然后根据推理链生成附带有图形的可读证明，这种可读证明是基于向量回305
路的．
动态几何
动态几何作图模块，目的在于以作图的形式提供推理初始信息输入．允许用户操作鼠标
进行点线圆多边形等常见图形作图，从而实现信息输入，这是动态几何软件中作图的操作方
式．普通的动态几何作图有两步，第一步是先选择菜单中的子菜单或工具栏相应的按钮，即310
告诉计算机用户接下来要做什么，接着用户用鼠标开始点击操作几何对象，像几何画板[15],
CABRI[16]就是使用了这种操作模式．如果能省略第一步，直接用鼠标就可以作用户想要的
图形，那就表明这种方式具有智能化的特点了．因此，跟踪鼠标，就可能实现人机交互．本
文提出一种智能作图的方式．设计的操作方法为，单击作点，拖动画线，双击作圆．尽量简
化作图操作，计算机主动给出作图目标提示，减轻作图者的操作负担．本系统能够根据鼠标315
的位置探测到当前位置的已有图形，判断用户想要做什么样的图形，并给出提示，释放鼠标，
作图即可瞬间地完成，这就是智能作图．
采用智能作图设计方法，可以减少用户点击和选择的次数，提高作图效率．当然，这有
赖于作图的直觉和对作图位置的判断．如要做一条线段的中点，即可以把鼠标移动到当前线
段上，线段默认显示为当前对象，光标继续移动到线段的中间位置，计算机即可给出提示“中320
点”．此时，松开鼠标，中点即可自动生成．
动态几何作图系统可以保存用户所做的各种几何图形对象，可以分析出各种图形信息和
几何关系，将这种几何信息提供给推理引擎，相当于完成了推理初始信息输入．
推理过程
在推理引擎中，设置推理不动点，以数据进行驱动，对可用的规则进行多轮的调用．每325
- 10 -
中国科技论文在线
次使用规则可得到新的信息，以备以后的规则使用．如果当前循环结束后，数据库的信息数
量没有发生变化，就是达到了推理不动点．即可结束推理，规范地生成命题的证明过程．
图 2 向量法推理流程图
The flow chart of the vector-based reasoning procedure 330
本引擎由以下几部分构成：数据产生器，算法调配器，算法执行器，信息记录器．
数据产生器：主要是完成初始数据收集工作．初始数据由动态几何图形模块进行分析可
得，信息存储在几何信息集中．
算法调配器：由于信息种类的不同，可以适用的算法也不同，由算法调配器来调配当前335
究竟应当调用哪些推理算法．这样，避免无关的算法被调用，减少时间消耗，可以提高执行
的效率．
算法执行器：它调用符合条件的可用算法，根据已知信息进行匹配推理，符合条件则得
出适当形式的结果，并将其送入信息记录器．
信息记录器：负责记录送入信息集中的所有信息，当信息为初始条件时，直接入库；如340
果是推理得到的信息则先检测库内有无此类同样的信息，若没有，则记录入库，如果有，则
舍弃．
证明生成器：对于选定结论中的几何信息，根据推理中保留的原因信息，经过回溯，生
成完整的证明过程．
可读证明 345
本系统中自动推理是由根据前推搜索法设计的推理引擎来实现的．它的一个优点是前推
- 11 -
中国科技论文在线
法是目前机器证明中可读又易被中学教学所接受的证明生成方法[17,18]．所有的向量推理结
果以层次结构树型显示，并且同时以欧氏几何的表示方式显示．图形与证明过程一起显示．如
有必要，则还会附加上几何的表示方式．
自动推理是几何习题证明的核心．几何图形是其输入，几何关系是其输出，几何习题生350
成则是自动证明的高级应用．如果用户想要了解一个几何题目能推理得到哪些的几何信息，
不用自己去考虑详细的证明过程．在点击“自动推理”后，系统可以得到诸多的几何关系信
息，这些几何关系根据分类，显示在一棵信息树上．用户可以随意点击查看，每个具体的信
息项打开后，显示的是其成立的条件信息．
本系统运用推理引擎，从一些几何图形中推理出很多非平凡的几何信息，有的是以欧氏355
几何信息的形式显示，有的则是由于平面向量推理而得出的结论信息，这些信息大多是一些
多项式等式的运算过程．为了查看结论得到的过程，有必要将生成的过程记录下来，方便查
看，供生成证明使用．
推理信息库中的这些几何信息与人交互十分方便，通过鼠标点击查看几何信息树就可以
动态效果来看看这些信息及其证明过程．证明过程可以存储成连续图片，所指信息对象区域360
马上显式呈现等，方便中学教学．
尽管我们还没有充足的支持推理的定理，我们已经了发现这种方法在实践中工作得很
好．某个特定类型的习题可能会失败，但每天使用它工作得很好．
4 算例与结果
应用本文的程序，可以对一些用平常方法非常难做的习题做出向量形式的自动推理，速365
度很快，下面的例题可以在 1-2 秒内得到结果．由于在图形显示系统中的局限，程序中用一
对“[ ]”表示向量．如，向量 AB
JJJG
，在图形中表示为[AB]．为了方便以后的使用，所有的证
明过程可以按用户的要求，输入到一个文本文件中，永久保存．
例 1.(井田问题)如图 3 上，已知 J 、 G为平面内任意四边形一组对边 AD、BC 的中点，
E 、F 三等分 AB，I 、H 三等分DC．求证：JG被 EI 、FH 三等分且 EI 、FH 又被 JG 平370
分．
图 3 井田问题
Geometry problem Jingtian
375
- 12 -
中国科技论文在线
图 4 井田问题的证明结果
The proof results of geometry problem Jingtian
根据题目条件作图完成后，点击“自动推理”即可迅速完成向量机器证明，如图 4． 380
由左侧展开的信息树中可以看出，[ ] = [ ]HL LF 说明 L是 FH 的中点．[ ]=*[ ]LG JL 说明
L三等分GL ．[ ]=*[ ]KJ GK ，说明K 三等分 JG．[ ]=[ ]EK KI ，说明K 是 EI 的中点．
使用传统的几何解题方法来解此题是相当不容易的，需要添加多条辅助线．
例 2.(矩形外一点的垂直) 如图 5，设 ABCD为矩形，点 E 为平面上一点，连接 AE、BE ，
作CF AE⊥ ，DG BE⊥ ，CF 和DG交于点H ，求证：EH AB⊥ ．（第 17 届全俄数学奥林385
匹克，1991 年）
图 5 第 17届全俄数学奥林匹克竞赛题
One of the 17th All-Russian Mathematical Olympiad problems
390
在完成几何图形后,我们执行了向量推理功能，如图 6 所示．
上面 [ ] [ ] 0EH AB⋅ = 的证明过程中，有些等式代换用到了普通欧氏几何引理的结
果．[ ] [ ] 0EH AB⋅ = 说明 EH AB⊥ ．
这道习题还可以使用坐标证法来解：建立坐标系，设 E 在 DC 的射影为O ，设 (0,0)O ，
( , ), (1, )A a b B b , (1, 0), ( , 0)C D a ， (0, ),E e ( , )H x y ，需证 0x = ． 395
由CF AE⊥ 得 0CH AE⋅ =
JJG JJG
，即 ( 1, ) ( , ) 0x y a e b− ⋅ − − = ，即 ( 1) ( ) 0a x y e b− − + − = ．
由 DG BE⊥ 得 0DH BE⋅ =
JJG JG
，即 ( , ) ( 1, ) 0x a y e b− ⋅ − − = ，即 ( ) ( ) 0x a y e b− − + − = ．
将所得两式相减得 (1 ) 0a x− = ，若 1a = 则矩形退化，所以只能是 0x = ．
相比较而言，还是向量法推理的结果比较简洁．
400
- 13 -
中国科技论文在线
图 6 图 5 的证明结果
The proof results for the geometry problem in
5 总结 405
向量法用于机器证明有实际的应用价值．向量法在中国已经写入了中学课本，是对欧氏
几何学的扩充．由于其良好的可读生，发展向量的机器证明新方法，对中学教学的是积极的
补充，为认识和理解向量提供了实践机会．向量法的学习增加了对数形结合的理解，在必要
的时候可以增加坐标运算进行辅助证明．它是数形结合的最佳研究实例．
向量法的研究还可以扩展到更多的习题类型，并可以深入到立体几何，使用回路，结合410
内积与外积，也能够解决大量问题．
如何把代数法，消点法和搜索法结合起来，组成可持续发展的具有人机交互功能的计算
机几何自动求解系统是更有意义的研究方向[19]，这将是我们下一步的研究目标．
[参考文献] (References) 415
[1] Wu Wen-Tsün．On the decision problem and the mechanization of theorem-proving in elementary
geometry[J]．Scientia Sinica．1978, 21:159-172
[2] 吴文俊.几何定理机器证明的基本原理[M].北京：科学出版社,1984
[3] Chou S. C.，Gao X. S.，Zhang J. Z.．Automated generation of readable proofs with geometric invariants .1.
Multiple and shortest proof generation[J]．Journal of Automated Reasoning．1996，17(3):325-347 420
[4] Zhang .，Chou S. C.，Gao X. S.．Automated production of traditional proofs for theorems in Euclidean
geometry-I. the hilbert intersection point theorems[J]．Annals of Mathematics and Artifical Intelligence．1995，
13:109-137
[5] Arthur J. Nevins．Plane Geometry Theorem Proving Using Forward Chaining[J]．Artifical Ingelligence．1974，
6(1):303-338 425
[6] S. C. Chou，X. S. Gao，J. Z. Zhang．A deductive database approach to automated geometry theorem proving
and discovering[J]．Journal of Automated Reasoning．2000，25(3):219-246
[7] 张景中，高小山，周咸青. 基于前推法的几何信息搜索系统[J]，计算机学报，1996，19(10): 721-727
[8] 江建国，张景中，王晓京．多项式等式型几何定理的可读证明[J]．计算机学报，，31 (2):207-213
[9] Chou ., Gao X,S, Zhang .．Automated geometry theorem proving by vector calculation[A]．Proceedings 430
of the 1993 international symposium on Symbolic and algebraic computation[C]．1993，ACM New York, NY,
- 14 -
中国科技论文在线
USA(SIGSAM: ACM Special Interest Group on Symbolic and Algebraic Manipulation):284 - 291XIAO J Z, LEI
B, WANG C Q. Reclamation on building waste produced from Wenchuan Earthquake[A]. XIAO J Z. The first
discussion forum of study on RAC[C]. Shanghai: Tongji University Press, 2008. J Z, LEI B, WANG
C Q. Reclamation on building waste produced from Wenchuan Earthquake[A]. XIAO J Z. The first discussion 435
forum of study on RAC[C]. Shanghai: Tongji University Press, 2008. 64-65.
[10] 张景中，李永彬．几何定理机器证明三十年[J]．系统科学与数学．2009，29(9):1155-1168
[11] S. Stifter．Geometry theorem proving in vector spaces by means of Grobner bases．the 1993 International
Symposium on Symbolic and Algebraic Computation，1993，1993:301-310
[12] . Yaglom．Geometric ,1955-1956:358 440
[13] 钟秀琴,符红光,佘莉,黄斌.基于本体的几何学知识获取及知识表示[J].计算机学报, 2010, 33(1) : 167-174
[14] H. Gelernter．Realization of a geometry-theorem proving machine[M]．Computers & thought,New York:
McGraw-Hill．1963:134-152
[15] 张景中，彭翕成．绕来绕去的向量法[M]．北京：科学出版社，2010
[16] N. Jaekiw．The Geometer's Sketchpad[Z]．KeyCurrieulumPress,1990 445
[17] J Laborde，Franck Bellemain．Cabri-GeometryⅡ[Z]．Texas Instruments，1993
[18] Z. Ye，S. C. Chou，X. S. Gao．Visually Dynamic Presentation of Proofs in Plane Geometry Part 1. Basic
Features and the Manual Input Method[J}．Journal of Automated Reasoning．2010，45(3):213-241
[19] Z. Ye，S. C. Chou，X. S. Gao．Visually dynamic presentation of proofs in Plane geometry part 2. automated
generation of visually dynamic presentations with the Full-Angle method and the deductive database 450
method[J]．Journal of Automated Reasoning．2010，45(3):243-266
