论文部分内容阅读
动态描述逻辑DDL（dynamic description logic）提供了一种基于描述逻辑的动作理论，适用于语义Web环境下对动态领域知识的刻画和推理．为了将分支时序逻辑的刻画能力引入到动态描述逻辑中，将时间的进展体现为原子动作的执行，从而将时序维与动态维统一起来．在此基础上，从描述逻辑ALCQIO出发构建了一个时序动态描述逻辑TDALCQIO,给出了TDALCQIO的Tableau判定算法，并证明了算法的可终止性和正确性．TDALCQIO不仅兼容了构建在描述逻辑ALCQIO基础上的动态描述逻辑的刻画