质点几何定理机器证明的研究进展

doi:10.12677/AAM.2018.712173

期刊菜单

质点几何定理机器证明的研究进展
Research Progress of Automated Particle Geometry Theorems Proving

DOI: 10.12677/AAM.2018.712173, PDF, HTML, XML, 下载: 1,238 浏览: 4,204
作者: 胡晓璐, 江建国, 张媛：辽宁师范大学数学学院，辽宁大连
关键词: 自动推理；质点几何；质点法；质点消去法；Automated Reasoning； Particle Geometry； Particle Method； Particle Elimination Method

摘要: 质点几何定理机器证明是当前几何定理机器证明领域内的一个研究热点。本文介绍了质点几何的基本理论。综述了质点几何定理机器证明近年来取得的一些比较显著的进展。比较了质点法和质点消去法这两种证明方法的优缺点。最后，展望了这个方向上需要进一步研究的问题。

Abstract: Nowadays, the automated particle geometry theorems proving is a new topic in automated rea-soning field. In this paper, we introduced firstly foundations of particle geometry theory, and then summarized the state of art of this topic in recent years. In addition, we compared two new auto-mated particle geometry theorems proving methods: the particle method and the particle elimi-nation method. Finally, we prospected some further research problems in this topic.

文章引用：胡晓璐, 江建国, 张媛. 质点几何定理机器证明的研究进展[J]. 应用数学进展, 2018, 7(12): 1490-1499. https://doi.org/10.12677/AAM.2018.712173

1. 引言

能否用机械的方法证明数学定理曾是许多伟大数学家的一个美妙设想。为此，笛卡尔、莱布尼茨、希尔伯特等数学家们均付出过努力。最早莱布尼茨提出过机器证明的设想。希尔伯特等人创立并发展的数学逻辑为机器证明提供了强有力的工具，使设想有了明确的数学形式。计算机的问世更为设想的实现提供了物质基础。

1948年，塔斯基提出了一个可用机械化方法判定初等几何问题的定理 [1] 。1956年，Newell和Simon等人编写的一个程序成功地证明了《数学原理》中的38条定理。1959年，王浩实现了一个程序，此程序仅用了9分钟就证明了《数学原理》中有关命题演算的全部定理。该成果在世界上引起了轰动。1976年，K.Appel等人在计算机上成功地证明了著名的四色定理。该项工作成功推动机器证明的发展。

1977年，吴文俊提出了“吴法” [2] ，给机器证明的分支几何定理证明研究带来了勃勃生机。周咸青基于吴法实现了一个证明器 [3] ，再次推动了几何定理机器证明的发展。在吴法的激励下，数学家们又陆续提出不同的代数方法，如Grobner基法 [4] [5] 、单点列证法 [6] 、数值并行法 [7] 等。

在代数法的启发下，许多数学家致力于研究几何定理的可读证明。1992年，周咸青、高小山、张景中等人提出面积法，使几何定理的可读证明取得重大突破 [8] 。在面积法的启发下，数学家们又陆续提出了全角法 [9] 、向量法 [10] 、复数法 [11] 和幅角法 [12] 等。此类方法后被统称为几何不变量法 [13] 或消点法 [14] 。

是否能用一些比上述几何不变量更加抽象的几何对象，如点、直线等，来发展一种可读性好且效率高的证明方法呢？近年来，邹宇、张景中等人根据质点几何的基本原理提出了一种将“质点”作为运算对象的证明方法——质点法 [15] [16] [17] 。同面积法相比，质点法可以直接消点而不一定用几何不变量。质点法的主要特点是不仅能直接对质点进行运算而且借助消点思想。消点思想与传统的解题思想截然不同。当遇到较难的几何问题时，传统的解题思想是如何添加辅助线，而消点思想是如何消去结论中的约束点，从而使结论变得越来越简单更加容易验证。

