语义网的一阶逻辑推理技术支持  

First-Order Logic Reasoning Support for the Semantic Web

作　　者：徐贵红[1,2] 张健[1] 

机构地区：[1]中国科学院软件研究所计算机科学国家重点实验室,北京100190 [2]中国科学院研究生院,北京100049

出　　处：《软件学报》2008年第12期3091-3099,共9页Journal of Software

基　　金：国家自然科学基金No.60673044~~

摘　　要：研究了一阶逻辑推理工具对语义网的推理支持.语义网的关键推理问题可以化为公式的可满足性判定问题.一阶逻辑的自动定理证明器可以证明不可满足性,而有限模型查找器为可满足的公式在有限域内构造模型.提出在语义网的推理中,同时使用定理证明器和有限模型查找器.实验结果表明,这样可以解决描述逻辑工具的不足,并可以弥补定理证明器对可满足的公式推理的不完备性.This paper investigates reasoning support for the semantic Web based on the first-order logic. The key reasoning tasks of the semantic Web can be reduced to deciding the satisfiability of formulas. The first-order logic theorem prover is efficient and complete for unsatisfiability, while finite model searcher finds models for satisfiable formula. This paper proposes to use a theorem prover and a finite model searcher concurrently in the semantic Web reasoning. The experiments show that the method can make up the deficiencies of the description logic reasoner and complement the theorem prover for satisfiable formulas.

关 键 词：语义网推理 一阶逻辑 描述逻辑 本体 可满足性 

分 类 号：TP301[自动化与计算机技术—计算机系统结构]