应用本体和AllegroGraph实现几何定理证明-论文.pdf

《应用本体和AllegroGraph实现几何定理证明-论文.pdf》由会员上传分享，免费在线阅读，更多相关内容在行业资料-天天文库。

1、第24卷第8期计算机技术与发展Vo1．24No．82014年8月COMPUTERTECHNOLOGYANDDEVELOPMENTAug．2014应用本体和AllegroGraph实现几何定理证明吴店年，李云清(江西师范大学计算机信息工程学院，江西南昌330022)摘要：由于传统的定理机器证明方法是基于规则的，使得定理证明出现几何信息增长迅猛，推理和计算效率低以及过程可读性差等问题。针对以上情况，提出了基于本体和AllegroGraph的几何定理证明方法。该方法通过本体构建几何定理命题模型，然后采用Prolog规则描述语言对几何

2、定理性质进行描述，同时通过分析本体模型和规则描述的对应关系，提出定理规则半自动生成方法。最后以AllegroGraph(AG)图形数据库的推理机制为基础，完成几何定理证明。实验结果表明，将本体和AllegroGraph推理机应用于几何定理证明领域可以摆脱以往几何定理证明代数化问题，几何证明过程容易理解，同时合理地控制了信息的增长，支持定理可持续证明。关键词：本体推理；AllegroGraph(AG)；Prolog规则；几何；定理证明中图分类号：TF301文献标识码：A文章编号：1673—629X(2014)08-0089-05

3、doi：10．3969／j．issn．1673—629x．2014．08．021RealizationofGeometryTheoremProvingwithOntologyandAllegroGraphWUDian—nian．LIYun—qing(SchoolofComputerandInformationEngineering，JiangxiNormalUniversity，Nanchang330022，China)Abstract：Astraditionaltheoremmechanicalprovingmethodsa

4、rebasedontherules，makingthegeometrytheoremprovingoccursrapidgrowth，reasoningandcalculationsineficient，andprocesspoorreadability．Fortheabovecases，adesignmethodofthegeometrytheoremprovingbasedonontologyandAllegroGraphispresented．Thismethodconstructsthemodelofgeometric

5、theorempropositionthroughontology，andthenusesthePrologruledescriptionlanguagetodescribethenatureofgeometrytheorems．Atthesametime，throughthea—nalysisofthecorrespondencebetweenontologymodelandrulesdescribed，proposesemi-automaticmethodforthegenerationoftheoremrules．Fin

6、allycompletegeometrictheoremprovingbasedonAllegroGraph(AG)，takingthereasoningmechanismofgraphicdatabaseasthefoundation．Theexperimenta／resultsshowthattheontologyandtheAllegroGraphinferenceengineusedinthefieldofgeometrytheo-remprovingcangetridofgeometrytheoremprovinga

7、lgebraic，geometricproofprocessiseasytounderstand，reasonablycontrolthegrowthofinformationandsupportsustainableprovetheorem．Keywords：ontologyreasoning；AllegroGraph(AG)；Prologrules；geometry；theoremprovingO引言照人们正常思想上的几何命题思路去证明；同时会产在人工智能和知识工程领域，定理机器证明是指生大量的几何信息，导致信息过于膨胀等

8、问题。把定理证明过程在计算机上通过自动实现符号形式化随着web技术的发展和Internet的广泛应用，语的技术进行演绎推理。截止目前，主要通过代数法⋯、义Web本体理论日益成熟。由于本体语义表达能力几何不变量方法和基于几何推理数据库方法等强，能对特定领域知识进行专业性定义，因