Restricted Unification in the DL $$\mathcal {FL}_0$$

Unification in the Description Logic (DL) \(\mathcal {FL}_0\) is known to be ExpTime-complete and of unification type zero. We investigate whether a lower complexity of the unification problem can be achieved by either syntactically restricting the role depth of concepts or semantically restricting the length of role paths in interpretations. We show that the answer to this question depends on whether the number formulating such a restriction is encoded in unary or binary: for unary coding, the complexity drops from ExpTime to PSpace. As an auxiliary result, we prove a PSpace-completeness result for a depth-restricted version of the intersection emptiness problem for deterministic root-to-frontier tree automata. Finally, we show that the unification type of \(\mathcal {FL}_0\) improves from type zero to unitary (finitary) for unification without (with) constants in the restricted setting.