关键词: 时态描述逻辑,分支时态逻辑,可满足性问题,Tableau算法,复杂度 中图法分类号TP301文献标识码A

Abstract: As a combination of the description logic and the temporal logic,the temporal description logic offers consi-derable expressive power．However most of the researches on temporal description logic have concentrated on the case where temporal operators occur within concepts and formula．In this setting,reasoning usually becomes quite hard．This paper combined standard description logic ALC with standard temporal logic CTL and proposed a new temporal description logic ALC-CTL．More precisely,we applied temporal operators only to formula not to concept．From the perspective of the computational tree logic,it is equivalent that atomic proposition in CTL is promoted to individual assertion in ALC．This ALC-CTL not only offers considerable expressive power going beyond both ALC and CTL,but also makes the satisfiability problem of it to preserve EXPTIME-complete．Based on a combination of the Tableau algorithm of CTL and the reasoning mechanism provided by ALC,this paper presented a Tableau decision algorithm for the logic ALC-CTL and proved that this algorithm is terminating,sound and complete.

Key words: Temporal description logic,Branching temporal tree logic,Satisfiability problem,Tableau algorithm,Complexity