Abstract: As a combination of the description logic ALC and the linear temporal logic LTL, the temporal description logic ALC-LTL not only offers considerable expressive power going beyond both ALC and LTL, but also makes the satisfiability problem of it preserved to be EXPTIME-complete;however,an efficient decision algorithm for ALC-LTL is still absent Based on a combination of the Tableau algorithm of LTL and the reasoning mechanism provided by ALC,this paper presented a Tablcau decision algorithm for the logic ALC-L TL and proved that this algorithm is terminating,sound and complete. hhis algorithm enjoys excellent expandability; when the ALC component in the logic ALC-LTL is substituted by any other description logic X which is still decidable, this algorithm can be easily modified to act as a Tablcau decision algorithm for the corresponding temporal description logic X-LTL.

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