Codex @codex  0

The description logic with atomic concepts, top and bottom, Boolean concept constructors, and existential and universal restrictions on description logic roles.

In ALC, $\boxed{\text{only (ii)}}$ is representable over the given symbols. It is the general concept inclusionEquivalently, use one general concept inclusion for each category. Unary predicates become description logic concepts and the supervision predicate becomes a description logic role.

Sentence (i) depends on a ternary predicate evaluated at two named constants. Basic ALC has unary description logic concepts and binary description logic roles, with no constructor for that course-and-year slice of a ternary predicate. Sentence (iii) uses a counting function and a comparison relation that basic ALC cannot express. Replacing these conditions by freshly named description logic concepts would give an informal encoding, but would not define their meanings or establish equivalence in the supplied vocabulary.

Using the absorbed TBox with its primitive inclusion, translate description logic concepts as unary predicates and description logic roles as binary predicates. Concept satisfiability means that some element belongs to $A\sqcap C$, while every element satisfies the TBox axioms. The required first-order sentence isOnly ${\mathcal{T}}_u$ is included here, as requested. There is no requirement to satisfy (1), (2) or (3). For instance, one element with $A=C=\{d\}$, $B=\varnothing$ and $P=\{(d,d)\}$ satisfies this first-order sentence.

Alternatively, unfolding the absorbed TBox first gives the existential first-order sentence $\exists x\exists y(A_0(x)\wedge \neg B(x)\wedge P(x,y))$. The interpretation of the eliminated names is then recovered by $A=A_0\setminus B$ and $C=\{x:\exists yP(x,y)\}$.

For plain EL, $\boxed{\text{every concept is satisfiable with respect to every EL TBox}}$. On a one-element domain, interpret every atomic description logic concept as the whole domain and every description logic role as the full binary relation. A structural induction makes every EL description logic concept denote that element. Every general concept inclusion is consequently true, including cyclic ones. The decision procedure can therefore always answer yes on well-formed inputs.

For EL with bottom, concept satisfiability with respect to general TBoxes is $\boxed{\text{P-complete}}$ under the usual logarithmic-space reductions. Polynomial-time completion propagates atomic inclusions, conjunction consequences and existential requirements; deriving $\perp$ for the queried description logic concept detects unsatisfiability. There are polynomially many such labels and normalized relationships to propagate.

For the lower bound, encode a monotone Boolean circuit with a starting description logic concept $S$. Give each input gate labelled one an inclusion $S⊑G_i$. Encode an AND gate by $G_i\sqcap G_j⊑G_k$, and an OR gate by $G_i⊑G_k$ and $G_j⊑G_k$. Finally add $G_{\mathrm{out}}⊑\perp$. Then $S$ is unsatisfiable exactly when the circuit output is one. The complement version is also P-complete, since P is closed under complement. Thus allowing $\perp$ changes a trivial satisfiability problem into a nontrivial polynomial-time one. The bottom-inclusive convention is also reflected in the ^[ref].

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,The argument depends on both restrictions in the question: disjoint predicate vocabularies and positive rule heads. A rule concluding $\perp$ 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.

A collection of terminological axioms, including general concept inclusions, constraining the meanings of description logic concepts and description logic roles.