=Paper=
{{Paper
|id=Vol-477/paper-55
|storemode=property
|title=Model-Based Most Specific Concepts in Some Inexpressive Description Logics
|pdfUrl=https://ceur-ws.org/Vol-477/paper_38.pdf
|volume=Vol-477
|dblpUrl=https://dblp.org/rec/conf/dlog/Distel09
}}
==Model-Based Most Specific Concepts in Some Inexpressive Description Logics==
https://ceur-ws.org/Vol-477/paper_38.pdf
Model-Based Most Specific Concepts in Some
Inexpressive Description Logics
Felix Distel⋆
TU Dresden, Germany
Abstract. Model-based most specific concepts are a non-standard rea-
soning service in Description Logics. They have turned out to be useful
in knowledge base completion for ontologies that are written in certain
extensions of EL. There is indication that model-based most specific
concepts can also be applied for knowledge base completion in other in-
expressive description logics. We show that model-msc exist in the logics
FL0 and FLE with cyclic TBoxes and for ALC ∪∗ with acyclic TBoxes.
We provide constructions for model-msc in these three logics.
Many of the ontologies that are used today are large in scale and formulated in
one of the less expressive Description Logics (DL). As ontologies become larger,
tools that support engineers during the process of building and maintaining
ontologies are gaining in importance. Often, the people who are in charge of
building an ontology are experts in the domain of interest, rather than experts
in Description Logics. They may sometimes be unable to comprehend the full
consequences of a statement. Several reasoning services have been developed to
assist them, such as Satisfiability Checking and Axiom Pinpointing [15]. Most
of these services can be used to check the correctness of the knowledge that is
already contained in the knowledge base. They cannot be used to detect what
knowledge is missing in the knowledge base.
Knowledge base completion addresses this issue. In knowledge base comple-
tion it is assumed that there is an expert (or a group of experts) who has complete
knowledge about the domain in the so-called “real world”. It is furthermore as-
sumed that this “real world” can be represented as a model of the knowledge
base. We sometimes call this model the background model of the knowledge base.
Intuitively, a knowledge base is complete, if all questions about the background
model can be answered by querying the knowledge base. Usually some kind of
restriction with regard to the structure of these questions is made.
Baader and Sertkaya have developed one knowledge base completion formal-
ism [6]. For their approach a knowledge base is complete if it can answer all
questions of the form “Does the general concept inclusion (GCI) C ⊑ D hold (in
the real world)?”. C and D cannot be arbitrary concept descriptions but must
be conjunctions of concepts that are already present in the knowledge base.
Rudolph’s approach (Relational Exploration) also asks for GCIs, but uses arbi-
trary concept descriptions from the DL FLE [13, 14]. Like Baader and Sertkaya
⋆
supported by Cusanuswerk e. V.
Rudolph uses an expert-assisted approach similar to attribute exploration from
Formal Concept Analysis (FCA) [11]. Both systems repeatedly find GCIs that
do not follow from the existing knowledge base and present them to the expert.
If the expert accepts the GCI it is added to the knowledge base. If she rejects
it, she is asked to add a counterexample.
Expert interaction is the most time-consuming part in the exploration pro-
cess, and it is a major goal to reduce it. The problem with Rudolph’s approach
is that the number of expert interactions can become relatively large. To reduce
expert interaction, it is important to find a small set of GCIs from which all
GCIs that hold in a given background model follow. Unlike Baader and Sertkaya
we still allow arbitrary GCIs from a given logic - not just GCIs formed using
conjunctions of previously selected concepts.
We present model-based most specific concepts (model-msc) as a tool to
reduce the number of GCIs that have to be considered. Model-msc are similar to
most specific concepts for ABoxes but exhibit certain different characteristics.
ABox-msc are the most specific concept describing an individual in an ABox [2,
7]. A model-msc is the most specific concept describing a subset of the domain
of some model or primitive interpretation. If they exist they are unique up to
equivalence, which justifies the notation mmsc(A) for the model-msc of a set A.
The reason why model-msc can help to reduce expert interaction is the fol-
lowing. We say that C ⊑ D follows from C ⊑ E iff all models of C ⊑ E are
models of C ⊑ D. Knowledge base completion aims at adding a minimal set
of GCIs B to a knowledge base, such that all GCIs that hold in a given back-
ground model i follow from B. Assume that model-msc exist for all models for
a given logic. Let C be a concept description in this logic, and C i its exten-
sion in the background model i. We shall show in this paper that every GCI
C ⊑ D that holds in the background model i follows from a single GCI, namely
C ⊑ mmsc(C i ). For a fixed description C there may be infinitely many GCIs
C ⊑ D that hold in the background model i. Knowing a single GCI from which
they all follow can greatly reduce the number of GCIs that need to be presented
to the expert.
For the logic EL with greatest fixpoint (gfp) semantics it can be shown that
model-msc always exist. They can be used to construct a small set of GCIs
that form a basis for the GCIs holding in some finite background model [4].
It is possible to transfer many ideas from FCA to the DL world. This can be
exploited to develop a knowledge base completion formalism [5].
So model-msc have been shown to be useful in the description logic EL with
gfp-semantics. The results for EL with gfp-semantics indicate that model-msc
might also be useful for knowledge base completion in other inexpressive descrip-
tion logics. In this work we examine the logics FL0 , FLE and ALC. Unfortu-
nately, there are examples of models for which model-msc do not exist for any
of the three logics. However, we present extensions for each of the three logics
in which they do exist. These extensions are gfp-semantics for FL0 and FLE,
and the universal role and reflexive transitive closure of roles fol ALC. We also
provide constructions for the model-msc in the extended logics.
Besides being useful in knowledge base completion, model-msc are also in-
teresting from a theoretical perspective. By comparing them to the similar msc
for ABoxes one can learn more about the implications of open-world semantics
versus closed-world semantics. We shall see that model-msc are not as closely
related to classical msc for ABoxes as one might think. Their computational
behaviour can be different. For example model-msc need not exist in FL0 with
acyclic TBoxes, but ABox-msc do exist for this logic.
1 Preliminaries
1.1 Greatest Fixpoint Semantics
The description logics that we are considering in this work are FL0 , FLE, and
ALC. FL0 provides for the concept constructors conjunction (⊓), value restric-
tions (∀), and the top concept (⊤). FLE extends FL0 with existential restric-
tions (∃). In addition to these constructors ALC provides for disjunction (⊔) and
negation ¬ and the bottom concept (⊥).
An acyclic or unfoldable TBox is a set of equivalence statements of the form
A ≡ C where A is a concept name and C is a concept description in the respective
logic. Every concept name may occur at most once as the right hand side of an
equivalence. No concept name may be used explicitly or implicitly in its own
definition. A cyclic TBox is like an acyclic TBox but without this last restriction.
An interpretation i = (∆i , ·i ) consists of a set ∆i and a function mapping
every concept name A to a subset Ai ⊆ ∆i and every role name r to a relation
ri ⊆ ∆i ×∆i . An interpretation can be extended such that it maps every concept
description to a subset of ∆i . The semantics of concept descriptions in FL0 , FLE
and ALC are defined in the usual way (cf. [8] for details). An interpretation i is
a model of an acyclic TBox T if Ai = C i holds for all statements A ≡ C in T .
In the case of cyclic TBoxes several possible semantics exist [12]. The seman-
tics that we use in this work are greatest-fixpoint semantics (or gfp-semantics
for short). We denote by Np the set of primitive concept names, i. e. the set
of concept names that do not occur on the left hand side of some equivalence
statement. A primitive interpretation i is a mapping that assigns a binary re-
lation ri ⊆ ∆i × ∆i to every r ∈ Nr and a set P i ⊆ ∆i to every P ∈ Np . An
interpretation j is based on the primitive interpretation i if it coincides with
i on Nr and Np and maps every defined concept name A to some Aj ⊆ ∆i .
It can be shown that for the logics FL0 and FLE, for every TBox T and for
every primitive interpretation of T there is a so-called gfp-model i among the
interpretations that are based on i. We are not going to give a full definition of
greatest fixpoint semantics. For more details consider for example [12].
Both for acyclic and for cyclic TBoxes a model is uniquely determined by an
interpretation of the primitive concept names and role names. Therefore, we will
use the terms model and primitive interpretation interchangeably and denote
both by the letter i.
mt
Carla Nicolas
S P
mt
Fig. 1. A Graph Representation of a Model
Models can be represented by directed graphs with labelled vertices and
edges. Given a model i the vertices of this graph are the elements of ∆i . A ver-
tex x is labelled with a primitive concept name P if x ∈ P i holds. Vertices x and y
are connected by an r-labelled edge iff (x, y) ∈ ri holds. Let us look at an example
for such a graph. As primitive concept names we use S (Singer ) and P (Politi-
cian), and as role name we use mt (isMarriedTo). The model iCouple consists
of the domain ∆iCouple = {Carla, Nicolas} and a mapping ·iCouple which maps
S to {Carla}, P to {Nicolas} and mt to {(Carla, Nicolas), (Nicolas, Carla)}.
Figure 1.1 shows a graph representation of this model.
1.2 Model-Based Most Specific Concepts
As usual we write C ⊑T D if C and D are concept names occurring in T and
C i ⊆ Di holds for all models i of T . A conservative extension of a TBox T is a
TBox T ′ such that T ⊆ T ′ , and if A and B are concept names used in T then
A ⊑T ′ B iff A ⊑T B.
A model-based most specific concept for a set X ⊆ ∆i in some model i is a
concept description whose extension contains X and is minimal with respect to
subsumption among all concept descriptions whose extension contains X.
Definition 1 (model-based most specific concepts). Let T be a TBox and
i a model of T . Let X ⊆ ∆i be some subset of the domain of i and E a defined
concept in T . Then E is called the most specific concept of X iff the following
conditions hold
– X ⊆ Ei
– If T ′ is a conservative extension of T that uses the same primitive concept
names and role names then for every defined concept F in T ′ with X ⊆ F i ,
it holds that E ⊑T ′ F .
If model-msc exist, they are unique up to equivalence. Therefore the notation
mmsc(X) for the model-msc of some X ⊆ ∆i is justified.
We say that a GCI C ⊑ D holds in a model i if C i ⊆ Di . A GCI C ⊑ D
follows from a set of GCIs L if C ⊑ D holds in all models in which all GCIs
from L hold. Knowledge base completion attempts to add GCIs to a knowledge
base such that eventually all GCIs that hold in some background model i follow
from the GCIs in the knowledge base. It is desirable to keep the number of newly
added GCIs small to the purpose of minimizing expert interaction.
Lemma 1. Assume that we are dealing with a logic such that model-msc always
exist, regardless of the model that is being used. If i is a model for the GCI
{C ⊑ D}, then C ⊑ D follows from {C ⊑ mmsc(C i )}.
Proof. Since i is a model for {C ⊑ D} it holds that C i ⊆ Di . The definition of
model-msc tells us that
mmsc(C i ) ⊑ D (1)
since mmsc(C i ) is the most specific concept whose extension contains C i .
Let j be some model of {C ⊑ mmsc(C i )}, i. e. C j ⊆ mmsc(C i )j . We have
assumed that the model-msc for C j in the model j exists. Because of C j ⊆
mmsc(C i )j it must hold that mmsc(C j ) ⊑ mmsc(C i ) (By Definition 1 mmsc(C j )
is subsumed by any concept description whose extension in j contains C j ). To-
gether with (1) we obtain mmsc(C j ) ⊑ D. But then C j ⊆ mmsc(C j )j ⊆ Dj
must hold. We have shown that if j is a model of {C ⊑ mmsc(C i )} then j is
also a model of C ⊑ D. Therefore C ⊑ D follows from C ⊑ mmsc(C i ).
This shows that in logics where model-msc exist, we do not need to add more
than one GCI for a given left-hand side C. Thus the number of GCIs can be
reduced. One might argue that this is true whenever the used logic allows for
conjunction and whenever there is a finite number of axioms with left-hand side
C. However, the axioms are what is meant to be computed, and mmsc(C i ) can be
computed without knowing any axioms beforehand. The following sections focus
on indentifying logics for which model-msc do exist. Due to the page restrictions
we can only sketch most of the following proofs. Where proofs or details of proofs
are omitted, they can be found in [10].
2 Model-Based Most Specific Concepts in Three
Different Logics
2.1 Unfoldable TBoxes
In FL0 , FLE and ALC most specific concepts do not exist if TBoxes are acyclic.
Informally, this is because the models can be contain cycles, which cannot be
described using an acyclic terminology. Consider the model from Figure 1.1.
E0 ≡ S, E1 ≡ ∀mt.∀mt.S, E2 ≡ ∀mt.∀mt.∀mt.∀mt.S, . . . is a sequence of concept
descriptions of increasing role depth. Still Carla ∈ Eki holds for all k ∈ N. If
there were a model-msc M for {Carla} then M ⊑ Ek for all k ∈ N would hold.
But in all three logics this would mean that M could be unfolded to a concept
description whose role depth is greater than that of Ek for all k ∈ N. Since the
role depth of the Ek goes toward infinity this is impossible.
2.2 F L0 with Cyclic TBoxes and gfp-Semantics
We thus need to find a way to describe cycles in our models. One way to do this
is to use gfp-semantics. FL0 with gfp-semantics has been studied by Baader et
al. [1]. The semantics proposed there make use of semi-automata with word tran-
sitions. A semi-automaton with word transitions is basically a finite automaton
where no initial state or final states have been specified (they will be specified
later on). Baader uses word transitions, so the transition function of the au-
tomaton takes words over an alphabet Σ, not symbols from Σ as input. More
formally, a semi-automaton A is a triple A = (Σ, Q, E) where Σ is a finite al-
phabet, Q is a set of states, and E ⊆ Q × Σ ∗ × Q is a set of labelled edges. In
every step the automaton can move from a state q1 to a state q2 on some input
w ∈ Σ ∗ if there are words w1 , w2 ∈ Σ ∗ such that w = w1 w2 and (q1 , w1 , q2 ) ∈ E.
A finite model i can easily be translated into a semi-automaton Ai = (Σi , Qi , Ei ),
where Σi = Nr , Qi = ∆i and Ei is the set of all labelled edges (a, r, b) such that
(a, b) ∈ ri . A state x is labelled with P ∈ Np iff x ∈ P i holds.
Similarly, a cyclic FL0 -TBox T can be translated into a semi-automaton
AT with ΣT = Nr . We assume that T is normalized in the sense that every
equivalence statement in T is of the form
D = ∀W1 .A1 ⊓ · · · ⊓ ∀Wk .Ak . (2)
The states of AT are the concept names occurring in T . For every defined concept
D ther is at most one equivalence statement of the form (2) in T . ET contains
an edge (D, Wk , Ak ) if this statement contains a term ∀Wk .Ak .
The automata AT and Ai give rise to the languages L(A, P ), L(x, y) and
L(x, P ), where A, P are concept names occurring in T and x, y ∈ ∆i . Define
– L(A, P ) consists of all words w ∈ Nr∗ for which AT can move from state A
to state P on input w.
– L(x, y) consists of all words w ∈ Nr∗ for which Ai can move from state x to
state y on input w.
– L(x, P ) = {W ∈ Nr∗ | ∀y ∈ ∆i : W ∈ L(x, y) implies y ∈ P i }.
The following characterization of the semantics of FL0 -TBoxes with gfp-
semantics makes use of these previously defined languages.
Lemma 2. Let T be a TBox and let AT be the corresponding semi-automaton.
Let i be a gfp-model of T and let D, E be concept names occurring in T . Let
x ∈ ∆i be some element of ∆i . Then
– x ∈ Di iff for all primitive concepts P ∈ Np it L(A, P ) ⊆ L(x, P ) holds, and
– A ⊑T B iff L(B, P ) ⊆ L(A, P ) holds for all primitive concepts P .
A regular language is a language which is accepted by a finite state automa-
ton. The languages L(A, P ) and L(x, y) are all regular, since they are accepted by
a finite state automaton. The languages L(x, P ) are also regular, which follows
from this lemma.
Lemma 3. For every model i, x ∈ ∆i and P ∈ Np
[
L(x, P ) = L(x, y)
y ∈P
/ i
r
r r s
a b A B ε P
s
s
(a) An Example for a (b) Semi-Automaton with
Model L(a, P ) = L(A, P )
Fig. 2. A Model and Corresponding Semi-Automaton
holds. The class of regular languages is closed under complement and set union.
Since the languages L(x, c) are regular this implies that L(x, P ) is also regular.
Since L(x, P ) is regular for every P ∈ Np , we can find a finite state automaton
which accepts L(x, P ). Therefore, there is a semi-automaton Ai = (Np , Qi , Ei )
and some E ∈ Qi such that L(E, P ) = L(x, P ). By Ti denote the TBox that cor-
responds to Ai . Then Lemma 2 shows that x ∈ E i holds. Let Ti′ be conservative
extension of Ti and let F be a defined concept in Ti′ such that x ∈ F i . Because of
Lemma 2 we have L(F, P ) ⊆ L(x, P ) for all P ∈ Np and thus L(F, P ) ⊆ L(E, P ).
Using Lemma 2 we obtain E ⊑Ti′ F . Thus E is the model-msc for x in i.
Theorem 1. Let i be a model and x ∈ ∆i . Let Ai be a semi-automaton with a
state E for which L(E, P ) = L(x, P ) for all P ∈ Np . Let Ti be the TBox that
corresponds to Ai . Then E in Ti is the model-msc for x in i.
Since it is known that least common subsumers exists in FL0 with greatest
fixpoint semantics, model-msc must also exist for non-singleton sets {x1 , . . . , xn }.
More precisely, we obtain mmsc({x1 , . . . , xn }) = lcs(mmsc(x1 ), . . . , mmsc(xn )).
Note that when we construct a finite state automaton that accepts the com-
plement a language we implicitly use the subset construction to make a non-
deterministic finite state automaton deterministic. This construction involves an
exponential blowup in size which cannot be avoided. Thus also the model-msc
may become exponentially large in the size of the model i.
An Example We give a short example of a model i0 and show how to construct
a model-based most specific concept for a ∈ ∆i0 . Let the model i0 be defined by
∆i0 = {a, b}, ri0 = {(a, b), (b, b)}, si0 = {(b, b)} and P i0 = ∅, where Nr = {r, s}
and Np = {P }. The semi-automaton Ai0 is depicted in Figure 2(a). To construct
a model-based most specific concept we need to compute L(a, P ) first. From
Lemma 3) we obtain L(a, P ) = L(a, a) ∪ L(a, b). The languages L(a, a), and
L(a, b) formulated as regular expressions are
L(a, a) = {ǫ}, L(a, b) = L(r{r, s}∗ )
So we obtain L(a, P ) = {ǫ} ∪ L(r{r, s}∗ ) = L(s{r, s}∗ ). A semi-automaton with
L(a, P ) = L(A, P ) is depicted in Figure 2(b). This automaton gives rise to the
TBox Ti = {A ≡ ∀s.B, B ≡ P ⊓ ∀r.B ⊓ ∀s.B}. A is the model-msc for a in i0 .
Informally, the model-msc describes individuals for which all s-successors and
all successors of s-successors are in the extension of P . This is true for a in i
since we know that a does not have any s-successors.
To illustrate the differences between open-world and closed-world semantics
consider an ABox A containing the assertions r(a, b), s(b, b) and r(b, b). A graph-
ical representation of this ABox would look exactly like Figure 2(a). Still the msc
for a in A would be ⊤ and not A, since because of the open-world semantics of
A we do not know whether A has s-successors or not.
2.3 F LE with Cyclic TBoxes and gfp-Semantics
We have seen in Section 2.1 that model-msc need not exist if we only allow for
unfoldable TBoxes. For the case of FL0 we have successfully shown that this
problem can be overcome by allowing for cyclic TBoxes with greatest fixpoint
semantics. The same thing can be done for FLE.
FLE-TBoxes can be visualized using so-called FLE-description graphs that
have been introduced by Baader et al. [8, 9]. Let T be a normalized FLE-TBox.
In this context we call T normalized if every concept definition in T is of the
form
A ≡ P1 ⊓ · · · ⊓ Pk ⊓ ∀r1 .B1 · · · ⊓ ∀rl .Bl ⊓ ∃s1 .C1 · · · ⊓ ∃sm .Cm , (3)
where A, B1 , . . . , Bl , C1 , . . . , Cm are the names of defined concepts, P1 , . . . ,
Pk are primitive concept names and r1 , . . . , rl , s1 , . . . , sm are defined concept
names.
An FLE-description graph GT is a directed graph with labelled nodes and
edges. The nodes of GT are the names of defined concepts in T . For every node A
there is exactly one statement of the form (3) in T . A node A is labelled with the
primitive concept names P1 , . . . , Pk that occur in its definition. For every term
∀rn .Bn in (3) there is an edge from A to Bn labelled ∀rn , and for every term
∃sn .Cn there is an edge from A to Cn labelled ∃sn . The description graph of an
unfoldable TBox will be a tree while the description graph of an cyclic TBox
will naturally be a cyclic graph. Apart from being a handy visualization tool
description graphs are also used to characterize the semantics of FLE-TBoxes,
for the cyclic case [10]. For an example of an FLE-description graph see the
example at the end of this section.
The construction for model-based most specific concepts in FLE with cyclic
TBoxes is a hybrid between the constructions for model-msc in EL and FL0 .
It is similar to the subset construction that is used to turn a nondeterministic
finite state automaton into a deterministic finite state automaton. This has been
used implicitly in Section 2.2. On the other hand the proofs and the semantical
characterizations that are involved make heavy use of graph simulations which
are also used in the case of EL [3].
For a given model i we define the canonical terminology of i as follows. Let
GTi be a description graph whose nodes are all subsets U ⊆ ∆i where
∃r ∀r ∃r ∀r
∀s ∀r
P ∅ {a} {b}
∃r
∃s ∀s ∃s ∀s
Fig. 3. The Canonical Terminology for the Model from Figure 2(a)
– a node U is labelled with P ∈ Np iff all elements of U are in the extension
of P , i. e. x ∈ P i for all x ∈ U , and
– there is an edge labelled ∃r from U to V ⊆ ∆i iff every x ∈ U has an
r-successor y in V , and
– there is an edge labelled ∀r from U to Sr,U where Sr,U = {x ∈ ∆i | ∃y ∈ U :
(x, y) ∈ ri } is the set of all r-successors of some element of U .
We call the TBox Ti that has GTi as its description graph the canonical termi-
nology of i. For every U ⊆ ∆i we denote the corresponding concept name by
AU , to avoid confusion.
Why does this help us with the construction of model-msc The underlying
idea of the canonical terminology is that every defined concept AU in T should be
the model-msc for U in i. Now, let us look at the description AU in detail. What
is the most specific description of the form ∀r.B that can subsume AU ? Under the
assumption that ASr,U is a most specific concept for Sr,U the answer is ∀r.ASr,U .
Since Sr,U is the set of all r-successors of some element of U , U ⊆ (∀r.ASr,U )i
must hold. On the other hand, ASr,U ⊑ B holds for every B with Sr,U ⊆ B i
(and thus for every B with U ⊆ (∀r.B)i ). Therefore, ∀r.ASr,U ⊑ ∀r.B holds for
all such B. It therefore makes perfect sense to add to GTi an edge labelled ∀r
pointing from U to Sr,U . The intuition for the existential restrictions is similar.
The complete proof of the following theorem uses a variant of the Knaster-
Tarski-fixpoint theorem and a characterization of gfp-semantics that is based on
graph-simulations between FLE-description graphs [10].
Theorem 2. Let i be a model for a given set of primitive concept names Np
and a set of role names Nr . Let U ⊆ ∆i be a subset of its domain and let Ti be
the canonical terminology for i. Then AU in Ti is the model-msc for i.
An Example Let us look at the example from Section 2.2 again. The model
i0 has the canonical terminology whose description graph is depicted in Fig-
ure 2.3. The vertex {a, b} is redundant and has been omitted to keep the dia-
gram somewhat legible. From the description graph we obtain the terminology
Ti = {Aa ≡ ∀r.Ab ⊓ ∀s.A∅ ⊓ ∃r.Ab , Ab ≡ ∀r.Ab ⊓ ∀s.Ab ⊓ ∃r.Ab ⊓ ∃s.Ab , A∅ ≡
P ⊓ ∀r.A∅ ⊓ ∀s.A∅ ⊓ ∃r.A∅ ⊓ ∃s.A∅ }.
2.4 ALC ∪∗
In the case of ALC it is not necessary to use the full expressive power of greatest-
fixpoint semantics in order to make sure that most specific concepts always exist.
It suffices to add union of roles (∪) and reflexive-transitive closure of roles (r∗ )
to guarantee existence of model-msc The semantics of ∪ and ·∗ are intuitively
defined as (r1 ∪ r2 )i = r1i ∪ r2i and (r∗ )i = (ri )∗ for all models i, where (ri )∗
denotes the reflexive transitive closure of the binary relation ri .
Let’s go back to the example from Section 1.1. First of all, notice that there
is a concept description (e. g. S) that has only Carla in its extension. Likewise,
P has only Nicolas in its extension. If such concept descriptions exist, we say
that Carla and Nicolas are distinguishable.
We try to find a model-msc for Carla. For a start consider the concept
descriptions DCarla ≡ S⊓¬P⊓∃mt.P⊓∀mt.P and DNicolas ≡ P⊓¬S⊓∃mt.S⊓∀mt.S
DCarla and DNicolas describe the elements Carla and Nicolas in the model i,
but they are not specific enough to be model-msc For example ∀mt.∃mt.S also
describes Carla, but does not subsume DCarla . But the concept description ∀mt.P
does. We know that Nicolas is the only Politician in the model i. Therefore,
it would be helpful to require something like “Every politician is an instance of
DNicolas . With the help of the transitive closure of roles we can do something
very similar, by defining
ECarla ≡ DCarla ⊓ ∀mt∗ .(¬P ⊔ DNicolas ) ⊓ ∀mt∗ .(¬S ⊔ DCarla ).
j
Let j be some model with the same signature as i and x ∈ ECarla . The term
∗ ∗ j
∀mt .(¬P ⊔ DNicolas ) makes sure that every mt -successor of x is in DNicolas if
j
it is in Pj (and it is in DCarla if it is in Sj ). Because x is an instance of DCarla
we can be sure that every mt-successor of x is a Politician. This means that this
successor has to be an instance of DNicolas , which in turn requires that all its
successors are Singers, and so on. This way, we have implictitly added a flavour
of cycles to ECarla without using cycles explicitly.
This gives us an idea how to formally construct model-msc for a given model
i. We first assume that all elements of ∆i are distinguishable, i. e. that for every
x ∈ ∆i there is some concept description Cx such that {x} = Cxi . Then define
l l l l G !
Dx ≡ P⊓ ¬P ⊓ ∃r.Cy ⊓ ∀r. Cy ,
P ∈Np P ∈Np r∈Nr y∈∆i y∈∆i
x∈P i / i
x∈P (x,y)∈r i (x,y)∈r i
where we define the empty disjunction to be ⊥ and the empty conjunction to be
⊤. Furthermore define
l [ ∗
Mx ≡ Cx ⊓ ∀ r .(¬Cy ⊔ Dy ). (4)
y∈∆i r∈Nr
A bisimulation is a relation ζ ⊆ ∆i × ∆j with the following three properties.
Let (y, y ′ ) ∈ ζ.
– For every P ∈ Np it holds that y ∈ P i iff y ′ ∈ P j .
– Forth condition. z ∈ ∆i , (y, z) ∈ ri ⇒ (∃z ′ ∈ ∆j : (y ′ , z ′ ) ∈ rj and (z, z ′ ) ∈ ζ)
– Back condition. z ′ ∈ ∆j , (y ′ , z ′ ) ∈ rj ⇒ (∃z ∈ ∆i : (y, z) ∈ ri and (z, z ′ ) ∈ ζ)
Let j = (∆j , ·j ) be a second model over the same signature and let x′ ∈ Mxj .
ALC and ALC ∪∗ can be viewed as modal logics. It is a well-known fact from
modal logics that if there is a bisimulation from x to x′ then x and x′ are
indistinguishable, i. e. there is no ALC ∪∗ -concept description C with x ∈ C i but
x′ ∈
/ C j . It is easy but tedious to show that
[ j
∗
Z = {(y, y ′ ) | y ∈ ∆i , y ′ ∈ Cyj , (x′ , y ′ ) ∈ r }
r∈Nr
′
is a bisimulation. This proves that x and x are indistinguishable. Therefore
for every ALC ∪∗ concept description D with x ∈ Di it holds that x′ ∈ Dj for
all x′ ∈ Mxj . Thus Mxj ⊆ Dj . Since j was an arbitrary model this implies that
Mx ⊑ D. Therefore, Mx is a most specific concept for {x}. Most specific concepts
for non-singleton sets {x1 , . . . , xn } can be obtained as the disjunction of Mx1 ,
. . . , Mxn .
Theorem 3. If i is a model over a signature (Np , Nr ) then Mx as defined in (4)
is a model-msc for {x}. Since least common subsumers exist in ALC ∪∗ (ALC ∪∗
provides for disjunction) this shows that model-msc exist for all subsets of ∆i .
Theorem 3 can be generalized to the case of models that do contain indistin-
guishable states [10].
3 Conclusion and Future Work
We have seen that in many standard logics model-msc need not exist. In the
present work we have presented constructions for model-mscs in ALC with union
of roles and reflexive-transitive closure of roles and in FL0 and FLE with cyclic
TBoxes and gfp-semantics. There is hope that the model-msc can be used for
knowledge base completion. The existence of model-msc ensures that a basis
for the set of GCIs that hold in a given background model need not contain
more than one GCI with a given left-hand side and that the right-hand-side of
this GCI can be computed without knowing a finite set of axioms beforehand.
However, the number of left-hand sides may still be large. For EL one can use
ideas from Formal Concept Analysis to further reduce the number of GCIs and
to obtain a knowledge base completion formalism [5]. It remains to be examined
whether this can also be done for the three logics presented here.
The three logics used here are admittedly not very common. This is firstly
because of the gfp-semantics involved. For the case of EL it has been shown that
one can get rid of cyclic concept descripitions (and gfp-semantics) easily after a
complete set of GCIs has been found. A similar result for the logics presented
here is needed to make the results useful in practice.
Secondly, one might argue that the logics FLE, and FL0 are still not com-
monly used, even without gfp-semantics. However, they are fragments of com-
monly used logics. Completeness with respect to GCIs formulated using one of
these fragments is still much stronger than completeness with respect to GCIs
that are only allowed to use conjunction.
References
1. Franz Baader. Using automata theory for characterizing the semantics of termino-
logical cycles. Ann. of Mathematics and Artificial Intelligence, 18:175–219, 1996.
2. Franz Baader. Least common subsumers and most specific concepts in a description
logic with existential restrictions and terminological cycles. In Georg Gottlob and
Toby Walsh, editors, Proc. of the 18th Int. Joint Conf. on Artificial Intelligence,
pages 319–324. Morgan Kaufmann, 2003.
3. Franz Baader. Terminological cycles in a description logic with existential restric-
tions. In Georg Gottlob and Toby Walsh, editors, Proc. of the 18th Int. Joint Conf.
on Artificial Intelligence (IJCAI 2003), pages 325–330, Acapulco, Mexico, 2003.
Morgan Kaufmann, Los Altos.
4. Franz Baader and Felix Distel. A finite basis for the set of EL-implications holding
in a finite model. In Raoul Medina and Sergei Obiedkov, editors, Proc. of the 6th
Int. Conf. on Formal Concept Analysis (ICFCA ’08), volume 4933 of Lecture Notes
in Artificial Intelligence, pages 46–61. Springer, 2008.
5. Franz Baader and Felix Distel. Exploring finite models in the description logic
ELgfp . In Proc. of ICFCA 2009. Springer, 2009.
6. Franz Baader, Bernhard Ganter, Ulrike Sattler, and Barış Sertkaya. Completing
description logic knowledge bases using formal concept analysis. In Proc. of the
20th Int. Joint Conf. on Artificial Intelligence (IJCAI 2007). AAAI Press/The
MIT Press, 2007.
7. Franz Baader and Ralf Küsters. Computing the least common subsumer and the
most specific concept in the presence of cyclic ALN -concept descriptions. In Proc.
of the 22nd German Annual Conf. on Artificial Intelligence (KI’98), volume 1504
of Lecture Notes in Computer Science, pages 129–140. Springer-Verlag, 1998.
8. Franz Baader, Ralf Küsters, and Ralf Molitor. Computing least common subsumers
in description logics with existential restrictions. In Proc. of the 16th Int. Joint
Conf. on Artificial Intelligence (IJCAI’99), pages 96–101, 1999.
9. Sebastian Brandt and Anni-Yasmin Turhan. Computing least common subsumers
for FLE + . In Proc. of DL 2003, CEUR-WS, 2003.
10. Felix Distel. Model-based most specific concepts in description logics with value re-
strictions. LTCS-Report 08-04, Institute for theoretical computer science, TU Dres-
den, Dresden, Germany, 2008. http://lat.inf.tu-dresden.de/research/reports.html.
11. Bernhard Ganter and Rudolf Wille. Formal Concept Analysis: Mathematical Foun-
dations. Springer, New York, 1997.
12. Bernhard Nebel. Terminological cycles: Semantics and computational properties.
In John F. Sowa, editor, Principles of Semantic Networks, pages 331–361. Morgan
Kaufmann, Los Altos, 1991.
13. Sebastian Rudolph. Exploring relational structures via FLE. In K. E. Wolff, H. D.
Pfeiffer, and H. S. Delugach, editors, ICCS, volume 3127 of LNCS, pages 196–212,
2004.
14. Sebastian Rudolph. Relational Exploration – Combining Description Logics and
Formal Concept Analysis for Knowledge Specification. PhD thesis, Technische
Universität Dresden, 2006.
15. Stefan Schlobach and Ronald Cornet. Non-standard reasoning services for the
debugging of description logic terminologies. In Georg Gottlob and Toby Walsh,
editors, Proc. of the 18th Int. Joint Conf. on Artificial Intelligence (IJCAI 2003),
pages 355–362, Acapulco, Mexico, 2003. Morgan Kaufmann, Los Altos.