可判定的时序动态描述逻辑  

Decidable Temporal Dynamic Description Logic

作　　者：常亮[1] 史忠植[2] 古天龙[1] 王晓峰[2] 

机构地区：[1]桂林电子科技大学广西可信软件重点实验室,广西桂林541004 [2]中国科学院计算技术研究所智能信息处理重点实验室,北京100190

出　　处：《软件学报》2011年第7期1524-1537,共14页Journal of Software

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

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

关 键 词：动态描述逻辑 分支时序逻辑 知识表示和推理 动作理论 Tableau判定算法 

分 类 号：TP181[自动化与计算机技术—控制理论与控制工程]