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

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

May 13, 2024 | Barbara Morawska
This paper presents an algorithm for unification in the description logic FL⊥*, which extends FL0 with the bottom concept. FL⊥* allows expressing disjointness between concepts, which is not possible in FL0. The algorithm runs in exponential time with respect to the problem size. The unification problem is defined as a set of pairs of concepts, where a substitution makes the concepts equivalent. The algorithm involves two stages: flattening and solving a normalized problem. Flattening reduces the problem to a set of subsumptions, while solving involves handling start, flat, and increasing subsumptions. The algorithm uses shortcuts to distribute particles and resolve conflicts. The paper also proves the correctness of the algorithm and shows that it can solve unification problems in FL⊥* efficiently. The algorithm is tested on various examples, including cases where unification is impossible. The main contribution is the development of an exponential-time algorithm for unification in FL⊥*, which extends previous results for FL0 and EL.This paper presents an algorithm for unification in the description logic FL⊥*, which extends FL0 with the bottom concept. FL⊥* allows expressing disjointness between concepts, which is not possible in FL0. The algorithm runs in exponential time with respect to the problem size. The unification problem is defined as a set of pairs of concepts, where a substitution makes the concepts equivalent. The algorithm involves two stages: flattening and solving a normalized problem. Flattening reduces the problem to a set of subsumptions, while solving involves handling start, flat, and increasing subsumptions. The algorithm uses shortcuts to distribute particles and resolve conflicts. The paper also proves the correctness of the algorithm and shows that it can solve unification problems in FL⊥* efficiently. The algorithm is tested on various examples, including cases where unification is impossible. The main contribution is the development of an exponential-time algorithm for unification in FL⊥*, which extends previous results for FL0 and EL.
Reach us at info@study.space