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

Application of Ontology Reasoning in Mechanical Geometry Theorem Proving

文中阐述了平面几何定理机器证明的基本原理及方法,针对几何定理机器证明过程中可读证明的产生,及推理信息快速增长的问题,提出了一种基于本体推理的几何定理机器证明方法。通过具体案例,描述了以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.