# FILO: unication solver for FL0

Barbara Morawska, Slawomir Kost, Dariusz Marzec, Michal Henne

## ► To cite this version:

Barbara Morawska, Slawomir Kost, Dariusz Marzec, Michal Henne. FILO: unication solver for FL0. UNIF 2025 - 39th International Workshop on Unification, Jul 2025, Birmingham, United Kingdom. hal-05148721

HAL Id: hal-05148721

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

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>
FILO: unification solver for $\mathcal{FL}_0$

Barbara Morawska¹, Sławomir Kost¹, Dariusz Marzec¹, and Michał Henne¹

Institute of Computer Science, University of Opole, Oleska 48, Opole 45-052, Poland
{barbara.morawska, skost, dariusz.marzec, michal.henne}@uni.opole.pl

**Abstract**

In this paper, we present FILO, the first application that decides the unification problem for the description logic $\mathcal{FL}_0$. This is a restricted description logic that allows only conjunction, the top constructor and value restrictions to construct complex concepts from a set of concept names (unary predicates) and role names (binary predicates). Unification of concepts in description logics has been proposed as a non-standard reasoning task—the standard ones being subsumption and consistency checking—that can help eliminate redundancies from ontologies. Unification problem in $\mathcal{FL}_0$ is EXPTIME-complete, therefore FILO is based on an algorithm that is exponential only in the worst case.

# 1 Introduction

Description Logics (DLs) are a formalism used to represent knowledge in a given domain. Usually, this knowledge is stored in the form of an ontology, a large set of definitions of concepts. DLs describe, in a formal way, how complex concepts can be constructed from simpler expressions, i.e. concept names and role names (binary relations). DLs differ from each other by providing different sets of constructors that can be used to construct complex concepts. The description logic $\mathcal{FL}_0$ is a member of a family of small description logics with restricted expressive power. It only provides the intersection (conjunction) constructor $\cap$, the $\top$ constructor, and the value restriction of the form $\forall r.C$, where C is a concept and r is a role name.

The unification problem in DLs was, in fact, first defined for our logic $\mathcal{EL}$. It was shown in [8] to be an EXPTIME-complete problem. The algorithm presented there reduced the problem to the emptiness problem for a root-to-frontier automaton on trees, which showed the exponential upper bound. The lower bound was established in the same paper, by reduction from the intersection problem for root-to-frontier automata on trees, [12]. Since the automaton is of size exponential in the size of a unification problem, this showed the exponential upper bound. For some reasons, this algorithm was never implemented. One of them was perhaps that the focus of researchers turned to another small DL, namely to $\mathcal{EL}$ which does not have a value restriction constructor but provides instead an existential restriction: $\exists r.C$. Unification of concepts formulated in $\mathcal{EL}$ was solved in [7] and shown to be an NP-complete problem. There are at least two algorithms, one a goal-directed based on inference rules [2] and the other based on a SAT-reduction [3], that establish the upper bound. The algorithms for solving unification in $\mathcal{EL}$ were automatized as a Java application UEL [6].

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 Union's Horizon 2020 research and innovation programme under the Marie Skłodowska-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>
In [9], we have revisited the unification algorithm for $\mathcal{FL}_0$ and developed a new one, based on reduction to a problem of finding finite Herbrand models for a set of anti-Horn clauses, which seemed a bit analogous to the SAT-reduction on the side of $\mathcal{EL}$. Now, we come back to that algorithm, and revise it again [11] (the extended version of this paper), so that it can be implemented. Our implementation called FILO works on unification problems in the form of ontology files, where variables are marked with the _var suffix. If it detects that an input problem is unifiable, it will output a unifier that can be extracted from its computations. FILO is the first application to solve unification in $\mathcal{FL}_0$, it joins a family of similar applications like UEL [1] solving unification problems in the description logic $\mathcal{EL}$, $\mathcal{FL}_0$-wer [4], a subsumption decider for $\mathcal{FL}_0$ with TBox, CEL [5] and JCEL [10] subsumption deciders for $\mathcal{EL}$ with TBox, and others. These systems play an important role in various knowledge representation reasoning problems.

## 2 The description logic $\mathcal{FL}_0$

