<?xml version="1.0" encoding="UTF-8"?>
<TEI xml:space="preserve" xmlns="http://www.tei-c.org/ns/1.0" 
xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" 
xsi:schemaLocation="http://www.tei-c.org/ns/1.0 https://raw.githubusercontent.com/kermitt2/grobid/master/grobid-home/schemas/xsd/Grobid.xsd"
 xmlns:xlink="http://www.w3.org/1999/xlink">
	<teiHeader xml:lang="en">
		<fileDesc>
			<titleStmt>
				<title level="a" type="main">Model-Based Most Specific Concepts in Some Inexpressive Description Logics</title>
			</titleStmt>
			<publicationStmt>
				<publisher/>
				<availability status="unknown"><licence/></availability>
			</publicationStmt>
			<sourceDesc>
				<biblStruct>
					<analytic>
						<author>
							<persName><forename type="first">Felix</forename><surname>Distel</surname></persName>
						</author>
						<author>
							<persName><forename type="first">T</forename><forename type="middle">U</forename><surname>Dresden</surname></persName>
						</author>
						<author>
							<persName><surname>Germany</surname></persName>
						</author>
						<title level="a" type="main">Model-Based Most Specific Concepts in Some Inexpressive Description Logics</title>
					</analytic>
					<monogr>
						<imprint>
							<date/>
						</imprint>
					</monogr>
					<idno type="MD5">C20AAFCC515D20453F31550C25CBB4EE</idno>
				</biblStruct>
			</sourceDesc>
		</fileDesc>
		<encodingDesc>
			<appInfo>
				<application version="0.7.2" ident="GROBID" when="2023-03-23T23:20+0000">
					<desc>GROBID - A machine learning software for extracting information from scholarly documents</desc>
					<ref target="https://github.com/kermitt2/grobid"/>
				</application>
			</appInfo>
		</encodingDesc>
		<profileDesc>
			<abstract>
<div xmlns="http://www.tei-c.org/ns/1.0"><p>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 FL0 and FLE with cyclic TBoxes and for ALC ∪ * with acyclic TBoxes. We provide constructions for model-msc in these three logics.</p></div>
			</abstract>
		</profileDesc>
	</teiHeader>
	<text xml:lang="en">
		<body>
