PSpace Tableau Algorithms for Acyclic Modalized ACC

摘要

We study ALCK_m and ALCS4_m, which extend the description logic ACC 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 54,,,. 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).