×

A tableau decision algorithm for modalized \(\mathcal A\mathcal L\mathcal C\) with constant domains. (English) Zbl 1010.03012

Summary: The aim of this paper is to construct a tableau decision algorithm for the modal description logic \(K_{\mathcal A\mathcal L\mathcal C}\) with constant domains. More precisely, we present a tableau procedure that is capable of deciding, given an \(\mathcal A\mathcal L\mathcal C\)-formula \(\varphi\) with extra modal operators (which are applied only to concepts and TBox axioms, but not to roles), whether \(\varphi\) is satisfiable in a model with constant domains and arbitrary accessibility relations. Tableau-based algorithms have been shown to be ‘practical’ even for logics of rather high complexity. This gives us grounds to believe that, although the satisfiability problem for \(K_{\mathcal A\mathcal L\mathcal C}\) is known to be NEXPTIME-complete, by providing a tableau decision algorithm we demonstrate that highly expressive description logics with modal operators have a chance to be implementable. The paper gives a solution to an open problem of F. Baader and A. Laux [“Terminological logics with modal operators”, in: C. Mellish (ed.), Proc. 14th International Joint Conference on Artificial Intelligence, Montreal, PQ, 1995, IJCAI-95. San Francisco: Morgan Kaufmann, 808-814 (1995)].

MSC:

03B45 Modal logic (including the logic of norms)
03B25 Decidability of theories and sets of sentences
03B35 Mechanization of proofs and logical operations
68T27 Logic in artificial intelligence
Full Text: DOI