<div xmlns="http://www.tei-c.org/ns/1.0"><p>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 <ref type="bibr" target="#b14">[15]</ref>. 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.</p><p>Knowledge base completion addresses this issue. In knowledge base completion 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 assumed 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.</p><p>Baader and Sertkaya have developed one knowledge base completion formalism <ref type="bibr" target="#b5">[6]</ref>. 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 arbitrary concept descriptions from the DL FLE <ref type="bibr" target="#b12">[13,</ref><ref type="bibr" target="#b13">14]</ref>. Like Baader and Sertkaya ⋆ supported by Cusanuswerk e. V.</p><p>Rudolph uses an expert-assisted approach similar to attribute exploration from Formal Concept Analysis (FCA) <ref type="bibr" target="#b10">[11]</ref>. 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.</p><p>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.</p><p>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 <ref type="bibr" target="#b1">[2,</ref><ref type="bibr" target="#b6">7]</ref>. 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.</p><p>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 C i 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(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.</p><p>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 <ref type="bibr" target="#b3">[4]</ref>. It is possible to transfer many ideas from FCA to the DL world. This can be exploited to develop a knowledge base completion formalism <ref type="bibr" target="#b4">[5]</ref>.</p><p>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 description logics. In this work we examine the logics FL 0 , FLE 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 FL 0 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.</p><p>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 FL 0 with acyclic TBoxes, but ABox-msc do exist for this logic.</p></div>
<div xmlns="http://www.tei-c.org/ns/1.0"><head n="1">Preliminaries</head></div>
<div xmlns="http://www.tei-c.org/ns/1.0"><head n="1.1">Greatest Fixpoint Semantics</head><p>The description logics that we are considering in this work are FL 0 , FLE, and ALC. FL 0 provides for the concept constructors conjunction (⊓), value restrictions (∀), and the top concept (⊤). FLE extends FL 0 with existential restrictions (∃). In addition to these constructors ALC provides for disjunction (⊔) and negation ¬ and the bottom concept (⊥).</p><p>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.</p><p>An interpretation i = (∆ i , • i ) consists of a set ∆ i and a function mapping every concept name A to a subset A i ⊆ ∆ i and every role name r to a relation r i ⊆ ∆ 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 FL 0 , FLE and ALC are defined in the usual way (cf. <ref type="bibr" target="#b7">[8]</ref> for details). An interpretation i is a model of an acyclic TBox T if A i = C i holds for all statements A ≡ C in T .</p><p>In the case of cyclic TBoxes several possible semantics exist <ref type="bibr" target="#b11">[12]</ref>. The semantics that we use in this work are greatest-fixpoint semantics (or gfp-semantics for short). We denote by N p 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 relation r i ⊆ ∆ i × ∆ i to every r ∈ N r and a set P i ⊆ ∆ i to every P ∈ N p . An interpretation j is based on the primitive interpretation i if it coincides with i on N r and N p and maps every defined concept name A to some A j ⊆ ∆ i . It can be shown that for the logics FL 0 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 <ref type="bibr" target="#b11">[12]</ref>.</p><p>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. 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) ∈ r i 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 i Couple consists of the domain ∆ i Couple = {Carla, Nicolas} and a mapping • i Couple which maps S to {Carla}, P to {Nicolas} and mt to {(Carla, Nicolas), (Nicolas, Carla)}. Figure <ref type="figure" target="#fig_0">1</ref>.1 shows a graph representation of this model.</p></div>
<div xmlns="http://www.tei-c.org/ns/1.0"><head n="1.2">Model-Based Most Specific Concepts</head><p>As usual we write C ⊑ T D if C and D are concept names occurring in T and C i ⊆ D i 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</p><formula xml:id="formula_0">A ⊑ T ′ B iff A ⊑ T B.</formula><p>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.</p><p>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</p><formula xml:id="formula_1">-X ⊆ E i -If T ′ is</formula><p>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 .</p><p>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.</p><p>We say that a GCI C ⊑ D holds in a model i if</p><formula xml:id="formula_2">C i ⊆ D i . A GCI C ⊑ D follows from a set of GCIs L if C ⊑ D holds</formula><p>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.</p><p>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 )}.</p><formula xml:id="formula_3">Proof. Since i is a model for {C ⊑ D} it holds that C i ⊆ D i . The definition of model-msc tells us that mmsc(C i ) ⊑ D<label>(1)</label></formula><p>since mmsc(C i ) is the most specific concept whose extension contains C i .</p><p>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 ). Together with (1) we obtain mmsc(C j ) ⊑ D. But then</p><formula xml:id="formula_4">C j ⊆ mmsc(C j ) j ⊆ D j 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 ).</formula><p>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 <ref type="bibr" target="#b9">[10]</ref>.</p><p>2 Model-Based Most Specific Concepts in Three Different Logics</p></div>
<div xmlns="http://www.tei-c.org/ns/1.0"><head n="2.1">Unfoldable TBoxes</head><p>In FL 0 , 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 <ref type="figure" target="#fig_0">1</ref>.1. E 0 ≡ S, E 1 ≡ ∀mt.∀mt.S, E 2 ≡ ∀mt.∀mt.∀mt.∀mt.S, . . . is a sequence of concept descriptions of increasing role depth. Still Carla ∈ E i k holds for all k ∈ N. If there were a model-msc M for {Carla} then M ⊑ E k 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 E k for all k ∈ N. Since the role depth of the E k goes toward infinity this is impossible.</p></div>
<div xmlns="http://www.tei-c.org/ns/1.0"><head n="2.2">F L 0 with Cyclic TBoxes and gfp-Semantics</head><p>We thus need to find a way to describe cycles in our models. One way to do this is to use gfp-semantics. FL 0 with gfp-semantics has been studied by Baader et al. <ref type="bibr" target="#b0">[1]</ref>. The semantics proposed there make use of semi-automata with word transitions. 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 automaton 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 alphabet, 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 q 1 to a state q 2 on some input w ∈ Σ * if there are words w 1 , w 2 ∈ Σ * such that w = w 1 w 2 and (q 1 , w 1 , q 2 ) ∈ E.</p><p>A finite model i can easily be translated into a semi-automaton</p><formula xml:id="formula_5">A i = (Σ i , Q i , E i ), where Σ i = N r , Q i = ∆ i and E i is the set of all labelled edges (a, r, b) such that (a, b) ∈ r i . A state x is labelled with P ∈ N p iff x ∈ P i holds.</formula><p>Similarly, a cyclic FL 0 -TBox T can be translated into a semi-automaton A T with Σ T = N r . We assume that T is normalized in the sense that every equivalence statement in T is of the form</p><formula xml:id="formula_6">D = ∀W 1 .A 1 ⊓ • • • ⊓ ∀W k .A k .</formula><p>(</p><formula xml:id="formula_7">)<label>2</label></formula><p>The states of A T 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 .</p><formula xml:id="formula_8">E T contains an edge (D, W k , A k ) if this statement contains a term ∀W k .A k .</formula><p>The automata A T and A i 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 ∈ N * r for which A T can move from state A to state P on input w.</p><p>-L(x, y) consists of all words w ∈ N * r for which A i can move from state x to state y on input w. -L(x, P ) = {W ∈ N * r | ∀y ∈ ∆ i : W ∈ L(x, y) implies y ∈ P i }. The following characterization of the semantics of FL 0 -TBoxes with gfpsemantics makes use of these previously defined languages.</p><p>Lemma 2. Let T be a TBox and let A T 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 ∈ D i iff for all primitive concepts P ∈ N p 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 .</p><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. Since the languages L(x, c) are regular this implies that L(x, P ) is also regular.</p><p>Since L(x, P ) is regular for every P ∈ N p , we can find a finite state automaton which accepts L(x, P ). Therefore, there is a semi-automaton A i = (N p , Q i , E i ) and some E ∈ Q i such that L(E, P ) = L(x, P ). By T i denote the TBox that corresponds to A i . Then Lemma 2 shows that x ∈ E i holds. Let T ′ i be conservative extension of T i and let F be a defined concept in T ′ i such that x ∈ F i . Because of Lemma 2 we have L(F, P ) ⊆ L(x, P ) for all P ∈ N p and thus L(F, P ) ⊆ L(E, P ). Using Lemma 2 we obtain E ⊑ T ′ i F . Thus E is the model-msc for x in i. Theorem 1. Let i be a model and x ∈ ∆ i . Let A i be a semi-automaton with a state E for which L(E, P ) = L(x, P ) for all P ∈ N p . Let T i be the TBox that corresponds to A i . Then E in T i is the model-msc for x in i.</p><p>Since it is known that least common subsumers exists in FL 0 with greatest fixpoint semantics, model-msc must also exist for non-singleton sets {x 1 , . . . , x n }. More precisely, we obtain mmsc({x 1 , . . . , x n }) = lcs(mmsc(x 1 ), . . . , mmsc(x n )). 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. 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.</p></div>
<div xmlns="http://www.tei-c.org/ns/1.0"><head>An Example</head><p>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 <ref type="figure">2(a)</ref>. 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.</p></div>
<div xmlns="http://www.tei-c.org/ns/1.0"><head n="2.3">F LE with Cyclic TBoxes and gfp-Semantics</head><p>We have seen in Section 2.1 that model-msc need not exist if we only allow for unfoldable TBoxes. For the case of FL 0 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.</p><p>FLE-TBoxes can be visualized using so-called FLE-description graphs that have been introduced by Baader et al. <ref type="bibr" target="#b7">[8,</ref><ref type="bibr" target="#b8">9]</ref>. Let T be a normalized FLE-TBox. In this context we call T normalized if every concept definition in T is of the form</p><formula xml:id="formula_9">A ≡ P 1 ⊓ • • • ⊓ P k ⊓ ∀r 1 .B 1 • • • ⊓ ∀r l .B l ⊓ ∃s 1 .C 1 • • • ⊓ ∃s m .C m ,<label>(3)</label></formula><p>where A, B 1 , . . . , B l , C 1 , . . . , C m are the names of defined concepts, P 1 , . . . , P k are primitive concept names and r 1 , . . . , r l , s 1 , . . . , s m are defined concept names.</p><p>An FLE-description graph G T is a directed graph with labelled nodes and edges. The nodes of G T 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 P 1 , . . . , P k that occur in its definition. For every term ∀r n .B n in (3) there is an edge from A to B n labelled ∀r n , and for every term ∃s n .C n there is an edge from A to C n labelled ∃s n . 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 <ref type="bibr" target="#b9">[10]</ref>. For an example of an FLE-description graph see the example at the end of this section.</p><p>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 FL 0 . 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 <ref type="bibr" target="#b2">[3]</ref>.</p><p>For a given model i we define the canonical terminology of i as follows. Let G Ti be a description graph whose nodes are all subsets U ⊆ ∆ i where a node U is labelled with P ∈ N p 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 S r,U where S r,U = {x ∈ ∆ i | ∃y ∈ U :</p><p>(x, y) ∈ r i } is the set of all r-successors of some element of U .</p><p>We call the TBox T i that has G Ti as its description graph the canonical terminology of i. For every U ⊆ ∆ i we denote the corresponding concept name by A U , 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 A U in T should be the model-msc for U in i. Now, let us look at the description A U in detail. What is the most specific description of the form ∀r.B that can subsume A U ? Under the assumption that A Sr,U is a most specific concept for S r,U the answer is ∀r.A Sr,U . Since S r,U is the set of all r-successors of some element of U , U ⊆ (∀r.A Sr,U ) i must hold. On the other hand, A Sr,U ⊑ B holds for every B with S r,U ⊆ B i (and thus for every B with U ⊆ (∀r.B) i ). Therefore, ∀r.A Sr,U ⊑ ∀r.B holds for all such B. It therefore makes perfect sense to add to G Ti an edge labelled ∀r pointing from U to S r,U . The intuition for the existential restrictions is similar.</p><p>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 <ref type="bibr" target="#b9">[10]</ref>.</p><p>Theorem 2. Let i be a model for a given set of primitive concept names N p and a set of role names N r . Let U ⊆ ∆ i be a subset of its domain and let T i be the canonical terminology for i. Then A U in T i is the model-msc for i.</p></div>
<div xmlns="http://www.tei-c.org/ns/1.0"><head>An Example</head><p>Let us look at the example from Section 2.2 again. The model i 0 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</p><formula xml:id="formula_10">T i = {A a ≡ ∀r.A b ⊓ ∀s.A ∅ ⊓ ∃r.A b , A b ≡ ∀r.A b ⊓ ∀s.A b ⊓ ∃r.A b ⊓ ∃s.A b , A ∅ ≡ P ⊓ ∀r.A ∅ ⊓ ∀s.A ∅ ⊓ ∃r.A ∅ ⊓ ∃s.A ∅ }.</formula></div>
<div xmlns="http://www.tei-c.org/ns/1.0"><head n="2.4">ALC ∪ *</head><p>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.</p><p>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 (r 1 ∪ r 2 ) i = r i 1 ∪ r i 2 and (r * ) i = (r i ) * for all models i, where (r i ) * denotes the reflexive transitive closure of the binary relation r i .</p><p>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.</p><p>We try to find a model-msc for Carla. For a start consider the concept descriptions D Carla ≡ S⊓¬P⊓∃mt.P⊓∀mt.P and D Nicolas ≡ P⊓¬S⊓∃mt.S⊓∀mt.S D Carla and D Nicolas 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 D Carla . 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 D Nicolas . With the help of the transitive closure of roles we can do something very similar, by defining</p><formula xml:id="formula_11">E Carla ≡ D Carla ⊓ ∀mt * .(¬P ⊔ D Nicolas ) ⊓ ∀mt * .(¬S ⊔ D Carla ).</formula><p>Let j be some model with the same signature as i and x ∈ E j Carla . The term ∀mt * .(¬P ⊔ D Nicolas ) makes sure that every mt * -successor of x is in D j Nicolas if it is in P j (and it is in D j Carla if it is in S j ). Because x is an instance of D Carla we can be sure that every mt-successor of x is a Politician. This means that this successor has to be an instance of D Nicolas , which in turn requires that all its successors are Singers, and so on. This way, we have implictitly added a flavour of cycles to E Carla 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 C x such that {x} = C i x . Then define</p><formula xml:id="formula_12">D x ≡ P ∈Np x∈P i P ⊓ P ∈Np x / ∈P i ¬P ⊓ r∈Nr y∈∆i (x,y)∈r i ∃r.C y ⊓ ∀r. y∈∆i (x,y)∈r i C y ,</formula><p>where we define the empty disjunction to be ⊥ and the empty conjunction to be ⊤. Furthermore define</p><formula xml:id="formula_13">M x ≡ C x ⊓ y∈∆i ∀ r∈Nr r * .(¬C y ⊔ D y ).<label>(4)</label></formula><p>A bisimulation is a relation ζ ⊆ ∆ i × ∆ j with the following three properties. Let (y, y ′ ) ∈ ζ.</p><p>-For every P ∈ N p it holds that y ∈</p><formula xml:id="formula_14">P i iff y ′ ∈ P j . -Forth condition. z ∈ ∆ i , (y, z) ∈ r i ⇒ (∃z ′ ∈ ∆ j : (y ′ , z ′ ) ∈ r j and (z, z ′ ) ∈ ζ) -Back condition. z ′ ∈ ∆ j , (y ′ , z ′ ) ∈ r j ⇒ (∃z ∈ ∆ i : (y, z) ∈ r i and (z, z ′ ) ∈ ζ)</formula><p>Let j = (∆ j , • j ) be a second model over the same signature and let x ′ ∈ M j</p><p>x . 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</p><formula xml:id="formula_15">Z = {(y, y ′ ) | y ∈ ∆ i , y ′ ∈ C j y , (x ′ , y ′ ) ∈ r∈Nr r * j</formula><p>} is a bisimulation. This proves that x and x ′ are indistinguishable. Therefore for every ALC ∪ * concept description D with x ∈ D i it holds that x ′ ∈ D j for all x ′ ∈ M j x . Thus M j x ⊆ D j . Since j was an arbitrary model this implies that M x ⊑ D. Therefore, M x is a most specific concept for {x}. Most specific concepts for non-singleton sets {x 1 , . . . , x n } can be obtained as the disjunction of M x1 , . . . , M xn . Theorem 3. If i is a model over a signature (N p , N r ) then M x as defined in ( <ref type="formula" target="#formula_13">4</ref>) 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 .</p><p>Theorem 3 can be generalized to the case of models that do contain indistinguishable states <ref type="bibr" target="#b9">[10]</ref>.</p></div>
<div xmlns="http://www.tei-c.org/ns/1.0"><head n="3">Conclusion and Future Work</head><p>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 FL 0 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 <ref type="bibr" target="#b4">[5]</ref>. It remains to be examined whether this can also be done for the three logics presented here.</p><p>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.</p><p>Secondly, one might argue that the logics FLE, and FL 0 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.</p></div><figure xmlns="http://www.tei-c.org/ns/1.0" xml:id="fig_0"><head>Fig. 1 .</head><label>1</label><figDesc>Fig. 1. A Graph Representation of a Model</figDesc></figure>
<figure xmlns="http://www.tei-c.org/ns/1.0" xml:id="fig_1"><head>Lemma 3 .LFig. 2 .</head><label>32</label><figDesc>Fig. 2. A Model and Corresponding Semi-Automaton</figDesc></figure>
<figure xmlns="http://www.tei-c.org/ns/1.0" xml:id="fig_2"><head></head><label></label><figDesc>We give a short example of a model i 0 and show how to construct a model-based most specific concept for a ∈ ∆ i0 . Let the model i 0 be defined by ∆ i0 = {a, b}, r i0 = {(a, b), (b, b)}, s i0 = {(b, b)} and P i0 = ∅, where N r = {r, s} and N p = {P }. The semi-automaton A i0 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 T i = {A ≡ ∀s.B, B ≡ P ⊓ ∀r.B ⊓ ∀s.B}. A is the model-msc for a in i 0 .</figDesc></figure>
<figure xmlns="http://www.tei-c.org/ns/1.0" xml:id="fig_3"><head>Fig. 3 .</head><label>3</label><figDesc>Fig. 3. The Canonical Terminology for the Model from Figure 2(a)</figDesc></figure>
		</body>
		<back>
			<div type="references">

				<listBibl>

