Solving unification in the description logic FL_\bot

2024/05/01 by Morawska, Barbara, Marzec, Dariusz
#FOS: Computer and information sciences #Logic in Computer Science (cs.LO) #Symbolic Computation (cs.SC)

paper · doi:10.48550/arxiv.2405.00912

Abstract

We present an algorithm for solving the unification problem in the description logic FL_\bot. This logic extends FL₀ 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 FL₀ and 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.

Related

• Efficient TBox Reasoning with Value Restrictions using the\n \FL_ower reasoner
• Yet Another Efficient Unification Algorithm
• FILO -- automated unification in FL₀
• Separating Data Examples by Description Logic Concepts with Restricted\n Signatures
• Union and Intersection of all Justifications