数学家莱布尼茨曾提过可对几何中的点进行代数运算的设想。数学家格拉斯曼曾做过许多质点几何这方面的基础理论研究工作。数学家吴文俊和张景中都介绍过质点几何中的应用 [18] [19] [20] 。另外，数学家莫绍揆先生还详细的介绍了质点几何的理论基础 [21] 。

本文余下内容主要分为三部分。第2部分主要介绍质点几何的基础知识。第3部分主要综述质点几何定理可读证明器的研究现状。第4部分主要展望质点几何定理证明器的研究未来。

2. 质点几何

2.1. 基础知识

在物理学中，当某物体不考虑其形状、大小等因素时，将它看成具有质量的点，称为质点。质点几何中“质点”与欧式几何中“点”不同。质点不仅表示空间中的一个位置而且具有一个质量。如果质点 $α$ 所在的空间位置为P点，其质量为m时，通常将质点 $α$ 记为 $α = m P$ 。特别地，当 $m = 1$ 时，称为单位质点，记为1P，一般简记成P。下面几个本文用到的质点几何的定义和定理。

定义1：设质点集 $G = {m P | m \in R, P \in V}$ ，实数域R，欧式空间V。在G上定义了加法运算+： $G \times G \to G$ 和数乘运算 $\cdot$ ： $R \times G \to G$ ，并且对G中任意的 $α$ ， $β$ ， $γ$ ，任意的实数 $k_{1}$ 和 $k_{2}$ ，满足如下的运算律：

1) $α + β = β + α$

2) $(α + β) + γ = α + (β + γ)$

3) $α + 0 = α$

4) $α + (- α) = 0$

5) $1 α = α$

6) $(k_{1} + k_{2}) α = k_{1} α + k_{2} α$

7) $k_{1} (α + β) = k_{1} α + k_{1} β$

8) $k_{1} (k_{2} α) = (k_{1} k_{2}) α$

称 $(G, +, \cdot)$ 为质点空间。

定义2：质点减法运算定义： $α - β = α + (- β)$ 。

定义3：如果有不全为0的实数 $k {}_{1}, k_{2}, \dots, k_{n}$ ，使 $k_{1} α_{1} + k_{2} α_{2} + \dots + k_{n} α_{n} = 0$ ，则质点 $α {}_{1}, α_{2}, \dots, α_{n}$ 是线性相关的。如果只有当 $k {}_{1}= k_{2} = \dots = k_{n} = 0$ 时才成立，则质点 $α {}_{1}, α_{2}, \dots, α_{n}$ 是线性无关的。

公理1：对质点空间 $(G, +, \cdot)$ 任意四个质点 $α_{1}$ ， $α_{2}$ ， $α_{3}$ ， $α_{4}$ ，恒有四个不全为0的实数 $k_{1}$ ， $k_{2}$ ， $k_{3}$ ， $k_{4}$ ，使得 $k_{1} α_{1} + k_{2} α_{2} + k_{3} α_{3} + k_{4} α_{4} \neq 0$ 。

公理2：对质点空间 $(G, +, \cdot)$ 任意五个质点 $α_{1}$ ， $α_{2}$ ， $α_{3}$ ， $α_{4}$ ， $α_{5}$ ，恒有五个不全为0的实数 $k_{1}$ ， $k_{2}$ ， $k_{3}$ ， $k_{4}$ ， $k_{5}$ ，使得 $k_{1} α_{1} + k_{2} α_{2} + k_{3} α_{3} + k_{4} α_{4} + k_{5} α_{5} = 0$ 。

下文将由公理1和公理2对定义的质点空间 $(G, +, \cdot)$ 称为一个质点平面。易知，质点平面上的任意一质点都可由平面上的三个线性无关的质点线性表示。可将质点平面上任意三个线性无关的质点看成是该平面的一组基点。欧式几何中的几何性质与质点几何中的质点关系式有一一对应关系(表1)。

Table 1. Correspondence between properties of Euclidean geometric objects and relational expressions of particles

表1. 质点关系式与欧式几何性质之间的对应关系