<biblStruct xml:id="b0">
	<analytic>
		<title level="a" type="main">Using automata theory for characterizing the semantics of terminological cycles</title>
		<author>
			<persName><forename type="first">Franz</forename><surname>Baader</surname></persName>
		</author>
	</analytic>
	<monogr>
		<title level="j">Ann. of Mathematics and Artificial Intelligence</title>
		<imprint>
			<biblScope unit="volume">18</biblScope>
			<biblScope unit="page" from="175" to="219" />
			<date type="published" when="1996">1996</date>
		</imprint>
	</monogr>
</biblStruct>

<biblStruct xml:id="b1">
	<analytic>
		<title level="a" type="main">Least common subsumers and most specific concepts in a description logic with existential restrictions and terminological cycles</title>
		<author>
			<persName><forename type="first">Franz</forename><surname>Baader</surname></persName>
		</author>
	</analytic>
	<monogr>
		<title level="m">Proc. of the 18th Int. Joint Conf. on Artificial Intelligence</title>
				<editor>
			<persName><forename type="first">Georg</forename><surname>Gottlob</surname></persName>
		</editor>
		<editor>
			<persName><forename type="first">Toby</forename><surname>Walsh</surname></persName>
		</editor>
		<meeting>of the 18th Int. Joint Conf. on Artificial Intelligence</meeting>
		<imprint>
			<publisher>Morgan Kaufmann</publisher>
			<date type="published" when="2003">2003</date>
			<biblScope unit="page" from="319" to="324" />
		</imprint>
	</monogr>
