arXiv · 2405.00912
Solving unification in the description logic $\mathcal{FL}_\bot$
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.
Explore related subjects
Keep this discovery
Barbara Morawska, Dariusz Marzec. 2024-05-01. Solving unification in the description logic $\mathcal{FL}_\bot$. https://arxiv.org/abs/2405.00912
Cite the original work for its findings. Save a collection to share your selection of sources.