定义4：设G是质点空间，R是实数域。在其上定义二次容积运算d： $G \times G \to R$ ，并满足如下条件：对所有的 $α, β, γ \in G$ ， $k_{1}, k_{2} \in R$ ，

1) $d (α, β) = - d (β, α)$

2) $d (α, α) = 0$

3) $d (k_{1} α, k_{2} β) = (k_{1} k_{2}) d (α, β)$

4) $d (α, β + γ) = d (α, β) + d (α, γ)$

5) $d (α + β, γ) = d (α, γ) + d (β, γ)$

定理1：两质点 $α$ ， $β$ 的二次容积计算决定唯一的 $d (α, β)$ 。

定义5：设G是质点空间，R是实数域。在其上定义三次容积运算s： $G \times G \times G \to R$ ，并满足如下条件：对所有的 $α, β, γ, λ \in G$ ， $k_{1}, k_{2}, k_{3} \in R$ ，

1) $s (α, β, γ) = s (β, γ, α) = s (γ, α, β) = - s (α, γ, β) = - s (β, α, γ) = - s (γ, β, α)$

2) $s (α, β, α) = s (β, α, α) = s (α, α, β) = 0$

3) $s (k_{1} α, k_{2} β, k_{3} γ) = (k_{1} k_{2} k_{3}) s (α, β, γ)$

4) $s (α + λ, β, γ) = s (α, β, γ) + s (λ, β, γ)$

5) $s (α, β + λ, γ) = s (α, β, γ) + s (α, λ, γ)$

6) $s (α, β, γ + λ) = s (α, β, γ) + s (α, β, λ)$

从定义可见，质点几何中的二次容积和三次容积这两个质点几何量，分别与欧式几何中线段的长度比和三角形的面积比这两个欧式几何量相类似。二次容积比和三次容积比分别与线段的长度比和三角形的面积比具有一一对应关系(表2)。

Table 2. Correspondence between ratios of Euclidean geometric quantities and ratios of particle volume

表2. 质点容积比与欧式几何量比之间的对应关系

2.2. 构造型质点几何命题

将几何定理中的已知条件可以用一系列的构图语句序列表述，结论可以用质点表达式来表述的几何命题，称为构造型质点几何命题。

几何命题中至少会涉及一组基点，因此将表述基点的构图语句 $BasePoints (A, B, C)$ 作为构图语句序列的第一条。构图序列中其余构图语句依据几何命题的已知条件依次表述其它新点，直到该命题中的全部点均表述出来为止。常用的质点几何图形的构图语句主要有：

1) $BasePoints (A, B, C)$ ：在平面上任取不共线的三点A，B，C。

2) $FreePoint (P)$ ：在平面上任作一点P。

3) $PointOnline (P, A, B)$ ：在直线AB上任取一点P。

4) $Midpoint (P, A, B)$ ：作线段AB的中点P。

5) $DPDP (P, A, B, k)$ ：作线段AB的定比分点P，使得 $\vec{A P} : \vec{P B} = k$ 。

6) $Translation (P, A, B, C)$ ：将点 $A$ 按向量 $\vec{B C}$ 平移到点P。

7) $Intersection (P, A, B, C, D)$ ：作两直线AB和 $C D$ 的交点P。

构造型质点几何命题的结论通常是一个能用质点表达式表述的几何性质。例如，证P是AB的中点、A，B，C三点共线等。构图语句序列的结论语句一般分为三种形式：一是检验函数的形式，如 $ifcolinear (A, B, C)$ ：检验A，B，C是否共线。二是线性质点关系式的形式，如 $A = x B + (1 - x) C$ ：表示A，B，C三点共线。若其中的x值存在，则证明成功，否则证明失败。三是容积型质点表达式的形式，如 $s (A, B, C)$ ：表示A，B，C的三次容积计算。若三次容积为0，则三点共线，否则三点不共线。