</biblStruct>

<biblStruct xml:id="b2">
	<analytic>
		<title level="a" type="main">Terminological cycles in a description logic with existential restrictions</title>
		<author>
			<persName><forename type="first">Franz</forename><surname>Baader</surname></persName>
		</author>
	</analytic>
	<monogr>
		<title level="m">Proc. of the 18th Int. Joint Conf. on Artificial Intelligence (IJCAI 2003)</title>
				<editor>
			<persName><forename type="first">Georg</forename><surname>Gottlob</surname></persName>
		</editor>
		<editor>
			<persName><forename type="first">Toby</forename><surname>Walsh</surname></persName>
		</editor>
		<meeting>of the 18th Int. Joint Conf. on Artificial Intelligence (IJCAI 2003)<address><addrLine>Acapulco, Mexico; Los Altos</addrLine></address></meeting>
		<imprint>
			<publisher>Morgan Kaufmann</publisher>
			<date type="published" when="2003">2003</date>
			<biblScope unit="page" from="325" to="330" />
		</imprint>
	</monogr>
</biblStruct>

<biblStruct xml:id="b3">
	<analytic>
		<title level="a" type="main">A finite basis for the set of EL-implications holding in a finite model</title>
		<author>
			<persName><forename type="first">Franz</forename><surname>Baader</surname></persName>
		</author>
		<author>
			<persName><forename type="first">Felix</forename><surname>Distel</surname></persName>
		</author>
	</analytic>
	<monogr>
		<title level="m">Proc. of the 6th Int. Conf. on Formal Concept Analysis (ICFCA &apos;08)</title>
		<title level="s">Lecture Notes in Artificial Intelligence</title>
		<editor>
			<persName><forename type="first">Raoul</forename><surname>Medina</surname></persName>
		</editor>
		<editor>
			<persName><forename type="first">Sergei</forename><surname>Obiedkov</surname></persName>
		</editor>
		<meeting>of the 6th Int. Conf. on Formal Concept Analysis (ICFCA &apos;08)</meeting>
		<imprint>
			<publisher>Springer</publisher>
			<date type="published" when="2008">2008</date>
			<biblScope unit="volume">4933</biblScope>
			<biblScope unit="page" from="46" to="61" />
		</imprint>
	</monogr>
