质点几何定理证明的机器实现

苏贺靓 江建国 高 华

（辽宁师范大学数学学院，辽宁 大连 116029）

0 引言

几何定理机器证明是自动推理领域内的一个热门课题.1977年,吴文俊先生提出的“吴法”[1-4]使得几何定理机器证明的研究取得了重大进展.通常,几何定理机器证明方法可分为三大类：代数法,人工智能法和几何不变量法.代数法的优点是证明效率高,缺点是可读性差；人工智能法虽然可读性好但效率低、不完备；几何不变量法的可读性介于代数法和人工智能法之间,证明效率与代数法也在伯仲之间.

质点几何使用了比几何不变量更抽象的对象——质点,作为基本几何元素.莫绍揆先生在文献[5]中系统地阐述了质点几何的理论和方法.质点几何支持对点直接进行线性运算,在处理仿射几何问题时较方便,为发展出一种可读性更好、效率更高的几何定理机器证明方法提供了可操作的依据.

邹宇等人采用质点几何作为模型,在质点几何的基础上,通过调用函数搜索质点在点表中的位置,从而调用向量表中相应位置数组进行运算,建立了能处理希尔伯特交点类命题的仿射几何机器证明算法MPM,发展了基于几何点的可读机器证明方法[6-7].

本文是在参考文献[6]的工作基础上,针对其只是对质点所一一对应的数组做运算而非质点本身消点运算的问题,作了纯质点代数运算.消点过程比邹宇的数组法简明.每一步消点过程都有相应的质点关系式输出,每个质点关系式又对应于相应的几何信息,消点过程结束,质点关系也就都明确了,再利用待定系数法而非数组计算法来判定结论语句是否成立,使得每一个步骤的几何意义都非常明确.建立了能处理构造型几何定理的证明器MMP,并通过Matlab语言实现机器证明.

1 质点几何

1.1 预备知识

质点几何使用了质点作为基本的几何元素.莫绍揆先生在《质点几何学》一书中系统地阐述了质点几何的理论和方法.质点几何支持对点直接进行线性运算,在处理仿射几何问题时较方便,为发展出可读性更好、效率更高的几何定理机器证明方法提供了依据.

质点是一个既有位置又有质量的基本几何元素,其质量为一个实数,可正可负以及零.质点几何的创新之处在于质点均有质量.当质量为非零实数时,质点表示一个点,或者其对应的位置；当质量为零时,质点表示一个矢量,或者其对应的方向.

通常,用小写希腊字母 ω,ξ,ψ,…表示质点,用大写英文字母 A,B,C,…表示平面上的点,用小写英文字母a,b,c,…表示实数,将位于点P处质量为m（m≠0）的质点记作mP.在不引起混淆的情况下,将位于点P质量为1的单位质点1P也简记成P.质点几何中常用的基本定理和运算律主要有：

1）实数r与质点ω的数乘决定唯一质点rω.

2）两质点 ω1,ω2的和决定唯一质点 ω1+ω2.

3）若P1,P2,P3是质点平面的一组基,则该平面上的任一点P都可以由这组基点线性表示,即必存在3个和为1的实数k1,k2和k3,使得P=4）点P在直线AB上当且仅当存在一个实数k使得P=kA+(1-k)B.5）A,B,C三点共线当且仅当存在实数m和n,使得mA+nB+(1-mn)C=0.

6）直线AB平行直线CD当且仅当存在一个实数k使得A-B=k(C-D).

7）对任意质点ω1,ω2和ω3,任意实数a和b,有如下运算律：

1.2 构造型质点几何命题

质点法不是利用尺规作要证定理的几何图形,而是使用一种叫做“构图语句”作图步骤按题中的已知条件一步一步地向图中引入新点,直到作出几何图形中全部的点为止.

构造型几何命题的前提能用有限的构图语句序列C0,C1,…,Cn描述,这里的构图语句C0必须是初始构图语句,其他构图语句即后继构图语句中出现的质点,除了新引进的质点外,其余的都必须是前面的构图语句所引进过的质点.

质点法使用引入点的“构图语句”来描述要证定理的前提,本文主要构图语句有以下几条：

2 证明器的设计

2.1 证明器的架构

MMP证明器主要由模块Mmprove、Loadgs和 Cinter组成.

当要利用该证明器证明几何定理时,首先将要证明的几何命题转化成相应的构图语句存储在文本文件中,Matlab通过调用模块Mmprove中的Loadgs读取该文本文件,并利用模块Loadgs将构图语句转化成相应的消点公式,来实现消点过程,其中求两直线交点的消点公式还需要交点模块Cinter的辅助,依据质点几何的基本原理和法则完成证明器的实现.

2.2 Loadgs模块

2.2.1 几何命题的输入

证明器MMP的模块Mmprove顺次阅读构图语句,调用相应的消点公式生成,显示质点关系式,几何定理结论以结论等式的形式输出

Loadgs模块将文本文件中的含有待定系数x的结论质点等式（EQ标识所在的行）读入到符号变量eq中,将要验证的待定系数的值（XV标识所在的行）读入到符号变量xv中.xv的取值为“exit”,表示xv的值只要存在就可以.若xv的值是数或符号表达式,则表示结论质点等式中的待定系数取此值才成立,否则不成立.

