= Solution
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 $\bot$. 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 use
$$
\boxed{\begin{aligned}
\exists R.A&\sqsubseteq X,\qquad X\sqsubseteq\exists R.A,\\
X&\sqsubseteq\exists R.X,\\
A\sqcap B&\sqsubseteq\bot,\\
C&\sqsubseteq\exists P.\top,\qquad \exists P.\top\sqsubseteq C.
\end{aligned}}
$$
These 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 $\bot$. 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\sqsubseteq\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\sqsubseteq\bot$ from this normalized <TBox>.
Back to article page