</biblStruct>

<biblStruct xml:id="b4">
	<analytic>
		<title level="a" type="main">Exploring finite models in the description logic EL gfp</title>
		<author>
			<persName><forename type="first">Franz</forename><surname>Baader</surname></persName>
		</author>
		<author>
			<persName><forename type="first">Felix</forename><surname>Distel</surname></persName>
		</author>
	</analytic>
	<monogr>
		<title level="m">Proc. of ICFCA 2009</title>
				<meeting>of ICFCA 2009</meeting>
		<imprint>
			<publisher>Springer</publisher>
			<date type="published" when="2009">2009</date>
		</imprint>
	</monogr>
</biblStruct>

<biblStruct xml:id="b5">
	<analytic>
		<title level="a" type="main">Completing description logic knowledge bases using formal concept analysis</title>
		<author>
			<persName><forename type="first">Franz</forename><surname>Baader</surname></persName>
		</author>
		<author>
			<persName><forename type="first">Bernhard</forename><surname>Ganter</surname></persName>
		</author>
		<author>
			<persName><forename type="first">Ulrike</forename><surname>Sattler</surname></persName>
		</author>
		<author>
			<persName><forename type="first">Barış</forename><surname>Sertkaya</surname></persName>
		</author>
	</analytic>
	<monogr>
		<title level="m">Proc. of the 20th Int. Joint Conf. on Artificial Intelligence (IJCAI 2007)</title>
				<meeting>of the 20th Int. Joint Conf. on Artificial Intelligence (IJCAI 2007)</meeting>
		<imprint>
			<publisher>AAAI Press/The MIT Press</publisher>
			<date type="published" when="2007">2007</date>
		</imprint>
	</monogr>
