Approximate Unification in the
                         Description Logic F L0

         Franz Baader1? , Pavlos Marantidis1?? , and Alexander Okhotin2
       firstname.lastname@tu-dresden.de, alexander.okhotin@utu.fi
                  1
                   Theoretical Computer Science, TU Dresden, Germany
            2
                Chebyshev Laboratory, St. Petersburg State University, Russia

Unification in DLs has been introduced as a novel inference service that can be
used to detect redundancies in ontologies, by finding out whether two concept
descriptions may potentially stand for the same concept. Intuitively, one assumes
for this that certain concept names occurring in the concept descriptions stand
for concepts that are not yet fully defined, and unification checks whether it is
possible to supply definitions for them that make the two concept descriptions
equivalent. Unification of concept descriptions was first introduced for the DL
FL0 in [1], where it was shown to be ExpTime-complete. The ExpTime upper
bound was proved by a reduction to solving certain language equations, which
in turn were solved using tree automata. In order to increase the recall of this
method for finding redundancies, we introduce and investigate the notion of
approximate unification. In contrast to exact unification, approximate unification
is not required to make the concept descriptions equivalent, but only “similar,”
where similarity is formalized using concept distances, i.e., functions that assign
non-negative real numbers to pairs of concept descriptions. We show that the
approach of [1] for exact unification can be extended to approximate unification.
In fact, by linking concept distances with language distances, we can reduce
approximate unification in FL0 to approximately solving language equations. In
order to reduce this problem to a problem for tree automata, we do not employ
the original construction of [1], but the more sophisticated one of [2]. We provide
procedures for solving the problem w.r.t. two particular language distances. The
problem for the first distance translates to a reachability problem in the tree
automaton constructed from the language equation. For the second distance, we
derive from the tree automaton a system of equations over the real numbers,
which can be solved using Linear Programming techniques. For both distances,
the complexity of approximate unification is the same as for exact unification.
    This paper was accepted and presented in JELIA 2016, in Larnaca, Cyprus.

References
1. Baader, F., Narendran, P.: Unification of concept terms in description logics. J. of
   Symbolic Computation 31(3), 277–305 (2001)
2. Baader, F., Okhotin, A.: On language equations with one-sided concatenation. Fun-
   damenta Informaticae 126(1), 1–35 (2013)

 ?
     Supported by the Cluster of Excellence ‘Center for Advancing Electronics Dresden’.
??
     Supported by DFG Graduiertenkolleg 1763 (QuantLA).