微信服务号

微信订阅号

2025年4月1日 18:25 星期二
首页 > 过刊浏览>2011年第22卷第7期 >1524-1537. DOI:10.3724/SP.J.1001.2011.03869
PDF HTML阅读 XML下载 导出引用 引用提醒
可判定的时序动态描述逻辑
作者:
基金项目:

国家自然科学基金(60903079, 60775035, 60963010, 60803033); 国家高技术研究发展计划(863)(2007AA01Z132); 国家重点基础研究发展计划(973)(2007CB311004); 广西自然科学基金(0832006Z)


Decidable Temporal Dynamic Description Logic
Author:
  • 摘要
    • | |
  • 访问统计
    • |
  • 参考文献 [19]
    • |
  • 相似文献 [20]
    • |
  • 引证文献
    • | |
  • 文章评论
    摘要:

    动态描述逻辑DDL(dynamic description logic)提供了一种基于描述逻辑的动作理论,适用于语义Web 下对动态领域知识的刻画和推理.为了将分支时序逻辑的刻画能力引入到动态描述逻辑中,将时间的进展体现子动作的执行,从而将时序维与动态维统一起来.在此基础上,从描述逻辑ALCQIO出发构建了一个时序动态描辑TDALCQIO,给出了TDALCQIO 的Tableau 判定算法,并证明了算法的可终止性和正确性.TDALCQIO 不仅兼容了构描述逻辑ALCQIO 基础上的动态描述逻辑的刻画和推理能力,而且还可从可达性、安全性等角度对整个动态的时序特征进行刻画和推理,从而为语义Web 环境下对动态领域知识的刻画和推理提供了进一步的逻辑支持.

    Abstract:

    The dynamic description logic DDL (dynamic description logic) provides a kind of action theory based on description logics. It is a useful representation of the dynamic application domains in the environment of the Semantic Web. In order to bring the representation capability of the branching temporal logic into the dynamic description logic, this paper treats the time slices of temporal logics as the executions of atomic actions, so that the temporal dimension and the dynamic dimension can be unified. Based on this idea, constructed over the description logic ALCQIO, a temporal dynamic description logic, named TDALCQIO, is presented. Tableau decision algorithm is provided for TDALCQIO. Both the termination and the correctness of this algorithm have been proved. The logic TDALCQIO not only inherits the representation capability provided by the dynamic description logic constructed over ALCQIO (attributive language with complements, qualified number restrictions, inverse roles and nominals), but it also has the ability to describe and reason about some temporal features such as the reachability property and the safety property of the whole dynamic application domains. Therefore, TDALCQIO provides further support for knowledge representation and reasoning in the environment of the Semantic Web.

    参考文献
    [1] Bonatti P, Lutz C, Wolter F. Description logics with circumscription. In: Doherty P, Mylopoulos J, Welty C, eds. Proc. of the 10thInt’l Conf. on Principles of Knowledge Representation and Reasoning. Menlo Park: AAAI Press, 2006. 400-410.
    [2] Ma Y, Hitzler P, Lin ZQ. Algorithms for paraconsistent reasoning with OWL. In: Franconi E, Kifer M, May W, eds. Proc. of the4th European Semantic Web Conf. Belin: Springer-Verlag, 2007. 399-413. [doi: 10.1007/978-3-540-72667-8_29]
    [3] Kang DZ, Xu BW, Lu JJ, Li YH. Reasoning within extended fuzzy description logic supporting terminological axiom restrictions.Journal of Software, 2007,18(7):1563-1572 (in Chinese with English abstract). http://www.jos.org.cn/1000-9825/18/1563.htm [doi:10.1360/jos181563]
    [4] Jiang YC, Wang J, Tang SQ, Xiao B. Reasoning with rough description logics: An approximate concepts approach. InformationSciences, 2009,179(5):600-612. [doi: 10.1016/j.ins.2008.10.021]
    [5] Shi ZZ, Dong MK, Jiang YC, Zhang HJ. A logical foundation for the semantic Web. Science in China (Series F: InformationSciences), 2005,48(2):161-178. [doi: 10.1360/03yf0506]
    [6] Chang L, Shi ZZ, Qiu LR, Lin F. A tableau decision algorithm for dynamic description logic. Chinese Journal of Computers, 2008,31(6):896-909 (in Chinese with English abstract).
    [7] Chang L, Shi ZZ, Chen LM, Niu WJ. Family of extended dynamic description logics. Journal of Software, 2010,21(1):1-13 (inChinese with English abstract). http://www.jos.org.cn/1000-9825/21/1.htm [doi: 10.3724/SP.J.1001.2010.03494]
    [8] Shi ZZ, Chang L. Reasoning about semantic Web services with an approach based on dynamic description logics. Chinese Journalof Computers, 2008,31(9):1599-1611 (in Chinese with English abstract).
    [9] Gabbay DM, Kurucz A, Wolter F, Zakharyaschev M. Many-Dimensional Modal Logics: Theory and Applications. New York:Elsevier, 2003. 367-375.
    [10] Henriksen JG, Thiagarajan PS. Dynamic linear time temporal logic. Annals of Pure and Applied Logic, 1999,96(1-3):187-207. [doi:10.1016/S0168-0072(98)00039-6]
    [11] Clarke EM, Emerson EA. Design and synthesis of synchronization skeletons using branching time temporal logic. In: Kozen D, ed.Proc. of the Logic of Programs. LNCS 131, Heidelberg: Springer-Verlag, 1982. 52-71. [doi: 10.1007/BFb0025774]
    [12] Chang L, Lin F, Shi ZZ. A dynamic description logic for representation and reasoning about actions. In: Zhang ZL, Siekmann J, eds.Proc. of the 2nd Int’l Conf. on Knowledge Science, Engineering and Management. Berlin: Springer-Verlag, 2007. 115-127. [doi:10.1007/978-3-540-76719-0_15]
    [13] Wang J, Jiang YC, Shen YM. Satisfiability and reasoning mechanism of terminological cycles in description logic vL. Science inChina (Series F: Information Sciences), 2008,51(9):1204-1214. [doi: 10.1007/s11432-008-0101-6]
    [14] Hromkovic J, Seibert S. Translating regular expressions into small ε-free nondeterministic finite automata. Journal of Computerand System Sciences, 2001,62(4):565-588. [doi: 10.1006/jcss.2001.1748]
    [15] Baader F, Lutz C, Milicic M, Sattler U, Wolter F. Integrating description logics and action formalisms: First results. In: Veloso M,Kambhampati S, eds. Proc. of the 12th National Conf. on Artificial Intelligence. Menlo Park: AAAI Press/The MIT Press, 2005.572-577.
    [16] Gu YL, Soutchanski M. Decidable reasoning in a modified situation calculus. In: Veloso M, ed. Proc. of the 20th Int’l Joint Conf.on Artificial Intelligence. Menlo Park: AAAI Press, 2007. 1891-1897.
    [17] Giordano L, Martelli A. Tableau-Based automata construction for dynamic linear time temporal logic. Annals of Mathematics andArtificial Intelligence, 2006,46(3):289-315. [doi: 10.1007/s10472-006-9020-7]
    [18] Giordano L, Martelli A, Schwind C. Reasoning about actions in dynamic linear time temporal logic. Logic Journal of the IGPL,2001,9(2):273-288. [doi: 10.1093/jigpal/9.2.273]
    [19] Giordano L, Martelli A, Schwind C. Specifying and verifying interaction protocols in a temporal action logic. Journal of AppliedLogic, 2007,5(2):214-234. [doi: 10.1016/j.jal.2005.12.011]
    网友评论
    网友评论
    分享到微博
    发 布
引用本文

常亮,史忠植,古天龙,王晓峰.可判定的时序动态描述逻辑.软件学报,2011,22(7):1524-1537

复制
分享
文章指标
  • 点击次数:5190
  • 下载次数: 6083
  • HTML阅读次数: 0
  • 引用次数: 0
历史
  • 收稿日期:2009-11-03
  • 最后修改日期:2010-03-05
文章二维码
友情链接:中国科学院软件研究所中国计算机学会中国科学院国家自然科学基金委员会CCF数字图书馆Int'l J of Softw Info计算机系统应用
您是第19765620位访问者
版权所有：中国科学院软件研究所 京ICP备05046678号-3
地址：北京市海淀区中关村南四街4号,邮政编码：100190
电话：010-62562563 传真：010-62562533 Email：jos@iscas.ac.cn
技术支持：北京勤云科技发展有限公司

京公网安备 11040202500063号