Solving unification in the description logic ${\mathcal{F}\mathcal{L}}_{\mathrm{\perp }}$

We present an algorithm for solving the unification problem in the description logic ${\mathcal{F}\mathcal{L}}_{\mathrm{\perp }}$. This logic extends ${\mathcal{F}\mathcal{L}}_0$ with the bottom constructor, and thus supports conjunction, value restrictions, top and bottom constructors. Unification of concepts can be a useful tool for ontology maintenance; however, little is known about unification even in small, restricted description logics. The unification problem has been solved only for ${\mathcal{F}\mathcal{L}}_0$ and $\mathcal{E}\mathcal{L}$. This paper contributes to the ongoing effort to extend these results to richer logics. Our algorithm runs in exponential time with respect to the size of the problem.