</biblStruct>

<biblStruct xml:id="b6">
	<analytic>
		<title level="a" type="main">Computing the least common subsumer and the most specific concept in the presence of cyclic ALN -concept descriptions</title>
		<author>
			<persName><forename type="first">Franz</forename><surname>Baader</surname></persName>
		</author>
		<author>
			<persName><forename type="first">Ralf</forename><surname>Küsters</surname></persName>
		</author>
	</analytic>
	<monogr>
		<title level="m">Proc. of the 22nd German Annual Conf. on Artificial Intelligence (KI&apos;98)</title>
		<title level="s">Lecture Notes in Computer Science</title>
		<meeting>of the 22nd German Annual Conf. on Artificial Intelligence (KI&apos;98)</meeting>
		<imprint>
			<publisher>Springer-Verlag</publisher>
			<date type="published" when="1998">1998</date>
			<biblScope unit="volume">1504</biblScope>
			<biblScope unit="page" from="129" to="140" />
		</imprint>
	</monogr>
</biblStruct>

<biblStruct xml:id="b7">
	<analytic>
		<title level="a" type="main">Computing least common subsumers in description logics with existential restrictions</title>
		<author>
			<persName><forename type="first">Franz</forename><surname>Baader</surname></persName>
		</author>
		<author>
			<persName><forename type="first">Ralf</forename><surname>Küsters</surname></persName>
		</author>
		<author>
			<persName><forename type="first">Ralf</forename><surname>Molitor</surname></persName>
		</author>
	</analytic>
	<monogr>
		<title level="m">Proc. of the 16th Int. Joint Conf. on Artificial Intelligence (IJCAI&apos;99)</title>
				<meeting>of the 16th Int. Joint Conf. on Artificial Intelligence (IJCAI&apos;99)</meeting>
		<imprint>
			<date type="published" when="1999">1999</date>
			<biblScope unit="page" from="96" to="101" />
		</imprint>
	</monogr>
