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

TL;DR

This paper introduces an exponential-time algorithm for unification in the description logic _ot, extending previous results to a richer logic that includes the bottom constructor.

Contribution

It provides the first unification algorithm for _ot, expanding the scope of unification in description logics beyond _0 and .

Findings

Algorithm runs in exponential time.

Supports conjunction, value restrictions, top and bottom constructors.

Extends unification results to richer description logics.

Abstract

We present an algorithm for solving the unification problem in the description logic $\mathcal{FL}_\bot$. This logic extends $\mathcal{FL}_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{FL}_0$ and $\mathcal{EL}$. 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.