The description logic $\mathcal{FL}_0$ deals with concepts constructed from a countable set of *concept names* (unary predicates) **N** and a countable set of *role names* (binary predicates) **R**. Concepts are generated by the following grammar: $C ::= A \mid C \sqcap C \mid \forall r.C \mid \top$, where **A** is an arbitrary element of **N** and **r** is an element of **R**.

An interpretation $I$ is a pair $(\Delta^I, .^I)$, where $\Delta^I$ is a non-empty domain and $.^I$ is an interpreting function such that a concept name $A$ is interpreted by $A^I \subseteq \Delta^I$, and a role name $r$ is interpreted by $r^I \subseteq \Delta^I \times \Delta^I$. This interpretation is extended to all $\mathcal{FL}_0$-concepts as usual: $(C_1 \sqcap C_2)^I = C_1^I \sqcap C_2^I$, $(\forall r.C)^I = \{e \in \Delta^I \mid \forall d \in \Delta^I ((e, d) \in r^I \implies d \in C^I)\}, \top^I = \Delta^I$.

Based on this semantics, we define a subsumption relation between a pair of concepts $C \sqsubseteq D$ iff for every interpretation $I$, $C^I \subseteq D^I$. The equivalence of concepts is then defined as subsumption in both directions: $C \equiv D$ iff $C \sqsubseteq D$ and $D \sqsubseteq C$.

With respect to equivalence, one can easily notice that the intersection of concepts is associative, commutative, has $\top$ as its unit and it is idempotent. The value restrictions behave as homomorphisms: $\forall r.(C_1 \sqcap C_2) \equiv \forall r.C_1 \sqcap \forall r.C_2$.

Due to these properties, each concept is equivalent to a conjunction of concepts of the form: $\forall r_1.\forall r_2.\dots\forall r_n.A$, where $r_1, \dots, r_n$ are (not necessarily different) role names and $A$ is a concept name. For brevity, we write $\forall v.A$, where $v$ is a word over **R**, and call such a concept a *particle*. Hence, each concept is equivalent to a conjunction of particles, each conjunction is identified with a set and an empty conjunction is considered to be $\top$. Moreover, each concept can be represented in such a way that no one of the following *reduction rules* applies to particles: $C \sqcap \top \leadsto C$, $\top \sqcap C \leadsto C$, or $\forall v.\top \leadsto \top$. We call such a concept (a conjunction of particles) a concept in normal form. Below we will assume that each concept is in normal form.

In $\mathcal{FL}_0$, subsumption between two concepts $C$ and $D$ can be decided in polynomial time.

**Proposition 1.** Let $C = P_1 \sqcap \dots \sqcap P_m$ and $D = P'_1 \sqcap \dots \sqcap P'_n$.

1. $C \sqsubseteq D$ iff for every $1 \le i \le n$, $P_1 \sqcap \dots \sqcap P_m \sqsubseteq P'_i$

2. for every $1 \le i \le n$, $P_1 \sqcap \dots \sqcap P_m \sqsubseteq P'_i$ iff $P'_i \in \{P_1, \dots, P_m\}$.

*Proof.* Both statements follow from the properties of subsumption that establish a partial order with respect to the sets of particles. $\square$

The next proposition justifies dividing decision of a subsumption relation between two concepts into a set of decisions of smaller subsumptions that are restricted w.r.t. different constants. For a concept $C$, we define its *restriction* w.r.t. a concept name $A$ as $C_A = \bigcap \{\forall v.A \mid \forall v.A \in C\}$.
**Proposition 2.** Let $C = P_1 \sqcap \cdots \sqcap P_m$ and $D = P'_1 \sqcap \cdots \sqcap P'_n$. Then $C \subseteq D$ iff for every $A \in \mathbb{N}$, $C_A \subseteq D_A$.

*Proof.* The conclusion follows directly from Proposition 1. □

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

# 3 The unification problem

In order to define a unification problem in $\mathcal{FL}_0$, we have to decide which of the concept names are variables and which are constants. The variables may be substituted by concepts and constants cannot be substituted. Hence we divide concept names $\mathbb{N}$ into two disjoint sets $\mathcal{C}$ which will be called *constants* and *Var*, *variables*.

A *substitution* is a mapping defined first for variables, assigning to them possibly complex concepts. It is then extended to all concepts in a usual way.

