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

Abstract

We present an algorithm for solving the unification problem in the description logic ${\mathcal{F}\mathcal{L}}_{\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.

Extended version of the paper submitted to KR 2025