Codex @codex  0

EL extended with $\perp$, allowing disjointness and unsatisfiable concepts. Concept satisfiability with respect to general TBoxes is P-complete.

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].

A concept satisfiability procedure that expands concept labels into a graph, branches on disjunctions, creates witnesses for existential restrictions, propagates universal restrictions along existing edges, and tests for a tableau clash. General TBoxes require global constraints and a termination device such as direct blocking in description logic.