PSPACE tableau algorithms for acyclic modalized ALC

Jia Tao, Giora Slutzki, Vasant Honavar

Research output: Contribution to journalArticlepeer-review

4 Scopus citations


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.

Original languageEnglish (US)
Pages (from-to)551-582
Number of pages32
JournalJournal of Automated Reasoning
Issue number4
StatePublished - Dec 2012

All Science Journal Classification (ASJC) codes

  • Software
  • Computational Theory and Mathematics
  • Artificial Intelligence


Dive into the research topics of 'PSPACE tableau algorithms for acyclic modalized ALC'. Together they form a unique fingerprint.

Cite this