例1：如图1所示，A、B、C、D是平面上的4个点，E是AB和CD的交点，是AC和BD的交点，P、Q、R分别是AD、BC、EF的中点。求证：P、Q、R三点共线。

Figure 1. Example 1

图1. 例1

这是一个典型的构造型质点几何命题，命题的前提可用如下的构图语句序列描述：

$BasePoints (A, B, C)$

$F r e e P o i n t (D)$

$I n t e r s e c t i o n (E, A, B, C, D)$

$I n t e r s e c t i o n (F, A, C, B, D)$

$M i d p o i n t (P, A, D)$

$M i d p o i n t (Q, B, C)$

$M i d p o i n t (R, E, F)$

而命题的结论语句可分为三种表述形式：1) 检验函数： $i f c o l i n e a r (P, Q, R)$ 。2) 线性质点关系式： $P - x Q - (1 - x) R$ 。3) 容积型质点表达式： $s (P, Q, R)$ 。

3. 研究现状

3.1. 质点法

质点法的解题方法是先消点再验证，其过程与解线性方程组的代入和消元相类似。邹宇、张景中等人提出了一种使用质点几何基本原理证明几何定理方法——质点法，并基于该方法实现了一个几何定理证明器MPM [15] 。该证明器的算法由构图数集CF，解题目标集AF和控制器MMC组成。对于上述的每个构图语句，在构图数集CF中均有一个构图函数可将构图语句转化为质点关系式并进行消点运算。解题目标集AF中包含不同的基本求值函数。如 $ifcolinear (A, B, C)$ ：检验A，B，C是否共线并输出对应结论。控制器MMC先依次读入构图语句，并调用构图数集CF中的构图函数生成基点列表及质点关系式列表，最后调用解题目标集AF中的求值函数检验并输出结论。

由构造型质点几何命题的特点知，基点将作为初始构图语句，不妨设为A，B，C。其余构图语句所引入的新点P均可由基点线性表出，即 $P = k_{1} A + k_{2} B + k_{3} C (k_{1} + k_{2} + k_{3} = 1)$ 。因此每个点P在内部均可用唯一的和为1的三元数组 $(k_{1}, k_{2}, k_{3})$ 表示。而点A，B，C对应数组分别为 $(1, 0, 0)$ ， $(0, 1, 0)$ ， $(0, 0, 1)$ 。由此，过程中对点的运算就等价于对点所对数组的运算，结论中求质点的线性关系等价于求各数组之间的线性关系。

在MPM算法中，用三个全局变量 $p n t s$ ， $v a r l i s t$ 和 $c o o r d l i s t$ 来分别记录问题中出现点的个数、引进点的有序集合、引进点所对三元数组的有序集合。初始设置 $p n t s = 0$ ， $v a r l i s t$ 和 $c o o r d l i s t$ 均为空表；初始语句引入一组基点A，B，C后， $p n t s = 3$ ， $v a r l i s t = {A, B, C}$ ， $c o o r d l i s t = {(1, 0, 0), (0, 1, 0), (0, 0, 1)}$ ；此后，每引入一个新点 $p n t s \to p n t s + 1$ ，把新引入的点和其对应的数组分别存到 $v a r l i s t$ 和 $c o o r d l i s t$ 的第 $p n t s + 1$ 的位置上，并输出相应的质点关系式。最后，每个检验函数先搜索并记录所需验证点在 $v a r l i s t$ 中的位置，并调用 $c o o r d l i s t$ 中相应位置的数组进行约定的计算，求出其线性关系并输出结论。

对上节例1的几何定理，证明器MPM输出的证明：

1) 基点：

A B C

2) 质点关系式：

$D = a A + b B + (1 - a - b) C$

$(a + b) E = D - (1 - a - b) C = a A + b B$

$(1 - b) F = D - b B = a A + (1 - a - b) C$

$2 P = A + D = (a + 1) A + b B + (1 - a - b) C$

$2 Q = B + C$

$2 R = E + F = \frac{a (a + 1)}{(a + b) (1 - b)} A + \frac{b}{a + b} B + \frac{1 - a - b}{1 - b} C$

