A PSpace Tableau Algorithm for Acyclic Modalized ALC

Tao, Jia, Slutzki, Giora and Honavar , Vasant (2010) A PSpace Tableau Algorithm for Acyclic Modalized ALC. Technical Report TR11-01, Computer Science, Iowa State University.

Abstract

We study ALCK_m, which extends the description logic ALC by adding modal operators of the basic multi-modal logic K_m. We develop a sound and complete tableau algorithm Lambda_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, we are able to give a PSpace implementation for Lambda_K. We next consider answering ALCK_m queries w.r.t. an ALCK_m knowledge base in which the epistemic operators correspond to those of classical multi-modal logic S4_m. The expansion rules in the tableau algorithm Lambda_{S4} are designed to syntactically incorporate the epistemic properties. We also provide a PSpace implementation for Lambda_{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 ALCK_m offers computationally manageable and practically useful fragment of K_{ALC}.