# The unification type of the description logic FL⊥ is nullary

Barbara Morawska, Slawomir Kost

► To cite this version:

Barbara Morawska, Slawomir Kost. The unification type of the description logic FL⊥ is nullary. UNIF 2025 - 39th International Workshop on Unification, Jul 2025, Birmingham, United Kingdom. hal-05148632

HAL Id: hal-05148632

https://hal.science/hal-05148632v1

Submitted on 7 Jul 2025

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
# The unification type of the description logic $\mathcal{FL}_{\perp}$ is nullary

Barbara Morawska* and Sławomir Kost†

Institute of Computer Science, University of Opole, Oleska 48, Opole 45-052, Poland

## Abstract

Description Logics are used to formalize knowledge in the form of complex concepts, constructed from concept names using provided logical constructors. The description logic $\mathcal{FL}_{\perp}$ is a sub-boolean logic, with very limited expressive power. It provides only conjunction, value restrictions, and top and bottom constructors. In particular, there is no negation constructor available. Subsumption between concepts is polynomial. The unification problem has not yet been solved. We present a proof of type zero unification for $\mathcal{FL}_{\perp}$. The result is inspired by a similar result for the modal logic K in [3].

**Keywords:** description logic, unification type.

## 1 Introduction.

Description logics belong to the area of knowledge representation. They use concept names (unary predicates) and role names (relations) to model general statements in a domain of interest, such as human anatomy, taxonomy of diseases, etc. Restricted rules for constructing complex concepts from primitive names provide a means to precisely define semantics, which is essentially the same as the semantics employed in first-order logic. This approach to formalizing knowledge through description logics offers many ways to automate reasoning over large knowledge repositories, called ontologies.

The standard reasoning task in this area is to decide the subsumption problem between two concepts and, further, to construct a hierarchy of all concepts in a given domain with respect to the subsumption relation. Another reasoning task, proposed as a formal tool for maintaining ontologies, is unification of concepts. Unification can help ontology engineers detect redundancies in an ontology and, by removing them, significantly reduce the complexity of typical tasks (such as searching or retrieving information).

Unification in description logics was first studied in [2] by F. Baader and P. Narendran. Their paper provided the first algorithm to solve unification in the description logic $\mathcal{FL}_0$. The problem was proven to be ExpTime-complete. As noted by the authors, this logic has nullary unification because it can be directly translated into the equational theory ACUIh, which has been proven to have nullary unification [1]. Consequently, although the unification problem in $\mathcal{FL}_0$ is decidable, we may not have a compact representation of all solutions.

This research is part of the project No 2022/47/P/ST6/03196 within the POLONEZ BIS programme co-funded by the National Science Centre and the European Unions Horizon 2020 research and innovation programme under the Marie Skodowska-Curie grant agreement No. 945339. For the purpose of Open Access, the author has applied a CC-BY public copyright licence to any Author Accepted Manuscript (AAM) version arising from this submission.

<figure><img src="image_2.png" /></figure>

<footnote>*barbara.morawska@uni.opole.pl</footnote>

<footnote>†skost@uni.opole.pl</footnote>
The logic we are considering in this paper, $\mathcal{FL}_{\perp}$, extends $\mathcal{FL}_0$ with the bottom concept ($\perp$) a concept interpreted as false, i.e., by the empty set in all domains. Since $\mathcal{FL}_0$ does not include negation, bottom provides a minimal way to express negative statements, e.g., that two concepts are disjoint or that no relation exists between them. Despite many attempts, we have not yet been able to prove that unification in $\mathcal{FL}_{\perp}$ is decidable. Nevertheless, we can show that it has nullary type unification.

We discovered this result by leveraging the known correspondence between description and modal logics. In particular, it is well known that the description logic $\mathcal{ALC}$ corresponds to a multi-modal version of the modal logic $\mathcal{K}$. In [3], Jerábek shows that the unification in the modal logic $\mathcal{K}$ is nullary. He observes that this result directly applies to the description logic $\mathcal{ALC}$. We argue, however, that the result in [3] translates more accurately to the description logic $\mathcal{FL}_{\perp}$ which is a sub-logic of $\mathcal{ALC}$. Nevertheless we prove the nullary type for the unification in $\mathcal{FL}_{\perp}$ directly, using only the tools available within description logic.

## 2 The description logics $\mathcal{FL}_{\perp}$