</biblStruct>

<biblStruct xml:id="b8">
	<analytic>
		<title level="a" type="main">Computing least common subsumers for FLE +</title>
		<author>
			<persName><forename type="first">Sebastian</forename><surname>Brandt</surname></persName>
		</author>
		<author>
			<persName><forename type="first">Anni-Yasmin</forename><surname>Turhan</surname></persName>
		</author>
	</analytic>
	<monogr>
		<title level="m">Proc. of DL 2003</title>
				<meeting>of DL 2003</meeting>
		<imprint>
			<publisher>CEUR-WS</publisher>
			<date type="published" when="2003">2003</date>
		</imprint>
	</monogr>
</biblStruct>

<biblStruct xml:id="b9">
	<monogr>
		<title level="m" type="main">Model-based most specific concepts in description logics with value restrictions</title>
		<author>
			<persName><forename type="first">Felix</forename><surname>Distel</surname></persName>
		</author>
		<idno>08-04</idno>
		<ptr target="http://lat.inf.tu-dresden.de/research/reports.html" />
		<imprint>
			<date type="published" when="2008">2008</date>
			<pubPlace>Dresden, Germany</pubPlace>
		</imprint>
		<respStmt>
			<orgName>Institute for theoretical computer science, TU Dresden</orgName>
		</respStmt>
	</monogr>
	<note type="report_type">LTCS-Report</note>
