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.

翻译：描述逻辑是知识表示中常用的一种形式化方法，其中知识通过从受限词汇表中以受控方式构建的概念形式进行捕获。这使得能够有效检测概念间的一致性及包含关系。概念合一同样可能成为分析概念间关系的有用工具。针对描述逻辑$\mathcal{FL}_0$和$\mathcal{EL}$的合一问题已被解决，但这些小型逻辑无法表达否定概念。本文提出了一种在$\mathcal{FL}_\bot$中求解合一的算法，该逻辑在$\mathcal{FL}_0\)基础上扩展了底概念。底概念允许表达两个概念不相交。该算法的时间复杂度与问题规模呈指数关系。