

Tao, Jia, Slutzki, Giora and Honavar , Vasant (2010) A PSpace Tableau Algorithm for Acyclic Modalized ALC. Technical Report TR1101, Computer Science, Iowa State University.
Abstract
We study ALCK_m, which extends the description logic ALC
by adding modal operators of the basic multimodal 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 lefthand 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 multimodal 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 NEXPTIMEcomplete, we conclude that ALCK_m offers computationally manageable and practically useful fragment of K_{ALC}.
Contact site administrator at: ssg@cs.iastate.edu
