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

被引：42

作者：

徐贵红 ^{[1
,2
]}

张健 ^{[1
]}

机构：

[1] 中国科学院软件研究所计算机科学国家重点实验室

[2] 中国科学院研究生院

来源：

软件学报 | 2008年 / 12期

关键词：

语义网推理; 一阶逻辑; 描述逻辑; 本体; 可满足性;

D O I：

暂无

中图分类号：

TP393.09 [];

学科分类号：

摘要：

研究了一阶逻辑推理工具对语义网的推理支持.语义网的关键推理问题可以化为公式的可满足性判定问题.一阶逻辑的自动定理证明器可以证明不可满足性,而有限模型查找器为可满足的公式在有限域内构造模型.提出在语义网的推理中,同时使用定理证明器和有限模型查找器.实验结果表明,这样可以解决描述逻辑工具的不足,并可以弥补定理证明器对可满足的公式推理的不完备性.

引用

页码：3091 / 3099

页数：9