A unification problem is then defined by its input and output as follows.

**Input:** $\Gamma = \{C_1 \sqsubseteq? D_1, \dots, C_n \sqsubseteq? D_n\}$, where $C_1 \dots C_n, D_1 \dots D_n$ are $\mathcal{FL}_0$-concepts constructed over constants and variables. We call $C \sqsubseteq? D \in \Gamma$ an *input goal*.

**Output:** “true” if there is a substitution $\gamma$ such that $\gamma(C_1) \sqsubseteq \gamma(D_1), \dots, \gamma(C_n) \sqsubseteq \gamma(D_n)$ and “false” otherwise. The substitution $\gamma$ is called a *unifier* or a *solution* of $\Gamma$.

Due to Proposition 1, we can assume that for each input goal, $C \sqsubseteq? D$, $D$ is a particle.

# 4 Solver

FILO is an application written in Java using OWL API<fnref n="1" /> and Maven<fnref n="2" /> for a dependency management. As for now it is a standalone application (FILO.jar). The application can be easily opened by double-clicking the file (Windows) or running `java -jar Filo.jar` in the command line (Linux). The compiled file is available at https://unifdl.cs.uni.opole.pl/unificato r-app-for-the-description-logic-fl_0/ and the source files are available at the public GitHub repository https://github.com/barbmor/FILO.

The main application window is divided into three sections. The input section allows the user to select a predefined test from the dropdown menu or choose an ontology file with an `.owx` or `.owl` extension. Such an ontology may be created using the ontology editor, Protégé<fnref n="3" />. Concept names in such an ontology are treated by FILO as constants, unless they have the `_var` suffix.

The output section shows the results of the unification process, including discovered unifier and/or relevant message.

The options panel provides controls for setting the type of log messages – they can be more (FINE option) or less detailed (INFO option) – as well as buttons to save the log file (Save log file) and to display diagnostic data (Show statistics) which contains basic information about the computation, for example, the maximal number of variables which is the number of variables in a generic goal created during computation, or the time of computation (given in milliseconds). This data may indicate the difficulty of a unification problem.

## 4.1 Overview of FILO computation

Having opened the input file, FILO performs the following actions automatically.

<footnote n="1">¹http://owlcs.github.io/owlapi/</footnote>

<footnote n="2">²https://maven.apache.org/</footnote>

<footnote n="3">³https://protege.stanford.edu/</footnote>
1. **Flattening I.** During this stage, an internal representation of the input, called a *Filo model*, and internal structures representing concepts from the input ontology are created. Concept intersections from the input are represented by sets of *flat particles*, i.e. particles of the form $\forall r.C$, where *C* is a variable or a constant. This is illustrated in Example 1.

2. **Main Loop.** After successfully reading the input and creating a Filo model, FILO enters a loop: *for each constant* in the model. If there are no constants, only variables, then FILO returns success and the problem has a solution sending all variables to $\top$. Otherwise, FILO attempts to solve the problem for each constant *separately* (in the manner presented in Proposition 2) and if it returns **failure** for any one of them, it breaks the main loop immediately returning **failure**. Such a problem is not unifiable. Let us fix the *current constant* *A*.

(a) **Flattening II** Depending on the current constant, FILO performs further flattening. The goal of this stage is to obtain flat subsumptions of the form $X_1 \sqcap \cdots \sqcap X_n \sqsubseteq Y$, where all of the concept names are variables or the current constant *A*. For implementation reasons, we allow the current constant to be one of $X_i$. The set of flat subsumptions and additional *increasing subsumptions* of the form $X \sqsubseteq^? \forall r.X^r$, where $X^r$ is a *decomposition variable* and *X* is the *parent* variable for $X^r$. The set of flat subsumptions and increasing subsumptions is called *generic goal*. This is further explained in Example 2.

(b) **Choices Loop** Now FILO has to make choices for each variable. Should it be equal to $\top$, TOP? If not, does it contain the current constant, CONSTANT? If not, it has the choice NEITHER, which means that it will certainly not contain the current constant in the solution, but it is also not assumed to be $\top$. If there are no variables, only the constant *A*, FILO checks solvability of the generic goal by Implicit Solver, vide (i) and (ii) (it must return either **success** or **failure**). Otherwise, FILO checks all *consistent* choices for all variables in the generic goal, i.e. choices in which the decomposition variables and their parents satisfy appropriate relations. Hence, here FILO enters another loop. If there are no choices left, the loop for choices is ended and the program returns **failure**. Let us fix the current consistent choice.

