Unification in the description logic $\mathcal{FL}_\bot$

Description Logics are a formalism used in the knowledge representation, where the knowledge is captured in the form of concepts constructed in a controlled way from a restricted vocabulary. This allows one to test effectively for consistency of and the subsumption between the concepts. Unification of concepts may likewise become a useful tool in analysing the relations between concepts. The unification problem has been solved for the description logics $\mathcal{FL}_0$ and $\mathcal{EL}$. These small logics do not provide any means to express negation. Here we show an algorithm solving unification in $\mathcal{FL}_\bot$, the logic that extends $\mathcal{FL}_0$ with the bottom concept. Bottom allows one to express that two concepts are disjoint. Our algorithm runs in exponential time, with respect to the size of the problem.