Unification in the description logic $\mathcalFL_\bot$
<|reference_start|>Unification in the description logic $\mathcalFL_\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.<|reference_end|>
@article{morawska2024unification,
    title={Unification in the description logic $\mathcal{FL}_\bot$},
    author={Barbara Morawska},
    journal={arXiv preprint arXiv:2405.00912},
    year={2024},
    archivePrefix={arXiv},
    eprint={2405.00912},
    primaryClass={cs.SC cs.LO}
}