i. For this choice, FILO analyses the subsumptions in the generic goal and attempts to create a **goal**, i.e. a set of flat subsumptions, increasing subsumptions, and so-called *start subsumptions* of the form $X \sqsubseteq? A$ (*A* is the current constant) which are created for all variables for which the current choice assigns CONSTANT. During this process, Implicit Solver checks which subsumptions are solved by the current choice for variables. It may also detect contradictions. If this is the case, FILO aborts the computation, returns **failure** for the current choice and proceeds to check the next choice and starting from the generic goal, to construct another goal again. This step is illustrated by Examples 3 and 4.

ii. If the set of flat subsumptions is empty, i.e. Implicit Solver detects that the subsumptions are already solved, the computation is aborted and FILO returns **success** for the current constant. FILO then returns to the main loop, to start computations for the next constant. If there are no constants left, FILO returns **success**.

iii. **Shortcuts loop** If the set of flat subsumptions is not empty, FILO starts computation with shortcuts, i.e. sets of variables that have certain properties. This means that it enters a loop computing all necessary shortcuts. If the *initial shortcut*, i.e. a shortcut of the form: $\{X \mid X \sqsubseteq? A\}$ is a start subsumption $\} \cup \{A\}$
is computed, FILO returns **success** for the current constant. Otherwise, after computing all possible shortcuts, it returns **failure** for the current choice. This step is illustrated by Example 5.

The input problem is unifiable if either it contains no constants, or for each constant, there exists a choice for which FILO returns **success** (either by Implicit Solver or computing shortcuts).

## 4.2 Flattening I – reading input

During Flattening I, new system variables are created. One can see the Filo model in the log file if the logging option is set to FINE.

**Example 1.** Let an input goal in the notation of $\mathcal{FL}_0$ be: $\forall r(\forall r(A \sqcap B) \sqcap C) \sqcap \forall s.(A \sqcap C) \sqsubseteq A \sqcap \forall s.(\forall r(A \sqcap C) \sqcap B)$. After the Flattening I stage, we get the following set of subsumptions and equivalences:

$$ \forall r.C \sqcap \forall r.Var0 \sqcap \forall r.Var1 \sqcap \forall s.C \sqcap \forall s.A \sqsubseteq \forall s.Var3 \sqcap A \sqcap \forall s.B \sqcap \forall s.Var2, $$

$$ Var0 \equiv \forall r.A, Var1 \equiv \forall r.B, Var2 \equiv \forall r.A, Var3 \equiv \forall r.C. $$

## 4.3 Flattening II – creating generic goal

During Flattening II, FILO makes sure that if there is a solution $\gamma$ for the unification problem, $\gamma(X^r) = \bigcap\{P \mid \forall r.P \in \gamma(X)\}$, where P is a particle. $\gamma(X^r) = \top$ if no such P exists. With respect to a given constant A, FILO may introduce for a variable X a constant decomposition variable, $X_A$. This variable should be either $\top$ or $\gamma(X_A) = A$ iff $A \in \gamma(X)$. FILO creates decomposition variables and constant decomposition variables only if it is necessary to obtain flat subsumptions.

**Example 2.** Let our problem be:

$$ \Gamma = \{X \sqsubseteq? \forall r.A, Y \sqcap \forall r.X \sqsubseteq? X, X \sqsubseteq? \forall r.Y\}. $$

Then Flattening II yields the generic goal w.r.t. the constant A:

$$ \text{flat subsumptions: } \{X^r \sqsubseteq? A, Y^r \sqcap X \sqsubseteq? X^r, Y \sqsubseteq? X_A, X^r \sqsubseteq? Y\}, $$

$$ \text{increasing subsumptions: } \{X \sqsubseteq? \forall r.X^r, Y \sqsubseteq? \forall r.Y^r\} $$

where $X^r, Y^r$ are decomposition variables and $X_A$ is a constant decomposition variable.

## 4.4 Choice

