| 摘要: |
| 研究了一阶逻辑推理工具对语义网的推理支持.语义网的关键推理问题可以化为公式的可满足性判定问题.一阶逻辑的自动定理证明器可以证明不可满足性,而有限模型查找器为可满足的公式在有限域内构造模型.提出在语义网的推理中,同时使用定理证明器和有限模型查找器.实验结果表明,这样可以解决描述逻辑工具的不足,并可以弥补定理证明器对可满足的公式推理的不完备性. |
| 关键词: 语义网推理 一阶逻辑 描述逻辑 本体 可满足性 |
| DOI： |
| 分类号: |
| 基金项目:Supported by the National Natural Science Foundation of China under Grant No.60673044 (国家自然科学基金) |
|
| First-Order Logic Reasoning Support for the Semantic Web |
|
XU Gui-Hong,ZHANG Jian
|
| Abstract: |
| 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. |
| Key words: semantic Web reasoning first-order logic description logic ontology satisfiability |