3) 结论等式的计算判定：

$\frac{S_{P Q R}}{S_{A B C}} = | \begin{matrix} a + 1 & b & 1 - a - b \\ \frac{a (a + 1)}{(a + b) (1 - b)} & \frac{b}{a + b} & \frac{1 - a - b}{1 - b} \\ 0 & 1 & 1 \end{matrix} | = 0$

因此，输出结论“P、Q、R三点共线”。

由上例可知，证明器MPM在证明过程中利用质点对应的三元组进行约定的计算，从而求出所蕴涵的目标质点间关系式。但该证明器所求过程不够直接，而且几何意义难以理解。此外，证明器MPM没有一个判定结论的通用方法，而是根据结论的不同，从解题目标集AF中选取相应的函数来验证结论。由此增加了证明器实现的难度和复杂性。

3.2. 质点消去法

3.2.1. 线性质点消去法

2015年，为了进一步的提高质点法的可读性和证明效率，苏靓贺等人提出了一种新的几何定理方法——线性质点消去法，并基于此方法实现了一款几何定理证明器MPP [22] 。

线性质点消去法的基本思路是：第一步，证明器MPP读取第一条构图语句 $BasePoints (A, B, C)$ ，生成基点列表 ${A, B, C}$ ；第二步，依次读取其它的每条构图语句，生成新点及新点对应的消点公式；第三步，读取结论等式eq，并对结论等式eq进行消点运算。消点顺序按照新点引入的相反顺序循环消点。消点方法是当结论等式eq中存在新点时，将新点替换成其相应的消点公式，逐依排查直到结论等式eq中只剩下基点时结束；第四步，分别取该结论等式三个基点的系数构成一个方程组，并对该方程组求解，若方程组有解，则定理成立，否则不是定理。

对上节例1的几何定理，证明器MPP输出的证明：

1) 基点：

A B C

2) 消点公式：

$D = a A + b B + (1 - a - b) C$

$E = \frac{a}{a + b} A + \frac{1 - a}{a + b} B$

$F = \frac{- a}{b - 1} A + \frac{a + b - 1}{b - 1} C$

$P = \frac{1}{2} A + \frac{1}{2} D$

$Q = \frac{1}{2} B + \frac{1}{2} C$

$R = \frac{1}{2} E + \frac{1}{2} F$

3) 结论等式eq左端的消点过程：

eq： $P - x Q - (1 - x) R$

$= \frac{x - 1}{2} E + \frac{x - 1}{2} F + P + (- x) Q$ (消点R)

$= \frac{- x}{2} B + \frac{- x}{2} C + \frac{x - 1}{2} E + \frac{x - 1}{2} F + P$ (消点Q)

$= \frac{1}{2} A - \frac{x}{2} B - \frac{x}{2} C + \frac{1}{2} D + \frac{x - 1}{2} E + \frac{x - 1}{2} F$ (消点P)

$= (\frac{1}{2} - (\frac{a}{b - 1}) \frac{x - 1}{2}) A - \frac{x}{2} B + \frac{1}{2} D + \frac{x - 1}{2} E + (- \frac{x}{2} + (\frac{a}{b - 1} + 1) \frac{x - 1}{2}) C$ (消点F)

$= (\frac{1}{2} + (\frac{a}{a + b} - \frac{a}{b - 1}) \frac{x - 1}{2}) A + (\frac{- x}{2} + (\frac{b}{a + b}) \frac{x - 1}{2}) B + (\frac{- x}{2} + (\frac{a}{b - 1} + 1) \frac{x - 1}{2}) C + \frac{1}{2} D$ (消点E)

$\begin{array}{l} = (\frac{a + 1}{2} + (\frac{a}{a + b} - \frac{a}{b - 1}) \frac{x - 1}{2}) A + (\frac{- x + b}{2} + (\frac{- b}{a + b}) \frac{x - 1}{2}) B \\ + (\frac{- x - a - b + 1}{2} + (\frac{a + b - 1}{b - 1}) \frac{x - 1}{2}) C \end{array}$ (消点D)

