本体推理在几何定理机器证明中的应用  

Application of Ontology Reasoning in Mechanical Geometry Theorem Proving

作　　者：李晓霞[1] 陈强[1] 

机构地区：[1]广东第二师范学院计算机科学系,广东广州510310

出　　处：《计算机技术与发展》2013年第9期78-81,共4页Computer Technology and Development

基　　金：2012年广东省高等院校学科建设专项资金项目(2012KJCX0079);2011年东莞市现代信息服务业发展专项资金竞争性项目(DG201101)

摘　　要：文中阐述了平面几何定理机器证明的基本原理及方法,针对几何定理机器证明过程中可读证明的产生,及推理信息快速增长的问题,提出了一种基于本体推理的几何定理机器证明方法。通过具体案例,描述了以Protégér软件为工具,基于WordNet重用的领域本体半自动构建方法,构建几何本体模型的过程,并结合Prolog规则进行双向推理。结果表明将本体引入几何定理机器证明是可行的,且本体推理脱离了代数形式,使得推理过程更接近自然语言的描述,同时推理效率更高。The principle and method of the plane geometry theorem machine proving are expounded in this paper. According to the prob- lem of readability and information rapid growth in geometry theorem proving, a proving method based on ontology reasoning is proposed. Through the concrete case, the process of constructing geometric ontology models are described, which are constructed by using the Prot6g6 tool and the method of domain ontology semi-automatic construction based on WordNet reuse, then combine the Prolog rules to reasoning. The results show the geometry theorem proving based on ontology reasoning is feasible, and the ontology reasoning is divorced from the algebraic form, which makes the reasoning process are more closer to natural language, and the efficiency more higher.

关 键 词：定理机器证明 本体模型 规则 推理 领域属性 

分 类 号：TP31[自动化与计算机技术—计算机软件与理论]