基于本体与Prolog的平面几何定理证明

钟秀琴，符红光，丁盘苹

(电子科技大学计算机科学与工程学院 成都 610054)

定理机器证明(automated theorem proving，ATP)就是把证明定理的一般知识和规则以适当的形式存储到计算机中，让计算机通过运算自动地证明定理，因此也叫自动推理，它既是人工智能研究的重要课题，又属知识工程的范畴[1]。

几何定理机器证明方向在自动推理的研究中占有重要的地位。一方面，我国在该方向上具有领先优势；另一方面，该方向有清晰明确的应用背景，近年来在机器证明领域的研究十分活跃，值得关注。

到目前为止，几何定理机器证明的主要方法有代数方法、几何不变量方法和基于演绎数据库(或基于规则的搜索)等方法。

文献[2]提出了一个证明等式型初等几何定理的新的代数方法，用它可在微型计算机上花几分钟甚至几秒钟证明很不简单的定理，该方法即吴方法。几何定理机器证明的代数方法以吴方法为代表，吴方法的出现被公认为是机器证明领域里程碑式的突破。后来又出现了如国外的Grobner基方法[3]，国内的Dixon消元法、例证法等代数方法。但它们仅能够判断几何命题的成立与否，且证明过程十分复杂，需要进行大量的数值计算和符号计算，与传统几何证明的简洁明了大相径庭，人们很难读懂这些方法生成的证明过程。

文献[4]以面积法作为基础，提出消点算法是几何不变量方法的标志性算法。几何不变量的方法虽然实现了一大类几何定理的机器可读证明，但是该方法得到的证明过程常常不符合人们的思维习惯。

基于几何推理数据库或基于规则的方法[5]，是根据几何命题所给的条件、已知的公理、定理及公式等推理规则，通过大量的试验匹配的方法进行证明。文献[6]提出了一个基于前推模式的几何信息搜索系统(GISS)，成功地证明了161个非平凡的几何命题。但该方法所表现的信息十分丰富，即中间过程的几何信息呈指数增长，成为该方法研究的瓶颈。

如何生成让人容易读懂的几何证明过程？该问题成为研究者们面临的又一个严峻挑战。本文从理论研究入手，旨在找到一种脱离代数的几何定理证明方法，且使其具有接近自然语言的描述，以摆脱只有专家才能读懂定理机器证明的尴尬处境。

本体是当前的研究热点，本体可以表示领域内概念与概念之间的关系。到目前为止，本体在很多方面得到了应用，如WordNet、Enterprise ontology[7]和Gene ontology[8]等都是典型的本体应用。进一步，本体可作为信息检索系统的核心，通过构造形式化的领域本体，将知识表示和知识处理引入互联网信息处理，为互联网上半结构化数据和关系数据库提供统一的语义模型。因此，本文在前人研究与实践的基础上，将本体引入平面几何定理机器证明，进一步拓展本体模型的应用。

本文首先对平面几何定理证明所需的基础理论进行分析，然后以具体实例说明领域本体模型的构建过程，以及如何将本体推理与规则推理结合进行几何定理机器证明，最后给出整个问题求解的过程和所得到的结论。

1 平面几何本体模型的构建

1.1 本体相关概念

本体作为一种能在语义和知识层次上描述信息系统的概念模型的建模工具，被提出后迅速成为信息系统与人工智能领域的研究热点。“知识本体(ontology)是共享概念模型的明确的形式化的规范说明”[9]。该定义包含4层含义。

1) 概念化：通过抽象出客观世界中一些现象的相关概念而得到的模型，其含义独立于具体的环境状态。

2) 明确：所使用的概念及使用这些概念的约束都有明确(显式)的定义。

3) 形式化：知识本体是计算机可读的。

4) 共享：知识本体中所体现的是共同认可的知识，所反映的是相关领域中公认的概念集，所针对的是团体而不是个体。