$= 0$

4) 使用待定系数法判定结论等式eq：

${\begin{cases} \frac{a + 1}{2} + (\frac{a}{a + b} - \frac{a}{b - 1}) \frac{x - 1}{2} = 0 \\ \frac{- x + b}{2} - \frac{- b}{a + b} \frac{x - 1}{2} = 0 \\ \frac{- x - a - b + 1}{2} + \frac{a + b - 1}{b - 1} \frac{x - 1}{2} = 0 \end{cases}$

解线性方程组得：

$x = b - \frac{b}{a} + \frac{b^{2}}{a}$

因方程组的解存在，故结论等式eq成立，即：P、Q、R三点共线。

同证明器MPM相比，证明器MPP主要有3个特点：1) 基点没有坐标，引入的新点也不需要计算出坐标，生成的机器证明同样不依赖于坐标。2) 证明器MPP为每个新引入的点(除基点)都计算出一个消点公式，而不是一个含有新点的质点关系式。3) 证明器MPP一步一步地给出了结论等式eq的消点过程，而不是调用解题目标函数集中的求值函数进行约束求解。

3.2.2. 容积型质点消去法

现有的质点几何定理证明器都不能证明涉及到面积、长度等几何量的定理。为增强证明器的解题能力，李辉等人提出了一种能证明该类型定理的方法——容积型质点消去法，并基于此法实现了一款证明器PGP [23] 。在计算机上作了十几个容积型质点几何定理的证明实验，结果表明该证明器不仅能自动生成简短、可读性好的证明，而且证明范围更广。

容积型质点消去法的基本思想是：第一步和第二步同线性质点消去法相同，不再复述；第三步，读取结论等式eq，对结论等式eq的类型进行判断，一种是线性质点关系式，消点运算与上法相同。另一种是容积型质点表达式，消点运算中的消点顺序及方法同线性质点消去法相同。不同在于消点运算中的化简，容积型质点消去法的化简规则是依据容积的定义将含有两个以上相同质点的项直接消去；第四步，输出结论等式eq的系数为命题结论。

例2：如图2所示，在三角形ABC中，分别取AB、BC、AC的三等分点D、E、F，连接CD、AE、BF分别交于点P、M、N。求证： $S_{Δ A B C} : S_{Δ P M N} = 7$ 。

Figure 2. Example 2

图2. 例2

证明器PGP输出的证明：

$A$

$B$

$C$

$D = (2 * A) / 3 + B / 3$

$E = (2 * B) / 3 + C / 3$

$F = (2 * C) / 3 + A / 3$

$P = (4 * A) / 7 + (3 * E) / 7$

$M = A / 7 + (6 * E) / 7$

$N = (3 * D) / 7 + (4 * C) / 7$

EQ： $s (P, M, N)$

$= (4 * s (P, M, C)) / 7 + (3 * s (P, M, D)) / 7$ (消点N)

$= (4 * s (P, A, C)) / 49 + (3 * s (P, A, D)) / 49 + (24 * s (P, E, C)) / 49 + (18 * s (P, E, D)) / 49$ (消点M)

$= (96 * s (A, E, C)) / 343 + (12 * s (E, A, C)) / 343 + (72 * s (A, E, D)) / 343 + (9 * s (E, A, D)) / 343$ (消点P)

$\begin{array}{l} = (64 * s (A, B, C)) / 343 + (8 * s (B, A, C)) / 343 + (48 * s (A, B, D)) / 343 \\ + (6 * s (B, A, D)) / 343 + (24 * s (A, C, D)) / 343 + (3 * s (C, A, D)) / 343 \end{array}$ (消点E)

$= (64 * s (A, B, C)) / 343 + (8 * s (A, C, B)) / 343 + (8 * s (B, A, C)) / 343 + s (C, A, B) / 343$ (消点D)