Loadgs模块将初始构图语句FreePo int s(A,B,C)引入的3个点A、B和C存储到基点列表base.构图语句序列中的其它后续语句所引入的点都可直接或间接地用前面已引入的点线性表示出来.将这些质点关系式称为构图语句所引入点的消点公式.Loadgs模块根据质点几何中的有相关的基本命题,可以直接求出下列构图语句所引入点的消点公式：

DPDP(X,A,B,λ)所引入点X的消点公式：

Translation(X,A,B,C)所引入点X的消点公式：

上述消点公式中的a和b都是表示实数的符号变量,λ是实数或为表示实数的符号变量,X1,X2和X3是质点平面的一组基点.

2.2.2 消点公式

在质点平面上任作三个线性无关的单位质点X,Y和Z.将这三个单位质点选定为其所在的质点平面的一组基后,那么构图语句序列中的其它语句所作的点都可直接或间接地用这组基线性表示出来,

这些质点公式分别叫做构图语句所作点X的消点公式.具体情况如下：

这里,a和b都是取值为实数的符号变量,λ、u0和v0是取值为实数的符号常量,这些值决定了点X在平面上的确切位置.

2.3 Cinter模块

在上述消点公式中只有消点公式(epf6)需要复杂计算得到.下面给出求消点公式(epf6)的Cinter模块,该模块使用前面构图语句所作点的消点公式列表epfs和3个基点,求两直线AB和CD交点X的消点公式(epf6)中的u0和v0.

将消点公式列表epfs中新引进的质点Xi(i=1,…,n)依次存储到初始值为空的元胞数组po int s中,建立方程eq=uA+(1-u)B-vC-(1-v)D.依次检验元胞数组po int s中质点Xi(i=1,…,n)是否为eq中的符号常量,若Xj是的话,则用对应的消点公式epfsj替换掉Xj,继续循环,直至eq没有质点Xi(i=1,…,n)出现,此时eq只由基点的关系式表示.设基点对应系数分别用E1,E2和E3表示,令Ei=0(i=1,2,3),解此方程组得u0和v0的值.

3 Matlab实验

我们用Matlab编写程序实现了MMP证明器,下面是利用该证明器解题的例子.

（高斯线定理）设A、B、C、D是平面上的四点,E是AB、CD的交点,F 是 AC、BD 的交点,P、Q、R 分别是 AD、BC、EF 的中点,则 P、Q、R 三点共线.

在文本文件中输入：

下面是Matlab程序给出的实现过程：

消点过程：

消点结束后,令EQ=0,写成f1(x)A+f2(x)B+f3(x)C=0形式.

这里,系数fi(a,b)都是a和b的线性表达式,其中i=1,2,3.因A,B和C线性无关,可得

这是一个含有3个一元一次方程的超定线性方程组,由所作几何图形的合理性可知该方程组的解是存在的.解一元一次方程f1(x)=0,求出其解,分别带入方程f2(x)=0和f3(x)=0中,经验算f2(x0)=0和f3(x0)=0成立,则原方程组有且仅有唯一解.

待定系数x值存在,P,Q,R三点共线.

4 结论

本文在质点几何基本定理和法则的基础上,总结归纳质点法解题的特点,建立了能处理仿射几何定理机器证明的消点过程,并利用待定系数的方法而非数组计算法来判定定理结论是否成立,使得每一个质点关系式的几何意义都非常明确．本文基于质点法处理几何点本身,易于扩展和融合,形成了具有完全性的消点过程．由于可以对点直接进行运算,质点法的消点过程比面积法或向量法简明,并通过Matlab程序实现.

本文的质点法是继面积法之后又一个能对构造性几何命题生成可读证明的完全的消点过程．运行结果显示,本文的方法不仅效率高,程序自动生成的证明条理简明清晰、语义简洁易懂、几何意义明确、储存信息丰富,可读性强．此外,由于可以对点直接进行运算,质点法的算法和编程比面积法或向量法都要简明.本文基于点的可读机器证明的研究为扩展和融合其他已有的可读证明方法提供了基础,也为几何的研究提供了一个新的工具．

随着计算机技术的发展和机器证明方法的不断改进,几何定理可读证明的研究成果为研制的智能几何软件如几何专家、超级画板等提供了更广阔的平台.

［1］吴文俊.初等几何判定问题与机械化证明[J].中国科学(A),1977,6：507-516.

［2］Wu W T.On the decision problem and the mechanization of theorem-proving in elementary geometry[J].Scientia Sinica.1978,21：159-172.

［3］Wu W T.Mechanical theorem proving in geometries：Basic principles[M].Springer,New York,1994.

［4］Wu W T.Mathematics Mechanization[M].Science Press,Kluwer,2000.

［5］莫绍揆.质点几何学[M]．重庆：重庆出版社,1992.

［6］邹宇.几何代数基础与质点几何的可读机器证明[D].广州：广州大学,2010.

［7］邹宇,郑焕,张景中.仿射质点几何的可读机器证明[J].计算机应用,2010,30(7)：1989-1912.