Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

FILO -- automated unification in $\mathcal{FL}_0$

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

TL;DR

FILO provides a practical, executable decision procedure for unification in $\mathcal{FL}_0$, a small description logic with $\top$, conjunction, and value restrictions $\forall r.C$. By flattening inputs into a filo-model and then solving per constant through a structured combination of generic goals, decomposition variables, and a set of choice-based rules, FILO achieves ExpTime termination while offering a concrete unifier when possible. The core advances are the flattening II construction, the notion of generic goals with constant-centered solving, and the shortcut-based unification phase that yields a constructive solution. This work enables automated reasoning over ontologies expressed in $\mathcal{FL}_0$, and it highlights a concrete path from historical exponential unification ideas to a practical Java implementation with tunable diagnostics and outputs.

Abstract

FILO is a java application that decides unifiability for a unification problem formulated in the description logic $\mathcal{FL}_0$. If the problem is unifiable, it presents a user with an example of a solution. FILO joins a family of similar applications like UEL solving unification problems in the description logic $\mathcal{EL}$, $\mathcal{FL}_0$wer a subsumption decider for $\mathcal{FL}_0$ with TBox, CEL and JCEL subsumption deciders for $\mathcal{EL}$ with TBox, and others. These systems play an important role in various knowledge representation reasoning problems.

FILO -- automated unification in $\mathcal{FL}_0$

TL;DR

FILO provides a practical, executable decision procedure for unification in , a small description logic with , conjunction, and value restrictions . By flattening inputs into a filo-model and then solving per constant through a structured combination of generic goals, decomposition variables, and a set of choice-based rules, FILO achieves ExpTime termination while offering a concrete unifier when possible. The core advances are the flattening II construction, the notion of generic goals with constant-centered solving, and the shortcut-based unification phase that yields a constructive solution. This work enables automated reasoning over ontologies expressed in , and it highlights a concrete path from historical exponential unification ideas to a practical Java implementation with tunable diagnostics and outputs.

Abstract

FILO is a java application that decides unifiability for a unification problem formulated in the description logic . If the problem is unifiable, it presents a user with an example of a solution. FILO joins a family of similar applications like UEL solving unification problems in the description logic , wer a subsumption decider for with TBox, CEL and JCEL subsumption deciders for with TBox, and others. These systems play an important role in various knowledge representation reasoning problems.

Paper Structure

This paper contains 15 sections, 13 theorems, 1 equation, 3 figures.

Table of Contents

  1. Introduction
  2. The description logic $\mathcal{FL}_0$
  3. Unification problem
  4. Solver
  5. Input
  6. Reading input -- flattening I
  7. Main loop
  8. Creating generic goal -- flattening II
  9. Choice
  10. Goal
  11. Computing with shortcuts
  12. Complexity and correctness
  13. Output
  14. Examples
  15. Implementation improvements

Key Result

Lemma 1

Let $C=P_1 \sqcap \cdots\sqcap P_m$ and $D=P'_1 \sqcap \cdots \sqcap P'_n$.

Figures (3)

  • Figure 1: FILO interface with statistics window.
  • Figure 2: Flattening of $\Gamma$
  • Figure 3: Implicit Solver

Theorems & Definitions (36)

  • Lemma 1
  • proof
  • Lemma 2
  • proof
  • Example 1
  • Lemma 3
  • Example 2
  • Definition 1
  • Example 3
  • Lemma 4
  • ...and 26 more