$= s (A, B, C) / 7$

因此，结论成立，即 $S_{Δ A B C} : S_{Δ P M N} = 7$ 。

证明器PGP是在证明器MPP的基础上进行了改进和推广，一是在算法中能直接化简容积型质点表达式，二是消点的过程中根据结论不同调用不同的化简方式。当结论等式为容积型质点表达式时，直接对结论等式进行循环消点，消点结束将直接得出命题结论，无需再用待定系数法进行求解。

4. 研究展望

回顾近几年的质点几何定理证明器发现证明范围仍然有限。主要原因有两方面，一个是质点几何的知识体系还不够完善，一个是质点几何定理证明器的证明能力有限。

质点几何的思想源于古希腊的阿基米德。许多数学家都先后研究过质点几何的理论、方法和思想等。但目前质点几何的知识体系还不够完善。例如，证明器目前仅能证明长度比和面积比，却无法证明长度和面积。原因是质点几何中未涉及到长度和面积的理论知识，即质点几何中没有相关的定义或原理。因此，若想扩大质点几何定理证明器的证明范围，应该进一步完善质点几何的知识体系。

质点几何定理证明器的证明范围有限，其另一个原因是目前证明器所实现的质点法和质点消去法中均未涉及角度、垂直等几何不变量的基本定理。所以现有的证明器不能证明涉及该类几何不变量的定理。下一步工作增强证明器这方面的能力，最好使其也能证明射影几何、仿射几何、度量几何等几何中的定理。另外，目前证明器实现的方法仅能证明等式型的定理。若可以将现有的证明方法推广到不等式的机器证明上，是值得思考的研究方向。

接下来的工作不仅要扩大证明器的证明范围，而且要提高证明器的证明效率。因此，下一步工作可尝试将现有的消点方法推广到消线、消面、消圆等，或综合运用消点法和其他几何不变量法。从而进一步提高证明器的证明效率。

近年来，定理机器证明的应用价值越来越大。例如，张景中等人将证明器MPM整合到一个处理几何类问题的平台SGARP中 [24] [25] ，使SGARP能更好地满足用户需求。因此，进一步工作可以将几何定理证明器的思想、方法和成果等推广应用到数学教育软件中。但现有的理论和算法所给出的证明过程，一般与数学课本上的证明过程有很大的不同，解题的方法也超过了学生所掌握的知识范围。所以，对于实现出可以应用到中学数学教育中的证明器，仍然是一项具有挑战性的任务。

5. 结束语

质点几何定理机器证明作为机器证明的重要分支已成为数学家们重点研究方向。本文从机器证明出发，着重分析了质点几何定理证明器的研究进展，并比较了质点法和质点消去法的优缺点。由证明实验可得，证明器不仅效率越来越高，而且自动生成的证明过程可读性越来越好。但是质点几何证明器的证明能力仍然有限。因此，下一步工作依然是增强证明器的证明能力，使其证明范围不断扩大。

参考文献