通过构建本体能够精确规范某个领域的概念，明确定义机器可以处理的概念及概念之间的关系，大大提高知识搜索、知识重用、知识共享的效率。

当前，本体构建工具主要包括Ontolingua Server、Ontosaurus、WebOnto、OntoEdit、Protégé等[10]，本文研究采用由斯坦福大学医学信息研究组开发的Protégé构建本体。1) Protégé是一个免费和开源的本体编辑平台，可以使用RDF、RDFS、OWL等本体描述语言编辑和修改本体；2) Protégé可以直接对类、实例和属性等进行编辑操作，用户不必掌握具体的本体表示语言；3) 用户可根据自己的应用需求开发新插件和定制已有插件；4) Protégé支持中文[10]。

本体描述语言OWL(web ontology language)是W 3C推荐的语义互联网中本体描述语言的标准。按照对本体功能的支持分为OWL Lite、OWL DL和OWL Full。其中OWL DL是基于描述逻辑(description logics)[11]的，它支持那些需要最强表达能力的推理系统的用户，且推理系统能够保证计算的完全性(computational completeness，即所有的结论都能够保证被计算出来)和可判定性(decidability，即所有的计算都在有限的时间内完成)[12]。因此，本文选择OWL DL作为本体模型描述语言。

本体模型的构建方法很多，有领域专家手工构建的领域本体，有自动或半自动构建的本体。本文采用的是基于WordNet重用的领域本体半自动构建方法[13]。首先通过WordNet接口提取基本的几何元素，以及这些元素的上位、下位、兄妹关系和同义词等关系，然后用Protégé编辑领域本体，并根据几何定理证明的具体要求，修改或添加一些必要的属性扩充领域本体，存储为.ow l文件。

1.2 平面几何本体模型

本体模型主要由如下几部分组成。

1) 类：一个类是一类个体的集合。一个领域中的最基本概念应分别对应于各个分类层次树的根。OWL中的所有个体都是类ow l:Thing的成员，主要包括rdfs:subClassOf、ow l:equivalentClass等关系。平面几何定理证明中的基本类包含点类、线类、角类、圆类、多边形类等。基于WordNet重用的领域本体半自动构建方法构建的多边形的分类关系如图1所示，其中长方形和矩形是等价类的关系。

图1 类的构建示意图

2) 属性：属性是断言关于类成员的一般事实以及关于个体的具体事实的依据，一个属性是一个二元关系。基本属性主要包括ObjectProperty、DatatypeProperty、Domain、TransitiveProperty、SymmetricProperty、FunctionalProperty、InverseOf、Range、HasValue等。此外，在平面几何定理证明领域，还需要添加一些领域属性，部分领域属性如表1所示。

表1 领域部分属性列表

如图2所示，虚线上方表示构建的是具有长度属性的线段类，属性类型是数据属性。一个类可具有多个属性。

3) 个体：类的成员是范畴中的一个个体。类仅是一个名称和一些描述某集合内个体的属性，而个体是该集合的成员。type表示一个RDF属性(RDF property)，用于关联一个个体和它所属的类。

图2 属性构建示意图

如图2所示，虚线下方为属性构建实例。已知个体“AB”和个体“2”之间具有“长度”属性，则可推理出“AB是线段”“2是长度值”。相反地，若已知“BC是线段”“2是长度值”，则可推理出“BC”与“2”之间具有“长度”属性。图中实线箭头表示已知条件，虚线箭头表示由本体推理出的结论。

1.3 本体模型构建思路

本文采用的是基于WordNet重用的领域本体半自动构建方法，并将几何模型中的基本元素作为本体模型中的类；将基本元素的性质及其关系作为本体模型类的属性；将几何定理作为联系整个本体模型的规则；然后将几何例题作为本体模型的个体进行实例化。

2 基于Prolog规则的推理

