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.
All Science Journal Classification (ASJC) codes
- Computational Theory and Mathematics
- Artificial Intelligence