A Tableau Calculus for Temporal Description Logic: the Expanding Domain Case
Holger Sturm · Journal of Logic and Computation · 2002
In this paper we present a tableau calculus for a temporal extension of the description logic ALC, called TLALC. This logic is based on the temporal language with ‘Until’ interpreted over the natural numbers with expanding ALC‐domains. The tableau calculus forms an elaborate combination of Wolper's tableau calculus for propositional linear temporal logic, the standard tableau‐algorithm for ALC, and the method of quasimodels introduced by Wolter and Zakharyaschev. Based on those three ingredients the paper provides a new method of how tableau‐based decision procedures can be constructed for many‐dimensional logics which lack the finite model property. The method can be applied to deal with other temporalized formalisms as well.