描述逻辑可以执行本体推理，但描述逻辑对陈述性知识的表达能力不足，不能提供关系间的组合推理。如已知属性关系hasFather(Tom,Jack)和关系hasSpouse(Jack,Rose)，却无法推理出hasMother(Tom,Rose)，即不能通过描述逻辑的推理。而大多数的问题求解都涉及复杂关系间的组合推理，因此需合理地将规则推理与本体推理相结合。

规则可遵循多种语法，常用的有SPARQL、Prolog等，本文使用Prolog进行规则描述。如线段相等，可用规则描述如下：

可以通过查询语句(select(?x ?y)(线段相等?x ?y))得到实例模型中所有相等的线段，由此可以判断线段AB和线段BC相等。该方法可应用于平面几何定理证明。

3 平面几何案例设计及实现

例：已知任意四边形ABCD，点E、F、G、H分别是线段AB、BC、CD、DA的中点，如图3所示。证明四边形EFGH是平行四边形。

考虑到目前的推理系统有前推系统(根据已知事实及相关的性质定理进行前向推理)、后推系统(从目标及相关的定义、判定定理进行后向推理)和将二者结合的双向推理系统。本文中采用的是双向推理的方法。

图3 实例示意图

表2 已知对象类的相关性质定理

1) 前推法分析。分析本例的已知条件，有点类、线段类、三角形类、四边形类、中点类等，每个类有与其相关的性质、定理及与其对应的本体模型。表2所示为已知对象类的相关性质、定理，表中列出了相应定理的结论。

三角形类的部分本体模型如图4所示，该图描述了与本例相关的三角形的属性、线段的属性、点的属性及部分实例等。三角形有边、有顶点的属性是从多边形继承来的，即由rdfs:subClassOf推理得出的。

进一步，由对表2的分析可以看出，与平行关系和线段等量关系相关的定理只有三角形中位线定理，而三角形中位线的本体模型描述如图5的虚线上方部分所示，虚线下方部分为三角形的中位线所具有性质的定理，可描述三角形的中位线所具有的属性。三角形的中位线的Prolog规则描述如下：

图4 三角形部分本体模型图

根据上述Prolog规则，可由建立的本体模型推理出f表示三角形，d表示三角形的中位线，z表示三角形的底边。通过三角形的中位线性质的定理可得出三角形的中位线与三角形的底边的关系为“三角形的中位线平行于第3边(底边)，且等于第3边(底边)的一半”，因此可建立三角形的中位线的平行关系属性和线段等量关系属性(等于1/2)，且两个属性都具有传递性(transitivity)。因此，根据上述Prolog规则和传递性的约束属性，可由前推法得到相关结论，如表3所示。

图5 三角形的中位线模型及其性质定理

表3 本体和规则推理结果

2) 后推法分析。分析本例中的结论为“四边形是平行四边形”，需用到相关的判定定理如表4所示。基于本体的平行四边形后推法模型可描述为如图6所示的过程。

表4 “四边形是平行四边形”结论的判定定理

四边形类的本体描述从略，其属性还包括对边、邻边等。如图6所示，要证明四边形为平行四边形，可通过平行四边形的定义和平行四边形的判定定理1～4等进行证明。定义平行四边形，需定义其两组对边分别平行。因此其相应的Prolog规则描述如下：

由表3、表4和该平行四边形的Prolog规则，即可推理出该四边形EFGH为平行四边形，从而基于本体和Prolog规则的推理描述结束。

图6 基于本体的后推法

最后，将本体实例模型保存为.ow l文件。支持ow l的推理机很多，如RACER、FaCT、Pellet、Jena等。本文采用基于Jena和Prolog的A llegro Graph(AG)数据库进行推理，因为AG数据库提供了外部调用的API，而且AG数据库存取数据的方式是三元组形式，与上述的模型描述一致，存取的形式接近自然语言。将上述本体实例模型和Prolog规则导入AG数据库，则得到平行四边形EFGH。至此，本文例题的平面几何定理证明圆满完成。

4 结 论

