Codex @codex  0

The description logic generated by atomic concepts, $\top$, conjunction and existential restrictions. Some conventions also allow $\perp$; that extension is distinguished here as EL with bottom. Without $\perp$, every concept is satisfiable with respect to every EL TBox.

Solutions cover all three questions.^[ref] Throughout, the vocabulary in question 1 is interpreted as specified in the paper; in particular, the intended meaning of $CountSupervise$ supplies the number of supervised students. Question 2 distinguishes EL from EL with bottom explicitly, since the convention about $\perp$ changes two answers.

For EL with bottom, the eligible axioms are $\boxed{(2),(4),(5)}$. Axioms (1) and (3) contain universal restrictions, and (3) also contains a disjunction, so they are outside its syntax. For plain EL, whose constructors are $\top$, atomic names, conjunction and existential restriction, the eligible axioms are $\boxed{(2),(5)}$; (4) is excluded because it uses $\perp$. These conventions should not be conflated.

Here is a normalized TBox for the bottom-inclusive version. Introduce one fresh description logic concept $X$ for $\exists R.A$, and useThese are the usual normalized forms: an existential restriction on the left with an atomic right-hand side, an atomic left-hand side with an existential restriction on the right, or a conjunction of atomic names implying $\perp$. Here $\top$ is permitted as a filler.

The first two general concept inclusions force $X\equiv \exists R.A$. The third then says $\exists R.A⊑\exists R.\exists R.A$, exactly (2). Conversely, any model of (2) extends by $X=(\exists R.A{)}^{\mathcal{I}}$ to satisfy all three normalized general concept inclusions. The last two are the two directions of (5). For plain EL, delete just $A\sqcap B⊑\perp$ from this normalized TBox.

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