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