Tableaux for temporal description logic with constant domains

We show how to combine the standard tableau system for the basic description logic ALC and Wolper’s tableau calculus for proposi- tional temporal logic PTL (with the temporal operators ‘next-time’ and ‘until’) in order to design a terminating sound and complete tableau- based satisfiability-checking algorithm for the temporal description logic PTL ALC of [20] interpreted in models with constant domains. We use the method of quasimodels [18,16] to represent models with in finite domains, and the technique of minimal types [11] to maintain these domains constant. The combination is flexible and can be extended to more expressive description logics or even to decidable fragments of first-order temporal logics