The description logic $\mathcal{FL}_{\perp}$ provides the following constructors for creating complex concepts from two disjoint sets $N_C$ and $N_R$, reffered to us concept names and role names, respectively: $\top$, $\perp$ – the true and false concept; $\sqcap$ – conjunction of concepts; $\forall r.C$ – value restriction of $r \in N_R$ to a concept $C$.

Hence the set of complex concepts, $CC$, are the formulas generated by the grammar: $C ::= \top | \perp | A | C \sqcap C | \forall r.C$ where $A \in N_C, r \in N_R$.

An interpretation of concepts in $\mathcal{FL}_{\perp}$ is a pair $I = (\Delta^I, .^I)$, where $\Delta^I$ is a non-empty domain of elements and $.^I$ is an interpreting function defined on concept names and role names as follow: $\top^I = \Delta^I$; $\perp^I = \emptyset$; $A^I \subseteq \Delta^I$, for any $A \in N_C$; $r^I \subseteq \Delta^I \times \Delta^I$, for any $r \in N_R$ and extended to all complex concepts in the usual way. $(C_1 \sqcap C_2)^I = C_1^I \cap C_2^I$; $(\forall r.C)^I = \{d \in \Delta^I | \forall e \in \Delta^I[(d, e) \in r^I \rightarrow e \in C^I]\}$; $(\forall v.C)^I = (\forall r_1\forall r_2\dots\forall r_n.C)^I$ where $v = r_1\dots r_n \in N_R^*$. If $v = \varepsilon$, $(\forall \varepsilon.C)^I = C^I$.

Based on the semantics it is easy to see that a complex concept may be reduced with the following reductions to an equivalent concept (interpreted by the same set in any interpretation). $C \sqcap \top, \top \sqcap C \rightsquigarrow C$; $C \sqcap \perp, \perp \sqcap C \rightsquigarrow \perp$; $\forall r.\top \rightsquigarrow \top$; $\forall r.(C_1 \sqcap C_2) \rightsquigarrow \forall r.C_1 \sqcap \forall r.C_2$. We call a concept *C reduced* iff none of the reduction rules applies to $C$.

### Particles

For convenience, we will use the notation $\forall v.\alpha$ for the concept of the form: $\forall r_1(\forall r_2(...(\forall r_n.\alpha))),$ where $v = r_1...r_n$ and $\alpha$ is either $\top$ or $\perp$ or a concept name $A$. A concept of this form is called a *particle*. The word $v$ over $N_R$ is called the *role word* of the particle $\forall v.\alpha$.

It is easy to see that a reduced concept is equivalent to a conjunction of particles, $C = \forall v_1.\alpha_1 \sqcap \dots \sqcap \forall v_n.\alpha_n$, where $v_1, \dots, v_n$ are possibly empty words over $N_R$. In fact because of properties of conjunction, we identify a reduced concept with a set of particles in such a conjunction, $C = \{\forall v_1.\alpha_1, \dots, \forall v_n.\alpha_n\}$.

**Definition 2.1** (Role depth). Let $C$ be an $\mathcal{FL}_{\perp}$-reduced concept. We define $rd(C)$ recursively: if $C = A$ or $C = \top$ or $C = \perp$, then $rd(C) = 0$; if $C = C_1 \sqcap C_2$, then $rd(C) = \max(\{rd(C_1), rd(C_2)\})$; if $C = \forall r.C'$, $rd(C) = rd(C') + 1$.

### Subsumption
Based on the semantics, we define subsumption and equivalence between concepts. $C \subseteq D$ if and only if for all interpretations $I$, $C^I \subseteq D^I$. $C \equiv D$ if and only if $C \subseteq D$ and $D \subseteq C$. It should be obvious that $\perp \subseteq C$ and $C \perp \top$, for any concept $C$.

Now, consider reduced concepts $C$ and $D = \{P_1, \dots, P_n\}$, where the $P_i$ are particles. By the properties of conjunction (here represented by a set of particles), we can see that:

$C \subseteq D$ holds if and only if for every $P \in D$, $C \subseteq P$.

Due to these properties, it is also easy to prove the following lemma characterizing subsumptions in $\mathcal{FL}_{\perp}$.

**Lemma 2.2.** Let $C$ and $P$ be reduced concepts, and let $P$ be a particle. Then $C \subseteq P$ holds if and only if one of the following conditions is satisfied.

1. $P \in C$ or