FILO has to check for each choice if there is a unifier for the given constant. Therefore, we use a lexicographic order to run through all the guesses. Due to the fact that we have a huge search space for even a small number of variables, we restrict choices by looking only for consistent choices.

**Example 3.** In Example 2, we have 5 variables: $X, X^r, X_A, Y, Y^r$. The first choice is a 5-tuple: $(0, 1, 0, 0, 0)$, where 0 signifies $\top$ and 1 signifies CONSTANT. This choice is not consistent since if $X$ is $\top$, $X^r$ should also be $\top$. A consistent choice for this generic goal is: $(1, 1, 1, 0, 0)$, but the goal defined for this choice is not unifiable, because it forces $X_A$ to be CONSTANT but $Y$ is $\top$, hence $Y \sqsubseteq? X_A$ cannot be unified. This decision is made by Implicit Solver.
## 4.5 Goal

When FILO finds a consistent choice for variables, it tries to create a goal with respect to this choice.

**Example 4.** Continuing with Example 3, FILO searches for a consistent choice, and finds (1, 1, 1, 1, 0). For this choice $X^r \sqsubseteq^? A$ is trivially satisfied. We are left with unsolved flat subsumptions: $Y^r \sqcap X \sqsubseteq^? X^r$, $Y \sqsubseteq^? X_A$, $X^r \sqsubseteq^? Y$. Moreover, we have 4 start subsumptions: $X \sqsubseteq^? A$, $X^r \sqsubseteq^? A$, $X_A \sqsubseteq^? A$, $Y \sqsubseteq^? A$.

## 4.6 Shortcuts loop

Computing with shortcuts is triggered if the set of flat unsolved subsumptions in the goal is not empty. This part is the main reason for the algorithm to be exponentially bounded in the size of the input. A *shortcut* is a non-empty subset $S$ of variables (we allow it to contain the constant too), such that it *satisfies* for each flat subsumption $Y_1 \sqcap \cdots \sqcap Y_n \sqsubseteq^? X$ the following implication: if $X \in S$, then $\{Y_1, \ldots, Y_n\} \cap S \neq \emptyset$.

FILO maintains the set of already computed shortcuts and the set of *good variables*. At first it computes all possible shortcuts that do not contain decomposition variables. The set of *good variables* initially does not contain decomposition variables as well. Next, sets of shortcuts are created recursively. If the parent of a decomposition variable occurs in an already computed shortcut then it is added to *good variables*. A new shortcut $S$, possibly containing decomposition variables but only those that are good, is added to the set of already computed shortcuts if it satisfies an additional property for every role name $r$: there is an already computed shortcut $S'$ such that for each decomposition variable $X^r$ in $S$, $X \in S'$ and for each variable $Y \in S'$ for which a decomposition variable $Y^r$ is defined, $Y^r \in S$. If this property is satisfied, we say that the shortcut $S$ is *resolved w.r.t. to the role r* with the shortcut $S'$.

**Example 5.** Continuing with Example 4, the initial shortcut is $\{A, X, Y, X^r, X_A\}$. A can occur only in the initial shortcut. The only shortcut without decomposition variables is $\{X\}$. Then, FILO proceeds to compute next shortcuts: $\{X, X^r\}$, $\{X, Y, X^r\}$, $\{X, Y, X^r, X_A\}$ and finally, $\{X, Y, X^r, X_A, A\}$ which is also the initial shortcut. At this moment the computation is terminated with success for the given constant. The solution is: $[X \mapsto A \sqcap \forall r.A, Y \mapsto A, X^r \mapsto A, X_A \mapsto A]$.

# 5 Examples

FILO provides more than 20 predefined examples in the dropdown menu. The Example 16 in this set is taken from [8] (page 11), the first paper in which unification in $\mathcal{FL}_0$ was introduced and solved, which contains a unification problem in the form of equivalence: $\forall r(A_1 \sqcap \forall r.A_2) \sqcap \forall rs.X_1 \equiv? \forall rs(\forall s.A_1 \sqcap \forall r.A_2) \sqcap \forall r.X_1 \sqcap \forall rr.A_2$.

FILO computes the same solution that is contained in the paper and its computation takes 3700 ms. During the computation, FILO worked with 29 variables, deciding 1290 goals already in the pre-processing stage, and trying to solve the problem by computing shortcuts 8 times.

