摘要
在一些基于本体的动态应用中,需要描述组合动作和变化域的时间特性。为了对这类应用建模,通过整合动态时序逻辑和描述逻辑,提出一类描述逻辑扩展。分析了该类扩展的基本形式DLTLALC的语法和语义,并提出一种可终止的tableau算法判别DLTLALC公式可满足性。利用该类扩展,可以表达组合动作执行过程中域变化的时间特性,该类扩展为语义Web服务等动态应用建模和推理提供了一条有效途径。
In some ontology based dynamic applications,there are needs for describing composite actions and time properties about changing domains.This paper proposed a family of extensions of description logics,integrating description logics into dynamic linear time temporal logic,for modeling these applications.First analyzed the syntax,semantics of DLTLALC,the basic formalism of the extensions,and presented a terminating tableau algorithm for determining the DLTLALC-formulas＇ satisfiability.With the extensions,time properties about changing domains according to the execution of composite actions can be expressed,so the extensions provide good support for modeling and reasoning about dynamic applications,such as semantic Web services etc.
出处
《计算机应用研究》
CSCD
北大核心
2012年第2期536-541,共6页
Application Research of Computers
基金
国家自然科学基金资助项目(60970040)
关键词
动态时序描述逻辑
动作推理
表判定算法
语义WEB服务
dynamic linear temporal description logics
reasoning about actions
tableau decision algorithm
semantic Web service
