Model-based most specific concepts are a non-standard reasoning 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 inexpressive description logics. We show that model-msc exist in the logics F L0 and F LE with cyclic TBoxes and for ALC∪∗ with acyclic TBoxes. We provide constructions for model-msc in these three logics.
Rudolph uses an expert-assisted approach similar to attribute exploration from
Formal Concept Analysis (FCA) [
Expert interaction is the most time-consuming part in the exploration process, 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 [
The reason why model-msc can help to reduce expert interaction is the following. 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 background 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 Ci its extension 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(Ci). 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 E L 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 [
So model-msc have been shown to be useful in the description logic E L with gfp-semantics. The results for E L with gfp-semantics indicate that model-msc might also be useful for knowledge base completion in other inexpressive description logics. In this work we examine the logics F L0, F LE and ALC. Unfortunately, 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 F L0 and F LE , 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 interesting 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 F L0 with acyclic TBoxes, but ABox-msc do exist for this logic. 1
1.1
Greatest Fixpoint Semantics The description logics that we are considering in this work are F L0, F LE , and ALC. F L0 provides for the concept constructors conjunction (⊓), value restrictions (∀), and the top concept (⊤). F LE extends F L0 with existential restrictions (∃). 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 F L0, F LE
and ALC are defined in the usual way (cf. [
In the case of cyclic TBoxes several possible semantics exist [
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.
S
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 vertex 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 (Politician), 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. As usual we write C ⊑T D if C and D are concept names occurring in T and Ci ⊆ 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 Ci ⊆ 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(Ci)}.
Proof. Since i is a model for {C ⊑ D} it holds that Ci ⊆ Di. The definition of model-msc tells us that mmsc(Ci) ⊑ D (1) since mmsc(Ci) is the most specific concept whose extension contains Ci.
Let j be some model of {C ⊑ mmsc(Ci)}, i. e. Cj ⊆ mmsc(Ci)j . We have assumed that the model-msc for Cj in the model j exists. Because of Cj ⊆ mmsc(Ci)j it must hold that mmsc(Cj ) ⊑ mmsc(Ci) (By Definition 1 mmsc(Cj ) is subsumed by any concept description whose extension in j contains Cj ). Together with (1) we obtain mmsc(Cj ) ⊑ D. But then Cj ⊆ mmsc(Cj )j ⊆ Dj must hold. We have shown that if j is a model of {C ⊑ mmsc(Ci)} then j is also a model of C ⊑ D. Therefore C ⊑ D follows from C ⊑ mmsc(Ci).
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(Ci) 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 [
Model-Based Most Specific Concepts in Three Different Logics 2.1
Unfoldable TBoxes In F L0, F LE 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.
We thus need to find a way to describe cycles in our models. One way to do this
is to use gfp-semantics. F L0 with gfp-semantics has been studied by Baader et
al. [
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 F L0-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 F L0-TBoxes with gfpsemantics 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 automaton. 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 a r
b (a) An Example for a Model r s
A s
ε P r B s (b) Semi-Automaton with
L(a, P ) = L(A, P ) 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 corresponds to Ai. Then Lemma 2 shows that x ∈ Ei 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 F L0 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 complement a language we implicitly use the subset construction to make a nondeterministic 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 graphical 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
We have seen in Section 2.1 that model-msc need not exist if we only allow for unfoldable TBoxes. For the case of F L0 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 F LE .
F LE -TBoxes can be visualized using so-called F LE -description graphs that
have been introduced by Baader et al. [
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 F LE -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 F LE -TBoxes,
for the cyclic case [
The construction for model-based most specific concepts in F LE with cyclic
TBoxes is a hybrid between the constructions for model-msc in E L and F L0.
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 E L [
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 ∃s
P ∅ ∀r ∀s ∀s {a} ∀r ∃r
{b} ∃r ∃s ∀r ∀s – 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 terminology 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 ⊆ Bi (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
KnasterTarski-fixpoint theorem and a characterization of gfp-semantics that is based on
graph-simulations between F LE -description graphs [
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 Figure 2.3. The vertex {a, b} is redundant and has been omitted to keep the diagram 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∅}. In the case of ALC it is not necessary to use the full expressive power of greatestfixpoint 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).
Let j be some model with the same signature as i and x ∈ ECjarla. 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 Dx ≡
l P ⊓ l ¬P ⊓ l P ∈Np x∈P i
P ∈Np x∈/P i r∈Nr l y∈Δi (x,y)∈ri ∃r.Cy ⊓ ∀r.
G y∈Δi (x,y)∈ri
Cy ! , where we define the empty disjunction to be ⊥ and the empty conjunction to be ⊤. Furthermore define
Mx ≡ Cx ⊓ l ∀ y∈Δi
∗ [ r .(¬Cy ⊔ Dy). r∈Nr (4)
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′) ∈ ζ) ALCLeatnjd=A(LΔCj∪, ∗·j )cabne abesevcioenwdedmaosdeml oovdearl tlhogeicsas.mIet siisgnaawtuerlel-kannodwlnetfxa′ct∈fMromxj. 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 ∈ Ci but x′ ∈/ Cj . It is easy but tedious to show that
Z = {(y, y′) | y ∈ Δi, y′ ∈ Cyj , (x′, y′) ∈ 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
indistinguishable states [
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 F L0 and F LE 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 E L one can use
ideas from Formal Concept Analysis to further reduce the number of GCIs and
to obtain a knowledge base completion formalism [
The three logics used here are admittedly not very common. This is firstly because of the gfp-semantics involved. For the case of E L 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 F LE , and F L0 are still not commonly used, even without gfp-semantics. However, they are fragments of commonly 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.