In this paper, we present FILO, the first application that decides the unification problem for the description logic ℱ ℒ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 that can help eliminate redundancies in ontologies. The unification problem in ℱ ℒ0 is ExpTime-complete. FILO is based on an algorithm that is exponential only in the worst case. The algorithm used by FILO is based on the one described in [1].
2. The description logic ℱ ℒ0 Complex concepts in ℱ ℒ0 are constructed from a countable set of concept names (unary predicates) N and a countable set of role names (binary relations) R according to the following grammar: ::= | ⊓ | ∀. | ⊤, where ∈ N and ∈ R.
An interpretation is a pair (Δ , · ), where Δ is a non-empty domain and · is an interpretation function. The interpretation of concept names ( ⊆ Δ ) and role names ( ⊆ Δ × Δ ) is extended to all concepts in the standard way: (1 ⊓ 2) = 1 ∩ 2 , (∀.) = { ∈ Δ | ∀∈Δ ((, ) ∈ =⇒ ∈ )}, ⊤ = Δ .. We define ⊑ if for every interpretation , ⊆ and ≡ if ⊑ and ⊑ .
We write ∀1.∀2. . . . ∀. as ∀., where is a word over R, and call such a concept a particle. With respect to the equivalence, one can easily observe that the intersection of concepts is associative, commutative, idempotent and has ⊤ as its unit element. The value restriction behaves as a homomorphism: ∀.( ⊓ ) ≡ ∀ . ⊓ ∀. . Thus, each concept can be identified as a set of particles, and the empty set is ⊤.
In ℱ ℒ0, subsumption between two concepts and can be decided in polynomial time. Lemma 1. Let = 1 ⊓ · · · ⊓ and = 1′ ⊓ · · · ⊓ ′. 1. ⊑ if for every 1 ≤ ≤ , 1 ⊓ · · · ⊓ 2. for every 1 ≤ ≤ , 1 ⊓ · · · ⊓
⊑ ′; ⊑ ′ if ′ ∈ {1, · · · , }.
Proof. Both these statements follow from the properties of subsumption that establish a partial order with respect to the sets of particles.
In order to define a unification problem in ℱ ℒ0, we divide the set of concept names N into two disjoint sets: constants, denoted C and variables, denoted Var. Variables may be substituted by concepts, and constants cannot be substituted.
A substitution is a mapping initially defined for Var, assigning to them possibly complex concepts. It is then extended to all concepts in the usual way: () := , where ∈ C, ( ⊓ ) := ()⊓ ( ), (∀.) := ∀. (), (⊤) := ⊤.
The unification problem is then defined by its input and output as follows.
Input: Γ = {1 ⊑? 1, . . . , ⊑? }, where 1 . . . , 1 . . . are ℱ ℒ0-concepts constructed over constants and variables. We call ⊑? ∈ Γ an input goal. Due to Lemma 1, we can assume that for each input goal ⊑? , is a particle.
Output: “true” if there is a substitution such that (1) ⊑ (1), . . . , () ⊑ () and “false” otherwise. The substitution is called a unifier or a solution of Γ.
FILO is an application written in Java using the OWL API and Maven for dependency management. As of now it is a standalone application (FILO.jar). The compiled file is available at https://unifdl.cs. uni.opole.pl/unificator-app-for-the-description-logic-fl_0/ and the source files are available in a public GitHub repository https://github.com/barbmor/FILO.
A unification problem which can be solved by FILO must be provided in the form of an ontology file. Such an ontology may be created using the ontology editor Protégé1. The concept names in such an ontology are treated by FILO as constants, unless they have the _var sufix. Input goals are defined as general class axioms or as concept subsumptions expressed through class hierarchy statements. FILO recognizes concept names (constants and variables), intersections of concepts, value restrictions and the ⊤ constructor. It reports an error if an unsupported constructor is encountered while reading the input file.
FILO is based on the algorithm presented in [
Nevertheless, the algorithm in [
During this stage, the internal structures representing concepts from the input ontology are created. Concept intersections from the input are represented by sets of flat particles of the form ∀., where is a variable or a constant. The internal representation of the input after Flattening I is called a Filo model.
Example 1. Let an input goal in the notation of ℱ ℒ0 be: ∀.1 ⊓ ∀.2 ⊓ ∀. ⊓ ∀.2 ≡ ? ∀.1 ⊓ ∀.2 ⊓ ∀. (Example 16 in FILO). After the Flattening I stage, we get the following set of equivalences: 2 ≡ ∀ .1, 5 ≡ ∀ .2, 0 ≡ ∀ .2, 6 ≡ ∀ ., 4 ≡ ∀ . 2, 1 ≡ ∀ .2, 3 ≡ ∀ . 1, ∀. 4 ⊓ ∀. ⊓ ∀. 0 ⊓ ∀. 3 ≡ ∀ . 5 ⊓ ∀.1 ⊓ ∀. 6.
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 ⊤. Otherwise, FILO attempts to solve the problem for each
constant separately–in the manner presented in [
Depending on the current constant, FILO performs further flattening. The goal of this stage is to obtain lfat subsumptions of the form 1 ⊓ · · · ⊓ ⊑? , where all of the concept names are variables or the current constant, and additional increasing subsumptions of the form ⊑ ∀.. The set of flat ? subsumptions and increasing subsumptions is called a generic goal.
Example 2. Following Example 1, flattening II yields the generic goal w.r.t. the constant 2: lfat subsumptions : 2 ≡ ⊤ , 5 ≡ 2, 0 ≡ 2, 6 ≡ , 4 ≡ ⊤ , 1 ≡ 2, 3 ≡ 1, 4 ⊓ ⊓ 0 ⊓ 3 ⊑ 5, 4 ⊓ ⊓ 0 ⊓ 3 ⊑ 6, 5 ⊓ 6 ⊑ 4, 5 ⊓ 6 ⊑ , 5 ⊓ 6 ⊑ 0, 5 ⊓ 6 ⊑ 3; increasing subsumptions: 5 ⊑ ∀. 5, 0 ⊑ ∀. 0, 6 ⊑ ∀. 6, 1 ⊑ ∀. 1, 3 ⊑ ∀. 3, where 5, 0, 6, 1, 3 are decomposition variables. Note that 4 is ⊤ since 2 is.
Now FILO has to make choices for each variable predicting their values in a solution: TOP if it is an empty conjunction, or CONSTANT if some of the particles contained in a solution is the current constant, or NEITHER otherwise. If there are no variables, only the current constant, FILO checks solvability of the generic goal by Implicit Solver (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 appropiate relations. Hence, here FILO enters another loop.
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. If the set of flat subsumptions is empty, FILO returns success for the current constant. If there are no choices left, the loop for choices is ended and the program returns failure. Let us fix the current consistent choice.
Example 3. Continuing with Example 2, FILO searches for a consistent choice, and finds: { 2, 4} ↦→ , { 5, 0, 1} ↦→ and the rest of variables is NEITHER.
For this choice, 2 ≡ ⊤ , 5 ≡ 2, 0 ≡ 2, 4 ≡ ⊤ , 1 ≡ 2, 5 ⊓ 6 ⊑ 4 are trivially satisfied. For the last subsumption, note that its right-hand is TOP. The rest of subsumptions is already flat.
If the set of flat subsumptions is not empty, FILO starts computation with shortcuts, i.e. sets of variables that satisfy all the flat subsumptions of the goal. It enters a loop computing shortcuts. Now, FILO attempts to extend the set of already computed shortcuts using the so-called resolving relation: is resolved by ′ w.r.t. a role name if ∈ implies ∈ ′ and if is defined for ∈ ′, then ∈ . If the initial shortcut, i.e. the set of the form { | is assigned the choice CONSTANT}, is computed, this means success for the current constant–FILO aborts computing new shortcuts. Otherwise, if the initial shortcut cannot be reached, it means failure for the current choice. Example 4. Continuing with Example 3, a shortcut of height 0, i.e. without decomposition variables, is { 6, 3}. Then, FILO proceeds to compute next shortcuts: {, 5, 0, 1, 3, 6, 3} and { 1, 5, 0} which is also the initial shortcut. At this moment, the computation is terminated with success for the given constant. The partial solution is: { 1, 5, 0} ↦→ 2, {, 5, 0, 1, 3, 6, 3} ↦→ ∀.2, { 6, 3} ↦→ ∀.2.
Assuming we obtain the partial solution for the constant 1: {, 2, 6} ↦→ 1, {, 6, 4, 2, 6, 4} ↦→ ∀.1, { 4, 6} ↦→ ∀.1, we obtain the following solution for the input goal: ↦→ ∀.2 ⊓ 1 ⊓ ∀.1.
FILO provides more than 20 examples, available in the dropdown menu in its interface. Among the
examples, Example 16 is taken from [
Out of the examples provided, Example 8 is most dificult. It contains two constants and is not unifiable for either of them. Hence it terminates with failure after checking the generic goal produced for one constant only. Nevertheless it takes 7545 ms to terminate. The maximal number of variables is 33 and 1525 goals are rejected in the pre-processing stage, while the shortcuts were computed 12 times.
During the preparation of this work, the authors used ChatGPT based on GPT-4o in order to: Grammar and spelling check. After using this tool, the authors reviewed and edited the content as needed and take full responsibility for the publication’s content.