本文通过对本体理论、本体建模、基于Prolog的推理等方面的研究和对例题证明过程的设计与实现，验证了基于本体和Prolog规则进行平面几何定理证明的可行性。虽然尚不能确定这是一种快速的方法，但是完全有理由相信这是一种有前途的机器证明方法。

首先，基于本体的方法很好地体现了概念及其关系之间的层次性和结构性，以及关系之间的约束性，基于Prolog规则的方法很好地解决了复杂的关系间的组合推理。将两种方式结合，可有效地规避问题求解中的多次判断问题。其次，可将问题分析和推理同步进行，证明的效率可得到较大的提高。再次，基于本体和Prolog规则的几何定理证明是接近自然语言的证明方法，是定理机器证明的新思路，且本体模型的构建及其推理还可进一步应用于数据挖掘，为行业用户提供精确的信息检索、智能推送等服务。

[1] 赵子都. 定理机器证明[J]. 自然辩证法研究, 1994, 10(5):46-50.

ZHAO Zi-du. The machine demonstration of theorems[J].Studies in Dialectics of Nature, 1994, 10(5): 46-50.

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

WU Wen-jun. on the decision problem and the mechanization of theorem in elementary geometry[J].Science in China, Ser A, 1977, 20(6): 507-516.

[3] BOSE N K. Multidimensional systems theory[M]. [S.l.].Reidel Publishing Company, 1985: 184-232.

[4] ZHANG Jin-zhong, ZHOU Xian-qing, GAO Xiao-shan.Automated production of traditional proofs for theorems in euclidean geometry[J]. Annals of Mathematics and Arti fi cial Intelligence, 1995, 13: 109.

[5] FU Hong-guang, ZHONG Xiu-qin, ZENG Zhen-bing.Automated and readable simplification of trigonometric expressions[J]. Mathematical and Computer Modeling, 2006,44(11-12): 1169-1177.

[6] ZHOU Xian-qing, Gao Xiao-shan, Zhang Jin-zhong. A deductive database approach to automated geometry theorem proving and discovering[J]. Journal of Automated Reasoning, 2000, 25(3):219-246.

[7] REN Nan, LIU Jian-yi, GE Shi-lun. Enterpise ontology for supporting M IS design[C]//Proceedings of the Seventh International Conference on Information and Management Sciences. Urumchi, China: China Academic Journal Electronic Publishing House, 2008: 77-80.

[8] LI Li-sha, ZHANG Ning-bo, LI Shao. Ranking effects of candidate drugs on biological process by integrating network analysis and Gene ontology[J]. Chinese Science Bulletin, 2010, 55(26): 2974-2980.

[9] 王长霞, 李冠宇, 陈布伟. 语义网本体构建工具现状及发展趋势研究[J]. 计算机与现代化, 2009, 缺卷号(7): 26-31.

WANG Chang-xia, LI Guan-yu, CHEN Bu-wei, Study on present situation and development trend of ontology construction tools[J]. Computer and Odernization, 2009, 缺卷号(7): 26-31.

[10] STUDER R, BENJAM INS V R, FENSEL D. Know ledge engineering, principles and methods[J]. Data & Know ledge Engineering, 1998, 25(1): 161-197.

[11] BAADER F, CALVANESE D, DEBORAH L. et al. The description logic handbook: Theory, imple mentation and application[M]. Cambridge: Cambridge University Press,2002.

[12] M ICHAEL K S. OWL Web Ontology Language Guide[DB/OL]. [2011-01-12]. http://www.w3.org/TR/2004/ REC-ow l-guide-20040210.

[13] 赵天忠, 苗壮, 张亚飞. 基于WordNet重用的领域本体构建方法[J]. 系统仿真学报, 2007, 19(19): 4583-4586.

ZHAO Tian-zhong, M IAO Zhuang, ZHUANG Ya-fei.Reusing WordNet for building domain ontology[J]. Journal of System Simulation, 2007, 19(19): 4583-4586.

编 辑 蒋 晓