主页期刊介绍编委会编辑部服务介绍道德声明在线审稿编委办公English
     
在线出版
各期目录
纸质出版
分辑系列
论文检索
论文排行
综述文章
专刊文章
美文分享
各期封面
E-mail Alerts
RSS
旧版入口
中国科学院软件研究所
  
投稿指南 问题解答 下载区 收费标准 在线投稿
徐贵红,张 健.语义网的一阶逻辑推理技术支持.软件学报,2008,19(12):3091-3099
语义网的一阶逻辑推理技术支持
First-Order Logic Reasoning Support for the Semantic Web
投稿时间:2007-08-27  修订日期:2007-10-26
DOI:
中文关键词:  语义网推理  一阶逻辑  描述逻辑  本体  可满足性
英文关键词:semantic Web reasoning  first-order logic  description logic  ontology  satisfiability
基金项目:Supported by the National Natural Science Foundation of China under Grant No.60673044 (国家自然科学基金)
作者单位
徐贵红 中国科学院 软件研究所 计算机科学国家重点实验室,北京 100190
中国科学院 研究生院,北京 100049 
张 健 中国科学院 软件研究所 计算机科学国家重点实验室,北京 100190 
摘要点击次数: 5986
全文下载次数: 8507
中文摘要:
      研究了一阶逻辑推理工具对语义网的推理支持.语义网的关键推理问题可以化为公式的可满足性判定问题.一阶逻辑的自动定理证明器可以证明不可满足性,而有限模型查找器为可满足的公式在有限域内构造模型.提出在语义网的推理中,同时使用定理证明器和有限模型查找器.实验结果表明,这样可以解决描述逻辑工具的不足,并可以弥补定理证明器对可满足的公式推理的不完备性.
英文摘要:
      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.
HTML  下载PDF全文  查看/发表评论  下载PDF阅读器
 

京公网安备 11040202500064号

主办单位:中国科学院软件研究所 中国计算机学会 京ICP备05046678号-4
编辑部电话:+86-10-62562563 E-mail: jos@iscas.ac.cn
Copyright 中国科学院软件研究所《软件学报》版权所有 All Rights Reserved
本刊全文数据库版权所有,未经许可,不得转载,本刊保留追究法律责任的权利