We worked on a machine with the following specifications: Intel(R) Core(TM) i7-1355U (1.70 GHz), 32.0 GB RAM, 64-bit operating system, running Windows 11 Pro (24H2).
References

[1] Franz Baader, Stefan Borgwardt, Julian Mendez, and Barbara Morawska. UEL: unification solver for EL. In Yevgeny Kazakov, Domenico Lembo, and Frank Wolter, editors, *Proceedings of the 2012 International Workshop on Description Logics, DL-2012, Rome, Italy, June 7-10, 2012*, volume 846 of CEUR Workshop Proceedings. CEUR-WS.org, 2012.

[2] Franz Baader, Stefan Borgwardt, and Barbara Morawska. A goal-oriented algorithm for unification in EL w.r.t. cycle-restricted tboxes. In Yevgeny Kazakov, Domenico Lembo, and Frank Wolter, editors, *Proceedings of the 2012 International Workshop on Description Logics, DL-2012, Rome, Italy, June 7-10, 2012*, volume 846 of CEUR Workshop Proceedings. CEUR-WS.org, 2012.

[3] Franz Baader, Stefan Borgwardt, and Barbara Morawska. SAT encoding of unification in $\mathcal{ELH}_{R+}$ w.r.t. cycle-restricted ontologies. In Bernhard Gramlich, Dale Miller, and Uli Sattler, editors, *Automated Reasoning - 6th International Joint Conference, IJCAR 2012, Manchester, UK, June 26-29, 2012. Proceedings*, volume 7364 of Lecture Notes in Computer Science, pages 30–44. Springer, 2012.

[4] Franz Baader, Patrick Koopmann, Friedrich Michel, Anni-Yasmin Turhan, and Benjamin Zarrieß. Efficient tbox reasoning with value restrictions using $\mathcal{FL}_0$ower reasoner. *Theory Pract. Log. Program.*, 22(2):162–192, 2022.

[5] Franz Baader, Carsten Lutz, and Boontawee Suntisrivaraporn. CEL - A polynomial-time reasoner for life science ontologies. In Ulrich Furbach and Natarajan Shankar, editors, *Automated Reasoning, Third International Joint Conference, IJCAR 2006, Seattle, WA, USA, August 17-20, 2006, Proceedings*, volume 4130 of Lecture Notes in Computer Science, pages 287–291. Springer, 2006.

[6] Franz Baader, Julian Mendez, and Barbara Morawska. UEL: unification solver for the description logic $\mathcal{EL}$ - system description. In Bernhard Gramlich, Dale Miller, and Uli Sattler, editors, *Automated Reasoning - 6th International Joint Conference, IJCAR 2012, Manchester, UK, June 26-29, 2012. Proceedings*, volume 7364 of Lecture Notes in Computer Science, pages 45–51. Springer, 2012.

[7] Franz Baader and Barbara Morawska. Unification in the description logic $\mathcal{EL}$. *Logical Methods in Computer Science*, 6(3), 2010. Special Issue of the 20th International Conference on Rewriting Techniques and Applications; also available at http://arxiv.org/abs/1006.2289.

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

[9] Stefan Borgwardt and Barbara Morawska. Finding finite Herbrand models. In Nikolaj Bjørner and Andrei Voronkov, editors, *Proc. of the 18th Int. Conf. on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR-18)*, volume 7180 of Lecture Notes in Computer Science, pages 138–152. Springer, 2012.

[10] Julian Mendez. jcel: A modular rule-based reasoner. In Ian Horrocks, Mikalai Yatskevich, and Ernesto Jiménez-Ruiz, editors, *Proceedings of the 1st International Workshop on OWL Reasoner Evaluation (ORE-2012), Manchester, UK, July 1st, 2012*, volume 858 of CEUR Workshop Proceedings. CEUR-WS.org, 2012.

[11] Barbara Morawska, Dariusz Marzec, Sławomir Kost, and Michał Henne. Filo – automated unification in $\mathcal{FL}_0$. https://arxiv.org/abs/2502.14130, 2025.

[12] Helmut Seidl. Haskell overloading is dexptime-complete. *Information Processing Letters*, 52(2):57–60, 1994.