= Solution
The satisfiability problem is $\boxed{\text{decidable}}$. Partition the positive facts according to their predicate symbols. Let $\mathcal A_{\mathcal T}$ contain those using <description logic concepts> or <description logic roles> from $\mathcal T$. Run an ordinary <ALC> <knowledge base> consistency procedure on $(\mathcal T,\mathcal A_{\mathcal T})$. Return `no` if it is inconsistent, and `yes` otherwise.
The `no` answer is sound because any model of the whole <knowledge base> would restrict to a model of $(\mathcal T,\mathcal A_{\mathcal T})$. For the converse, take a model $\mathcal I$ of that <ALC> part. Keep its domain, individual interpretations and <TBox> predicates. Interpret every predicate used by the positive <Datalog> rules as the full relation of its arity on this same domain. This is possible because those predicates are disjoint from the <TBox> predicates. Every <Datalog> rule head is then true under every variable assignment, so every positive rule and every remaining positive fact is satisfied. Predicates occurring only in facts can likewise be interpreted as full relations. Any individual name not already interpreted can denote an arbitrary domain element.
Consequently,
$$
\boxed{(\mathcal T,\mathcal R,\mathcal A)\text{ is satisfiable}\quad\Longleftrightarrow\quad(\mathcal T,\mathcal A_{\mathcal T})\text{ is satisfiable}.}
$$
The argument depends on both restrictions in the question: disjoint predicate vocabularies and positive rule heads. A rule concluding $\bot$ would not be made true by filling all relations. Sharing constants alone causes no problem, since the expansion uses the same domain and the same interpretations of those constants.
Back to article page