</biblStruct>

<biblStruct xml:id="b10">
	<monogr>
		<title level="m" type="main">Formal Concept Analysis: Mathematical Foundations</title>
		<author>
			<persName><forename type="first">Bernhard</forename><surname>Ganter</surname></persName>
		</author>
		<author>
			<persName><forename type="first">Rudolf</forename><surname>Wille</surname></persName>
		</author>
		<imprint>
			<date type="published" when="1997">1997</date>
			<publisher>Springer</publisher>
			<pubPlace>New York</pubPlace>
		</imprint>
	</monogr>
</biblStruct>

<biblStruct xml:id="b11">
	<analytic>
		<title level="a" type="main">Terminological cycles: Semantics and computational properties</title>
		<author>
			<persName><forename type="first">Bernhard</forename><surname>Nebel</surname></persName>
		</author>
	</analytic>
	<monogr>
		<title level="m">Principles of Semantic Networks</title>
				<editor>
			<persName><forename type="first">John</forename><forename type="middle">F</forename><surname>Sowa</surname></persName>
		</editor>
		<meeting><address><addrLine>Los Altos</addrLine></address></meeting>
		<imprint>
			<publisher>Morgan Kaufmann</publisher>
			<date type="published" when="1991">1991</date>
			<biblScope unit="page" from="331" to="361" />
		</imprint>
	</monogr>
</biblStruct>

<biblStruct xml:id="b12">
	<analytic>
		<title level="a" type="main">Exploring relational structures via FLE</title>
		<author>
			<persName><forename type="first">Sebastian</forename><surname>Rudolph</surname></persName>
		</author>
	</analytic>
	<monogr>
		<title level="j">LNCS</title>
		<editor>K. E. Wolff, H. D. Pfeiffer, and H. S. Delugach</editor>
		<imprint>
			<biblScope unit="volume">3127</biblScope>
			<biblScope unit="page" from="196" to="212" />
			<date type="published" when="2004">2004</date>
			<publisher>ICCS</publisher>
		</imprint>
	</monogr>
</biblStruct>

<biblStruct xml:id="b13">
	<monogr>
		<title level="m" type="main">Relational Exploration -Combining Description Logics and Formal Concept Analysis for Knowledge Specification</title>
		<author>
			<persName><forename type="first">Sebastian</forename><surname>Rudolph</surname></persName>
		</author>
		<imprint>
			<date type="published" when="2006">2006</date>
		</imprint>
		<respStmt>
			<orgName>Technische Universität Dresden</orgName>
		</respStmt>
	</monogr>
	<note type="report_type">PhD thesis</note>
</biblStruct>

<biblStruct xml:id="b14">
	<analytic>
		<title level="a" type="main">Non-standard reasoning services for the debugging of description logic terminologies</title>
		<author>
			<persName><forename type="first">Stefan</forename><surname>Schlobach</surname></persName>
		</author>
		<author>
			<persName><forename type="first">Ronald</forename><surname>Cornet</surname></persName>
		</author>
	</analytic>
	<monogr>
		<title level="m">Proc. of the 18th Int. Joint Conf. on Artificial Intelligence (IJCAI 2003)</title>
				<editor>
			<persName><forename type="first">Georg</forename><surname>Gottlob</surname></persName>
		</editor>
		<editor>
			<persName><forename type="first">Toby</forename><surname>Walsh</surname></persName>
		</editor>
		<meeting>of the 18th Int. Joint Conf. on Artificial Intelligence (IJCAI 2003)<address><addrLine>Acapulco, Mexico; Los Altos</addrLine></address></meeting>
		<imprint>
			<publisher>Morgan Kaufmann</publisher>
			<date type="published" when="2003">2003</date>
			<biblScope unit="page" from="355" to="362" />
		</imprint>
	</monogr>
</biblStruct>

				</listBibl>
			</div>
		</back>
	</text>
</TEI>
