= Solution
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 $\bot$ 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\sqsubseteq G_i$. Encode an AND gate by $G_i\sqcap G_j\sqsubseteq G_k$, and an OR gate by $G_i\sqsubseteq G_k$ and $G_j\sqsubseteq G_k$. Finally add $G_{\mathrm{out}}\sqsubseteq\bot$. 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 $\bot$ changes a trivial satisfiability problem into a nontrivial polynomial-time one. The bottom-inclusive convention is also reflected in the <OWL 2 Web Ontology Language Profiles (Second Edition)>[Sections 2 and 5: allowed class expressions and the complexity table for OWL 2 EL]{ref}.
Back to article page