[1]	Tarski, A. (1948) A Decision Method for Elementary Algebra and Geometry. The RAND Corporation Press, Santa Monica.
[2]	吴文俊. 初等几何判定问题与机械化证明[J]. 中国科学, A辑, 1977(6): 507-516.
[3]	Chou, S. (1984) Proving Elementary Geometry Theorems Using Wu’s Algorithm. In: Bledsoe, W. and Loveland, D., Eds., Au-tomated Theorem Proving: After 25 Years, AMS Contemporary Mathematics Series, 29, 243-286.
[4]	Buchberger, B., Collins, G. and Kutzler, B. (1995) Algebraic Methods for Geometric Reasoning. Annual Review of Computer Sciences, 3, 85-119.
[5]	Kutzler, B. and Stifter, S. (1986) On the Application of Buchberger’s Algorithm to Automated Geometry Theorem Proving. Journal of Symbolic Computation, 2, 389-397. https://doi.org/10.1016/S0747-7171(86)80006-2
[6]	Hong, J. (1986) Can Geometry be Proved by an Example? Scientia Sinica, 29, 824-834.
[7]	Zhang, J. and Yang, L. (1989) Principles of Parallel Numerical Method and Sin-gle-Instance Method of Mechanical Theorem Proving. Mathematics in Practice and Theory, 1, 34-43.
[8]	Zhang, J.Z., Chou, S.C. and Gao, X.S. (1995) Automated Production of Traditional Proofs for Theorems in Euclidean Geometry, I. The Hilbert Intersection Point Theorems. Annals of Mathematics and Artificial Intelligence, 13, 109-137. https://doi.org/10.1007/BF01531326
[9]	Chou, S.C., Gao, X.S. and Zhang, J.Z. (1996) Automated Generation of Readable Proofs with Geometric Invariants, II: Theorem Proving with Full-Angles. Journal of Automated Reasoning, 17, 349-370. https://doi.org/10.1007/BF00283134
[10]	Chou, S., Gao, X. and Zhang, J. (1993) Mechanical Geometry Theorem Proving by Vector Calculation. Proceedings of International Symposium on Symbolic and Algebraic Computation, ACM Press, New York, 284-291.
[11]	Chou, S., Gao, X. and Zhang, J. (1994) Machine Proofs in Geometry: Automated Production of Readable Proofs for Geometry Theorems. World Scientific, Singapore. https://doi.org/10.1142/2196
[12]	Yang, L., Gao, X. and Chou, S. (1997) Automated Production of Readable Proofs for Theorems in Non-Euclidean Geometries. Automated Deduction in Geometry, LNCS 1360, Springer-Verlag, 171-188. https://doi.org/10.1007/BFb0022725
[13]	Chou, S.C., Gao, X.S. and Zhang, J.Z. (1996) Automated Generation of Readable Proofs with Geometric Invariants-I: Multiple and Shortest Proof Generation. Journal of Automated Reasoning, 17, 325-347. https://doi.org/10.1007/BF00283133
[14]	Zhang, J.Z. (2000) Points Elimination Methods for Geometric Problem Solving. Mathematics Mechanization and Applications, Academic Press, London, 175-202. https://doi.org/10.1016/B978-012734760-8/50008-9
[15]	邹宇, 郑焕, 张景中. 仿射质点几何的可读机器证明[J]. 计算机应用, 2010, 30(7): 1989-1912.
[16]	邹宇. 几何代数基础与质点几何的可读机器明[D]: [博士学位论文]. 广州: 广州大学, 2010.
[17]	Zou, Y. and Zhang, J. (2010) Automated Generation of Readable Proofs for Constructive Geometry Statements with the Mass Point Method. In: Schreck, P., Narboux, J. and Richter-Gebert, J., Eds., ADG 2010, LNAI 6877, 221-258.
[18]	吴文俊. 力学在几何中的一些应用[M]. 北京: 中国青年出版社, 1962.
[19]	张景中, 邹宇. 从“两点如何相加”谈起(上) [J]. 湖南教育, 2012, 6(2): 27-30.
[20]	张景中, 邹宇. 从“两点如何相加”谈起(下) [J]. 湖南教育, 2012, 6(2): 27-30.
[21]	莫绍揆. 质点几何学[M]. 重庆: 重庆出版社, 1992.
[22]	江建国, 苏贺靓, 高华. 质点几何定理证明的机器实现[J]. 科技视界, 2015(15): 96-97.
[23]	李辉. 质点几何定理的机器证明[D]: [硕士学位论文]. 大连: 辽宁师范大学, 2017.
[24]	张景中, 张传军, 郑焕, 等. SGARP中符号计算模块的实现及其应用[J]. 计算机研究与发展, 2014, 51(6): 1341-1351.
[25]	张传军, 邹宇, 郑焕, 等. 质点法在SGARP中的新发现[J]. 数学的实践与认识, 2014, 51(6): 302-311.

为你推荐

友情链接