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.