2. $P = \forall v.\alpha$, where $\alpha$ is either a concept name or $\perp$, and there exists $\forall v'.\perp \in C$ such that $v' \le v$ ($v'$ is a prefix of $v$).

Here, $C$ and $P$ are reduced concepts and $P$ is a particle.

The following lemma will be useful for proving our result.

**Lemma 2.3.** Let $C$ be a reduced $\mathcal{FL}_{\perp}$ concept. If $C \subseteq \forall r.C$ then $C = \top$ or $C \subseteq \forall v.\perp$, where $|v| \le rd(C)$, with $|v|$ denoting the length of the role word $v$.

*Proof.* If $C = \top$, then the right-hand side of the subsumption $C \subseteq \forall r.C$ reduces to $\top$, and thus this subsumption clearly holds. Therefore, we now assume $C \neq \top$.

If $C$ is not $\top$, then $C$ is a non-empty set of particles. Consider a particle $P \in C$ such that $rd(P) = rd(C)$. Since $P \in C$, the particle $\forall r.P \in \neg \forall r.C \neg$, where $\neg \forall r.C \neg$ is the reduced form of $\forall r.C$. Then $\forall r.P \notin C$. By conditions in Lemma 2.2, this means that there is a particle $\forall v.\perp \in C$, such that $v$ is a prefix of the role word in $\forall r.P$. Obviously $C \subseteq \forall v.\perp$ and $|v| \le rd(C)$ as required.

□

Although we define concept equivalence via subsumption, it is helpful to observe that the semantics of $\mathcal{FL}_{\perp}$ induces an equational theory that satisfies a familiar set of algebraic laws. The equational theory for $\mathcal{FL}_{\perp}$ that characterizes when two concepts are semantically equivalent includes the following axioms:

* Associativity: $C_1 \sqcap (C_2 \sqcap C_3) = (C_1 \sqcap C_2) \sqcap C_3$

* Commutativity: $C_1 \sqcap C_2 = C_2 \sqcap C_1$

* Idempotence: $C \sqcap C = C$

* Unit: $C \sqcap \top = C$

* Homomorphism: $\forall r.(C_1 \sqcap C_2) = \forall r.(C_2) \sqcap \forall r.(C_1)$

These axioms define what is known as the ACIUh theory.
## 3 Unification problem in $\mathcal{FL}_{\perp}$

In order to define a unification problem, we partition the set of concept names $N_C$ into two disjoint sets: variables (Var) and constants (Cons). A variable is thus a concept name that may be replaced by any concept while a constant is a concept name that cannot be replaced.

By a *substitution* we understand a mapping from *Var* into the set of all *$\mathcal{FL}_{\perp}$-concepts*. This mapping is extended to all concepts in the obvious way, i.e., $\sigma(A) := A$ for a constant $A \in N_C$; $\sigma(\top) := \top$, $\sigma(\bot) := \bot$; $\sigma(C \sqcap D) := \sigma(C) \sqcap \sigma(D)$; $\sigma(\forall r.C) := \forall r.\sigma(C)$.

In other words, a substitution, as a mapping, provides a definition for a concept name in the set *Var*, and application of a substitution to a concept means eliminating a defined concept name with the right side of the definition. For a given subsumption $C \sqsubseteq D$, the expression $\sigma(C \sqsubseteq D)$ is used as an abbreviation for $\sigma(C) \sqsubseteq \sigma(D)$.

The unification problem is then defined as a set of possible equivalences,

$\Gamma = \{C_1 \equiv? D_1, \dots, C_n \equiv? D_n\}$. Since equivalence and subsumption are definable with each other, we simplify the problem to the general form: $\Gamma' = \{E_1 \sqsubseteq? F_1, \dots, E_m \sqsubseteq? F_m\}$. Moreover, due to the reductions and properties of subsumption we simplify the problem once more to the different general form:

$\Gamma'' = \{G_1 \sqsubseteq? P_1, \dots, G_k \sqsubseteq? P_k\}$, where $G_1, \dots, G_k, P_1, \dots, P_k$ are reduced concepts and $P_1, \dots, P_n$ are particles constructed over $N_C$ and $N_R$, hence they can contain concept names from *Var*. For a given unification problem $\Gamma$, the expression $\sigma(\Gamma)$ is used as an abbreviation for $\{\sigma(C \sqsubseteq D) \mid C \sqsubseteq D \in \Gamma\}$.

A unifier (or solution) of the problem is a substitution for variables that make the possible subsumptions into true subsumptions between the concepts. This means that a substitution $\sigma$ is a unifier for the problem $\Gamma = \{C_1 \sqsubseteq? P_1, \dots, C_n \sqsubseteq? P_n\}$ iff $\sigma(C_1 \sqsubseteq P_1), \dots, \sigma(C_n \sqsubseteq P_n)$. If there is a unifier for $\Gamma$, we say that the problem is *unifiable*.

Let $\Gamma$ be a unification problem with the set of variables $V$ and unifiers $\sigma, \gamma$. We say that $\sigma$ is *more general* than $\gamma$ (or $\gamma$ is *less general* than $\sigma$), if there is a substitution $\tau$ such that $\gamma(X) \equiv \tau(\sigma(X))$, for all $X \in V$. If a unifier is more general than any other unifier, we call it a *most general unifier* (an mgu) of $\Gamma$.

A set $\Pi$ of unifiers of a given unification problem $\Gamma$ is called a *complete set of unifiers* if every unifier of $\Gamma$ is less general than some element of $\Pi$.

For a given unification problem $\Gamma$ we define four *unification types* (from "best" to "worst") based on the existence and cardinality of its complete set. The problem has unification type *unitary* if there exists a complete set of unifiers consisting of one unifier $\sigma$. In this case $\sigma$ is a most general unifier of $\Gamma$; *finitary* if it has a finite complete set of unifiers, but has no most general unifier; *infinitary* if it has an infinite minimal complete set of unifiers; *nullary* (or *zero*) if it has no minimal complete set of unifiers. The unification type of a logic ($\mathcal{FL}_{\perp}$ in our case) is the worst unification type of its unifiable problems. We show that the description logic $\mathcal{FL}_{\perp}$ has nullary unification type.

## 4 Type nullary result

In this section we prove the following.

**Theorem 4.1.** *$\mathcal{FL}_{\perp}$ has nullary unification type.*

We show that the unification problem $\Gamma = \{X \sqsubseteq \forall r.X\}$ has no minimal complete set of unifiers. For this reason we introduce the following substitutions.
**Definition 4.2.** $\sigma_0(X) = \perp$; $\sigma_n(X) = X \sqcap \forall r.X \sqcap \dots \sqcap \forall r^{n-1}.X \sqcap \forall r^n.\perp$, for $n \ge 1$; $\sigma_\top(X) = \top$.

The set of all substitutions defined above will be denoted by $U$. The substitutions in $U$ are unifiers of $\Gamma$. We show this fact in the following lemma.

**Lemma 4.3.** $\sigma_\alpha$ is a unifier of $X \sqsubseteq \forall r.X$, for each $\alpha \in \mathbb{N} \cup \{\top\}$.

*Proof.* The lemma is obvious for $\alpha \in \{0, \top\}$. Let $n \ge 1$ be fixed. We will show that $\sigma_n(X) \sqsubseteq \forall r.\sigma_n(X)$. Since $\forall r.\sigma_n(X) = \forall r.X \sqcap \dots \sqcap \forall r^{n-1}.X \sqcap \forall r^n.X \sqcap \forall r^{n+1}.\perp$, we have to show that

$$\sigma_n(X) \sqsubseteq \forall r.X, \quad \sigma_n(X) \sqsubseteq \forall r^2.X, \dots, \sigma_n(X) \sqsubseteq \forall r^{n-1}.X,$$

$$\sigma_n(X) \sqsubseteq \forall r^n.X, \quad \sigma_n(X) \sqsubseteq \forall r^{n+1}.\perp.$$

Since $\sigma_n(X) = X \sqcap \forall r.X \sqcap \dots \sqcap \forall r^{n-1}.X \sqcap \forall r^n.\perp$, the above subsumptions of the form $\sigma_n(X) \sqsubseteq \forall r^k.X$ are obvious for each $1 \le k \le n-1$, because the right side of the subsumption is a part of the left side. The subsumption $\sigma_n(X) \sqsubseteq \forall r^n.X$ holds because $\forall r^n.\perp \sqsubseteq \forall r^n.X$ and the subsumption $\sigma_n(X) \sqsubseteq \forall r^{n+1}.\perp$ holds because $\forall r^n.\perp \sqsubseteq \forall r^{n+1}.\perp$.

□

Now we show that the set of unifiers defined in Definition 4.2 is complete.

**Lemma 4.4.** Let $\sigma$ be a unifier of $X \sqsubseteq \forall r.X$ not equal to $\sigma_\top$. Let $\sigma_n$ be as defined in Definition 4.2 where $n = \mathrm{rd}(\sigma(X))$. Then $\sigma(X) \equiv \sigma(\sigma_n(X))$.

*Proof.* Since $\sigma$ is a unifier of $X \sqsubseteq \forall r.X$,

$$\sigma(X) \sqsubseteq \sigma(X) \sqcap \forall r.\sigma(X) \sqcap \dots \sqcap \forall r^{n-1}\sigma(X). \quad (1)$$

By Lemma 2.3, since $\sigma(X)$ is not $\top$, we have

$$\sigma(X) \sqsubseteq \forall r^n.\perp. \quad (2)$$

From (1) and (2)

$$\sigma(X) \sqsubseteq \sigma(X) \sqcap \forall r.\sigma(X) \sqcap \dots \sqcap \forall r^{n-1}.\sigma(X) \sqcap \forall r^n.\perp \equiv \sigma(\sigma_n(X)).$$

By the fact that $\sigma(X)$ is a member of the right side of the above subsumption, the two sides are equivalent. □

Up to this point, we have shown that $U$ is a complete set of unifiers for $\Gamma$. To complete the argument, we now show that there is no minimal complete set of unifiers for $\Gamma$.

**Lemma 4.5.** $\sigma_{n+1}$ is more general than $\sigma_n$, but $\sigma_n$ is not more general than $\sigma_{n+1}$, for each $n \ge 0$.

*Proof.* Similarly to the proof of Lemma 4.3, we use the fact that, for each $k$, $\forall r^k.\perp \sqsubseteq \forall r^k.X$ and $\forall r^k.\perp \sqsubseteq \forall r^{k+1}.\perp$ to show that $\sigma_n(\sigma_{n+1}(X)) \equiv \sigma_n(X)$. This implies that $\sigma_{n+1}$ is more general than $\sigma_n$.

Since $\tau(\sigma_n(X)) \sqsubseteq \forall r^n.\perp$, for any substitution $\tau$, and $\sigma_{n+1}(X) \sqsupseteq \forall r_n.\perp$, then $\sigma_n$ cannot be more general than $\sigma_{n+1}$. □

**Theorem 4.6.** The type of the unification problem $\Gamma$ is nullary.
*Proof.* The proof is by contradiction. Assume that $U'$ is a minimal complete set of unifiers of $\Gamma$ and $\tau \in U'$ is not equal to $\sigma_{\tau}$. Then, by Lemma 4.4, there is $\sigma_n \in U$, for some $n \in \mathbb{N}$, more general than $\tau$. By Lemma 4.5, $\sigma_{n+1}$ is more general than $\sigma_n$ and $\sigma_n$ is not more general than $\sigma_{n+1}$. By the assumption, there exists $\gamma \in U'$ more general than $\sigma_{n+1}$. By transitivity composition, $\gamma$ is more general than $\tau$. Thus $\gamma = \tau$. But in this case $\sigma_n$ is more general than $\gamma$ and, by transitivity, $\sigma_n$ is more general than $\sigma_{n+1}$. Contradiction. $\square$

# 5 Conclusions

In this paper, we have shown that unification in $\mathcal{FL}_{\perp}$ has type nullary (or type zero). Hence, it has the same type as the known types of other sub-boolean description logics: $\mathcal{EL}$, $\mathcal{FL}_0$. It is easy to see that the nullary type of $\mathcal{FL}_0$ is inherited by $\mathcal{FL}\mathcal{E}$, which combines $\mathcal{EL}$ and $\mathcal{FL}_0$. From the nullary type of the modal logic $\mathcal{K}$, proved by Jerábek in [3], it follows that this is also the type of the boolean logic $\mathcal{ALC}$.

# References

[1] Franz Baader. Unification in commutative theories. *J. Symb. Comput.*, 8(5):479–497, 1989.

[2] Franz Baader and Paliath Narendran. Unification of concept terms in description logics. *Journal of Symbolic Computation*, 31(3):277–305, 2001.

[3] Emil Jerábek. Blending margins: the modal logic $\mathcal{K}$ has nullary unification type. *J. Log. Comput.*, 25(5):1231–1240, 2015.