PSPACE tableau algorithms for acyclic modalized ALC

We study ALCK _m and ALCS4 _m, which extend the description logic ALC by adding modal operators of the basic multi-modal logics K _m and S4 _m. We develop a sound and complete tableau algorithm ?K for answering ALCK _m queries w.r.t. an ALCK _m knowledge base with an acyclic TBox. Defining tableau expansion rules in the presence of acyclic definitions by considering only the concept names on the left-hand side of TBox definitions or their negations, allows us to give a PSpace implementation for ?K. We then consider answering ALCS4 _m queries w.r.t. an ALCS4 _m knowledge base (with an acyclic TBox) in which the epistemic operators correspond to those of classical multi-modal logic S4 ^m. The expansion rules in the tableau algorithm ?S4 are designed to syntactically incorporate the epistemic properties. Blocking is corporated into the tableau expansion rules to ensure termination. We also provide a PSpace implementation for ?S4. In light of the fact that the satisfiability problem for ALCK _m with general TBox and no epistemic properties (i.e., K _ALC) is NEXPTIME-complete, we conclude that both ALCK _m and ALCS4 _m offer computationally manageable and practically useful fragments of K _ALC.