| 摘要: |
| 动态描述逻辑DDL(dynamic description logic)提供了一种基于描述逻辑的动作理论,适用于语义Web 下对动态领域知识的刻画和推理.为了将分支时序逻辑的刻画能力引入到动态描述逻辑中,将时间的进展体现子动作的执行,从而将时序维与动态维统一起来.在此基础上,从描述逻辑ALCQIO出发构建了一个时序动态描辑TDALCQIO,给出了TDALCQIO 的Tableau 判定算法,并证明了算法的可终止性和正确性.TDALCQIO 不仅兼容了构描述逻辑ALCQIO 基础上的动态描述逻辑的刻画和推理能力,而且还可从可达性、安全性等角度对整个动态的时序特征进行刻画和推理,从而为语义Web 环境下对动态领域知识的刻画和推理提供了进一步的逻辑支持. |
| 关键词: 动态描述逻辑 分支时序逻辑 知识表示和推理 动作理论 Tableau 判定算法 |
| DOI：10.3724/SP.J.1001.2011.03869 |
| 分类号: |
| 基金项目:国家自然科学基金(60903079, 60775035, 60963010, 60803033); 国家高技术研究发展计划(863)(2007AA01Z132);
国家重点基础研究发展计划(973)(2007CB311004); 广西自然科学基金(0832006Z) |
|
| Decidable Temporal Dynamic Description Logic |
|
CHANG Liang1, SHI Zhong-Zhi2, GU Tian-Long1, WANG Xiao-Feng2
|
|
1.Guangxi Key Laboratory of Trusted Software, Guilin University of Electronic Technology, Guilin 541004, China;2.Key Laboratory of Intelligent Information Processing, Institute of Computing Technology, The Chinese Academy of Sciences, Beijing 100190
|
| 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. |
| Key words: dynamic description logic branching temporal logic knowledge representation and reasoning action theory Tableau decision algorithm |
