=Paper=
{{Paper
|id=Vol-1350/paper-07
|storemode=property
|title=Dismatching
and Local Disunification in EL (Extended Abstract)
|pdfUrl=https://ceur-ws.org/Vol-1350/paper-07.pdf
|volume=Vol-1350
|dblpUrl=https://dblp.org/rec/conf/dlog/BaaderBM15
}}
==Dismatching
and Local Disunification in EL (Extended Abstract)==
https://ceur-ws.org/Vol-1350/paper-07.pdf
Dismatching and Local Disunification in EL
(Extended Abstract)
Franz Baader, Stefan Borgwardt, and Barbara Morawska?
Theoretical Computer Science, TU Dresden, Germany
{baader,stefborg,morawska}@tcs.inf.tu-dresden.de
Motivation
Unification in Description Logics was introduced in [6] as a novel inference service
that can be used to detect redundancies in ontologies. For example, assume that
one developer of a medical ontology defines the concept of a patient with severe
head injury using the EL-concepts
Patient u ∃finding.(Head_injury u ∃severity.Severe), (1)
whereas another one represents it as
Patient u ∃finding.(Severe_finding u Injury u ∃finding_site.Head). (2)
Formally, these expressions are not equivalent, but they are nevertheless meant to
represent the same concept. They can obviously be made equivalent by treating
the concept names Head_injury and Severe_finding as variables, and substituting
them by Injuryu∃finding_site.Head and ∃severity.Severe, respectively. In this case,
we say that the concepts are unifiable, and call the substitution that makes
them equivalent a unifier. In [5], we were able to show that unification in EL
is NP-complete. The main idea underlying the proof of this result is to show
that any solvable EL-unification problem has a local unifier, i.e., a unifier built
from a polynomial number of atoms (concept names or existential restrictions),
which are determined by the unification problem. This yields a brute-force NP-
algorithm for unification, which guesses a local substitution and then checks (in
polynomial time) whether it is a unifier.
Intuitively, a unifier of two EL concepts proposes definitions for the concept
names that are used as variables: in our example, we know that, if we define
Head_injury as Injuryu∃finding_site.Head and Severe_finding as ∃severity.Severe,
then the two concepts (1) and (2) are equivalent w.r.t. these definitions. Of
course, this example was constructed such that the unifier (which is local) pro-
vides sensible definitions for the concept names used as variables. In general, the
existence of a unifier only says that there is a structural similarity between the
two concepts. The developer that uses unification needs to inspect the unifier(s)
to see whether the definitions it suggests really make sense. For example, the sub-
stitution that replaces Head_injury by Patient u Injury u ∃finding_site.Head and
Severe_finding by Patient u ∃severity.Severe is also a local unifier, which however
does not make sense. Unfortunately, even small unification problems like the one
?
Supported by DFG under grant BA 1122/14-1
in our example can have too many local unifiers for manual inspection. We pro-
pose disunification to avoid local unifiers that do not make sense. In addition to
positive constraints (requiring equivalence or subsumption between concepts), a
disunification problem may also contain negative constraints (preventing equiva-
lence or subsumption between concepts). In our example, the nonsensical unifier
can be avoided by adding the dissubsumption constraint
Head_injury 6v? Patient (3)
to the equivalence constraint (1) ≡? (2).
Disunification in DLs is closely related to unification and admissibility in
modal logics [7, 10–15], as well as (dis)unification modulo equational theories [5,
6, 8, 9]. In the following, we shortly describe the ideas behind our work. More
details can be found in [2, 3].
Preliminaries
We designate certain concept names as variables, while all others are constants.
An EL-concept is ground if it contains no variables. We consider (basic) disuni-
fication problems, which are conjunctions of subsumptions C v? D and dissub-
sumptions C 6v? D between concepts C, D.1 A substitution maps each variable
to a ground concept, and can be extended to concepts as usual. A substitution
σ solves a disunification problem Γ if the (dis)subsumptions of Γ become valid
when applying σ on both sides. We restrict σ to a finite signature of concept and
role names and do not allow variables to occur in a solution—it would not make
sense for the new definitions to extend the vocabulary of the ontologies under
consideration, nor to define variables in terms of themselves.
In the following, we consider a flat disunification problem Γ, i.e. one that
contains only (dis)subsumptions where both sides are conjunctions of flat atoms
of the form A or ∃r.A, for a role name r and a concept name A. We denote
by At the set of all such atoms that occur in Γ, by Var the set of variables oc-
curring in Γ, and by Atnv := At \ Var the set of non-variable atoms of Γ. Let
S : Var → 2Atnv be an assignment, i.e. a function that assigns to each variable
X ∈ Var a set SX ⊆ Atnv . The relation >S on Var is defined as the transitive
closure of {(X, Y ) ∈ Var2 | Y occurs in an atom of SX }. If >S is irreflexive,
then S is called acyclic. In this case, we can define the substitution
d σS induc-
tively along >S as follows: if X is minimal, then σS (X) := D∈SX D; other-
d that σS (Y ) is defined for all Y ∈ Var with X > Y , and define
wise, assume
σS (X) := D∈SX σS (D). All substitutions of this form are called local.
Results
Unification in EL is local : each problem Γ can be transformed into an equivalent
flat problem that has a local solution iff Γ is solvable, and hence (general) solv-
ability of unification problems in EL is in NP [5]. However, disunification in EL
1
A unification problem contains only subsumptions.
is not local in this sense: consider
Γ := {X v? B, A u B u C v? X, ∃r.X v? Y, > 6v? Y, Y 6v? ∃r.B}
with variables X, Y and constants A, B, C. If we set σ(X) := A u B u C and
σ(Y ) := ∃r.(A u C), then σ is a solution of Γ that is not local. This is because
∃r.(A u C) is not a substitution of any non-variable atom in Γ. Assume now
that Γ has a local solution γ. Since γ must solve the first dissubsumption, γ(Y )
cannot be >, and due to the third subsumption, none of the constants A, B, C
can be a conjunct of γ(Y ). The remaining atoms ∃r.γ(X) and ∃r.B are ruled
out by the last dissubsumption since both γ(X) and B are subsumed by B. This
shows that Γ cannot have a local solution, although it is solvable.
The decidability and complexity of general solvability of disunification prob-
lems is still open. However, we can show that each dismatching problem Γ,
which is a disunification problem where one side of each dissubsumption must
be ground, can be polynomially reduced to a flat problem that has a local solu-
tion iff Γ is solvable. This shows that deciding solvability of dismatching problems
in EL is in NP. The main idea is to introduce auxiliary variables and flat atoms
that allow us to solve the dissubsumptions using a local substitution. For exam-
ple, we replace the dissubsumption > 6v? Y from above with Y v? ∃r.Z. The
rule we applied here is the following:
Solving Left-Ground Dissubsumptions:
Condition: This rule applies to s = C1 u · · · u Cn 6v? X if X is a variable and
C1 , . . . , Cn are ground atoms.
Action: Choose one of the following options:
– Choose a constant A ∈ Σ, replace s by X v? A. If C1 u · · · u Cn v A, then fail.
– Choose a role r ∈ Σ, introduce a new variable Z, replace s by X v? ∃r.Z,
C1 6v? ∃r.Z, . . . , Cn 6v? ∃r.Z.
According to the rule, we can choose a constant or create a new existential
restriction with a fresh variable, and use it in the new subsumption and dissub-
sumptions. In our example the left hand side of the dissubsumption > 6v? Y is
empty, hence only a subsumption is produced.
However, the brute-force NP-algorithm for checking local solvability of the
resulting flat disunification problem is hardly practical. For this reason, we have
extended the rule-based algorithm from [5] and the SAT reduction from [4] by
additional rules and propositional clauses, respectively, to deal with dissubsump-
tions. The reason we extend both algorithms is that, in the case of unification,
they have proved to complement each other well in first evaluations [1]: the
goal-oriented algorithm needs less memory and finds minimal solutions faster,
while the SAT reduction generates larger data structures, but outperforms the
goal-oriented algorithm on unsolvable problems. The SAT reduction has been
implemented in our prototype system UEL.2 First experiments show that dis-
matching is indeed helpful for reducing the number and the size of unifiers. The
runtime performance of the solver for dismatching problems is comparable to
the one for pure unification problems.
2
version 1.3.0, available at http://uel.sourceforge.net/
References
1. Baader, F., Borgwardt, S., Mendez, J.A., Morawska, B.: UEL: Unification solver for
EL. In: Kazakov, Y., Lembo, D., Wolter, F. (eds.) Proc. of the 25th Int. Workshop
on Description Logics (DL’12). CEUR Workshop Proceedings, vol. 846, pp. 26–36
(2012)
2. Baader, F., Borgwardt, S., Morawska, B.: Dismatching and local disunfication
in EL. LTCS-Report 15-03, Chair for Automata Theory, TU Dresden, Germany
(2015), see http://lat.inf.tu-dresden.de/research/reports.html.
3. Baader, F., Borgwardt, S., Morawska, B.: Dismatching and local disunification in
EL. In: Fernández, M. (ed.) Proc. of the 26th Int. Conf. on Rewriting Techniques
and Applications (RTA’15). LIPIcs, vol. 36. Dagstuhl Publishing (2015), to appear.
4. Baader, F., Morawska, B.: SAT encoding of unification in EL. In: Fermüller, C.G.,
Voronkov, A. (eds.) Proc. of the 17th Int. Conf. on Logic for Programming, Arti-
ficial Intelligence, and Reasoning (LPAR’10). Lecture Notes in Computer Science,
vol. 6397, pp. 97–111. Springer-Verlag (2010)
5. Baader, F., Morawska, B.: Unification in the description logic EL. Logical Methods
in Computer Science 6(3) (2010)
6. Baader, F., Narendran, P.: Unification of concept terms in description logics. J. of
Symbolic Computation 31(3), 277–305 (2001)
7. Babenyshev, S., Rybakov, V.V., Schmidt, R., Tishkovsky, D.: A tableau method
for checking rule admissibility in S4. In: Proc. of the 6th Workshop on Methods
for Modalities (M4M-6). Copenhagen (2009)
8. Buntine, W.L., Bürckert, H.J.: On solving equations and disequations. J. of the
ACM 41(4), 591–629 (1994)
9. Comon, H.: Disunification: A survey. In: Lassez, J.L., Plotkin, G. (eds.) Com-
putational Logic: Essays in Honor of Alan Robinson, pp. 322–359. MIT Press,
Cambridge, MA (1991)
10. Ghilardi, S.: Unification through projectivity. Journal of Logic and Computation
7(6), 733–752 (1997)
11. Ghilardi, S.: Unification in intuitionistic logic. Journal of Logic and Computation
64(2), 859–880 (1999)
12. Iemhoff, R., Metcalfe, G.: Proof theory for admissible rules. Annals of Pure and
Applied Logic 159(1-2), 171–186 (2009)
13. Rybakov, V.V.: Admissibility of logical inference rules, Studies in Logic and the
Foundations of Mathematics, vol. 136. North-Holland Publishing Co., Amsterdam
(1997)
14. Rybakov, V.V.: Multi-modal and temporal logics with universal formula - reduction
of admissibility to validity and unification. Journal of Logic and Computation
18(4), 509–519 (2008)
15. Wolter, F., Zakharyaschev, M.: Undecidability of the unification and admissibility
problems for modal and description logics. ACM Transactions on Computational
Logic 9(4), 25:1–25:20 (2008)