Instance-driven TBox Revision in DL-Lite Zhe Wang1 , Kewen Wang1 , Guilin Qi2 , Zhiqiang Zhuang1 , and Yuefeng Li3 1 School of ICT, Griffith University, Australia 2 School of CSE, Southeast University, China 3 School of EECS, Queensland University of Technology, Australia Abstract. The development and maintenance of large and complex ontologies are often time-consuming and error-prone. Thus, automated ontology learning and revision have attracted intensive research interest. In data-centric applica- tions where ontologies are designed or automatically learnt from the data, when new data instances are added that contradict to the ontology, it is often desirable to incrementally revise the ontology according to the added data. This problem can be intuitively formulated as the problem of revising a TBox by an ABox. In this paper we introduce a model-theoretic approach to such an ontology revision problem by using a novel alternative semantic characterisation of DL-Lite ontolo- gies. We show some desired properties for our ontology revision. We have also developed an algorithm for reasoning with the ontology revision without comput- ing the revision result. The algorithm is efficient as its computational complexity is in coNP in the worst case and in PT IME when the size of the new data is bounded. 1 Introduction A large number of professional and comprehensive ontologies have been developed for accessing data, including the SNOMED CT [23] and the NCI ontologies [9]. The Web Ontology Language (OWL), with its latest version, OWL 2 , is accepted as the WWW Consortium (W3C) recommendation for ontology languages. OWL and OWL 2 are based on description logics (DLs) [2]. Three profiles of OWL 2 are proposed, namely EL, QL and RL , which are based on fine-tuned DLs for efficient reasoning. Existing large ontologies like SNOMED CT are mostly hand-crafted by human experts. The development and maintenance of such large ontologies are often time- consuming and error-prone. Recently, automated ontology learning [3, 15, 13] and re- vision [19, 18, 20, 17, 25, 26] have attracted intensive interest. Although it is often con- ceived that ontologies, once established, are more stable and reliable than data, auto- mated ontology crafting and revision are especially useful in data-centric applications and for pre-mature ontologies. A typical scenario is ontology learning, where termino- logical relations are learnt from example data provided by domain experts, which in DL terms is learning TBox axioms from ABox assertions. Several TBox learning ap- proaches have been proposed in the literature and effective learning tools have been de- veloped [15]. An obvious requirement in ontology learning is that the learnt ontologies must be consistent with the example data. However, when new data instances become available, it is possible that the new data may contradict some previously learnt axioms. Obviously, when the size(s) of the ontology and/or the data is large, it is undesirable to re-learn the ontology from the scratch. Thus, a challenge is how to revise the ontol- ogy according to the new data. In DLs, it amounts to the question of how to effectively revise a TBox by an ABox. TBox debugging and repair approaches [11, 22, 10] and interactive revision ap- proaches [16] can be used to pinpoint the problematic axioms, and most of TBox repair approaches seek to eliminate a minimal number of axioms to restore consis- tency. Similar syntax-based approach was adopted in revision [8, 18, 20]. However, most syntax-based approaches to TBox revision lack of a suitable semantic justifica- tion, which is partially reflected in their inability of preserving implicit knowledge. For example, given T = {Bird v CanFly, Mammal v ¬CanFly}, the revision of T by A = {CanFly(bat), Mammal(bat)} using syntax-based approaches in [8, 20] will dis- card implicit information Bird v ¬Mammal, though it does not involve in the contra- diction. To resolve this issue, some more recent works, such as [5, 6], advocate to define syntax-based ontology revision on the deductive closure cl(T ) of the initial TBox T in- stead of T itself. This of course relies on the finiteness of the deductive closure (with the exception of some special cases), and there may not exist a unique optimal solution to syntax-based revision [5], since often multiple minimal sets of axioms in T (or cl(T )) exist that are responsible for the contradictions. Seeing the TBox as a formalisation of the conceptual model of the data, which is a common perspective in ontology learning, the TBox essentially represents a collection of possible DL models. Taking this perspective, one can argue that in TBox revision, it is critical to ensure minimal changes to the prospective models. Extant model-based TBox revision literature only cover the revision by TBox axioms [17, 26]. In this paper, we develop a novel approach to revise a TBox by ABox assertions, and to full-fill the minimal change principle in a model-theoretic manner. To the best of our knowledge, it is the first work on this direction. However, as witnessed by previous model-based TBox revision approaches, working directly with classical DL models is difficult. Thus, we introduce the type semantics for DL-Litecore , which is the core logic underlying OWL 2 QL. We provide a concrete TBox revision operator based on types. We show that our operator possess desired properties. In particular, our operator supports revision of ax- ioms, and the result of revision is uniquely defined which eliminates non-determinism. For the computational aspects, we transform the entailment problem of TBox revision in DL-Lite into one in propositional logic. We show that entailment checking and revision computation can be done efficiently, and in particular, do not shift the corresponding complexity in propositional logic. 2 Preliminaries A signature S is a union of three disjoint (possibly infinite) sets SC , SR , and SI , where SC is the set of atomic concepts, SR is the set of atomic roles, and SI is the set of individual names. Concepts and roles in DL-Litecore and DL-LiteR are built on atomic ones as follows [4]: B → A | ∃R C → B | ¬B | ⊥ R → P | P− where A ∈ SC and P ∈ SR . B is a basic concept, C is a general concept, and R is a basic role. In what follows, we often use A for an atomic concept, B for a basic concept, C for a general concepts, P for an atomic role, and R for a basic role. B and R denotes the sets of basic concepts and basic roles over S, respectively. We write R− for P if R = P − ; and R+ for P , whenever R = P or R = P − . A DL-Litecore TBox is a finite set of concept inclusions or axiom of the form B v C. An ABox is a finite set of concept assertions of the form A(a) and role assertions of the form P (a, b), where a, b ∈ SI . For the convenience of presentation, we sometimes write P − (a, b) ∈ A meaning P (b, a) ∈ A. A knowledge base (KB) K = T ∪ A consists of a TBox T and an ABox A. In this paper, an ontology is a DL-Lite TBox. The semantics of DL-Litecore is defined as usual using interpretations I = (∆I , ·I ), and we refer to [4] for the details. An interpretation I satisfies inclusion B v C if B I ⊆ C I ; I satisfies assertion A(a) if aI ∈ AI ; and I satisfies assertion P (a, b) if (aI , bI ) ∈ P I . I satisfies TBox T (or ABox A) if I satisfies each inclusion in T (resp., each assertion in A). I is a model of T (A, or T ∪ A) if I satisfies T (resp., A, or both T and A). T ∪ A is consistent if it has at least one model. We also say that T is consistent with A. A concept or role E is satisfiable w.r.t. T if a model I of T exists such that E I 6= ∅; otherwise, E is unsatisfiable. T is coherent if all atomic concepts and atomic roles in T are satisfiable. T ∪ A entails an inclusion or assertion α, written T ∪ A |= α, if all models of T ∪ A satisfy α. Two KBs K1 , K2 are equivalent, written K1 ≡ K2 , if they have the same models. 3 Type Semantics To revise a TBox T by an ABox A, the result of revision should be a new TBox T 0 , such that T 0 is consistent with A and that T 0 preserves as much terminological knowledge as possible from T . We address TBox revision and minimal change from a model- theoretic perspective, that is, the models of the result of revision can be obtained from the models of the initial TBox with minimal change. To achieve this, we adapt classical model-based belief revision to DL-Lite, which measures change through a notion of model distance. However, DL models may have complex structures and the number of models is always infinite. This makes it hard to handle TBox revision directly through classical DL models. Hence, we introduce a new relation of satisfaction for DL-Litecore TBoxes based on the notion of types [14]. Such an alternative semantic characterisation use structures that are finite and much simpler than classical DL models. In TBox revision, it suffices to consider a finite signature S that covers the initial TBox and the new data. In this case, B and R are both finite. Formally, a type τ ⊆ B is a (possibly empty) set of basic concepts. The satisfaction relation between a type τ and a TBox T (or concept C) can be defined in the propositional manner, seeing τ as a propositional interpretation (with basic concepts seen as propositional atoms) and T (or C) as a propositional theory. P M (T ) (P M (C)) denotes the set of types corresponding to the propositional models of T (C). When T = {B v C} is a singleton, we also write P M (B v C). However, classical relation of satisfaction is insufficient and we need to introduce a refined definition of satisfaction. For example, let T = {∃P v ⊥}, then T |= ∃P − v ⊥. Yet P M (T ) 6⊆ P M (∃P − v ⊥), witnessed by the type τ = {∃P − }. For a well defined semantics, one would expect that the models of T are also models of ∃P − v ⊥. Hence, the refined satisfaction relation needs to take care of the non- propositional inference that ∃R v ⊥ implies ∃R− v ⊥ for any R ∈ R, and we will show that this is the only non-propositional inference needing special care in DL- Litecore . In [14, 25], this problem is remedied using a set of types (instead of a single type) in a model. However, the cost of using arbitrary sets of types as in [25] is an exponential blow up on the sizes of models. Although simpler (in particular polynomial- sized) models are defined in [14], the model structures are still rather complex. In what follows, we present a more succinct characterisation, the type semantics, and we will extend the type semantics to ABoxes. Definition 1. A type τ satisfies a DL-Litecore TBox T if the following conditions hold: 1. τ ∈ P M (T ). 2. if T |= ∃R v ⊥ then ∃R− 6∈ τ . In this case, τ is a type model (T-model) of T . The set of T-models of T is denoted as T M (T ). Again, we write T M (B v C) for a singleton TBox T = {B v C}. T-models can be used to characterise the semantics of DL-Litecore TBoxes, and major reasoning problems such as concept satisfiability and subsumption w.r.t. TBoxes can be characterised using T-models. Proposition 1. Given a DL-Litecore TBox T , the following results hold: 1. T is consistent iff there exists a T-model of T . 2. For a concept C, C is satisfiable w.r.t. T iff T M (T ) ∩ P M (C) 6= ∅. 3. For an inclusion B v C, T |= B v C iff T M (T ) ⊆ T M (B v C). 4. For a DL-Litecore TBox T 0 , T ≡ T 0 iff T M (T ) = T M (T 0 ). To prove this proposition, we first show a connection between the classical DL models and the type models of a TBox. Each DL interpretation I and each element d in the domain of I determines a unique type, i.e., τdI = {B ∈ B | d ∈ B I }. We call τdI the type of d in I. Lemma 1. Given a DL-Litecore TBox T and a DL interpretation I, I is a model of T iff τdI ∈ T M (T ) for each d ∈ ∆I . Lemma 1 shows for each DL interpretation I, a set M of types can be determined by I, and I is a model of some DL-Litecore TBox if and only if each element of M is a T-model of the TBox. The following lemma shows the converse is also true—given a T-model τ of a TBox T , a DL model of T can be constructed from τ . Lemma 2. Given a DL-Litecore TBox T and a T-model τ of T , there exists a DL model I of T and a domain element d ∈ ∆I such that τdI = τ . From Lemmas 1 and 2, we can prove Proposition 1. Proposition 1 shows that T-models capture the semantics of DL-Litecore TBoxes. In order to define the revision of a TBox by an ABox, our type semantics needs to define also (partially) the interpretations on the ABox, that is, we need to define which types constitute to the rational interpretations of the ABox. While type semantics cannot completely capture the semantics of ABoxes, due to the fact that types do not refer to individual names, we can define the “type-models” of an ABox A as those types determined by the models of A. As in the definition of interpretation-determined types, where each element in an interpretation uniquely determines a type, each named individual b in A and each in- terpretation I of A uniquely determines a type τbI = {B ∈ B | bI ∈ B I }. As there are often multiple models of A, b is associated with multiple types in A. Formally, type τ is an instance type of b (or a b-type) in A iff it is the type of bI in some model I of A. Intuitively, a b-type in A is the set of basic concepts to whom b is interpreted as a member by some model of A. For example, given A = {A(b), P (b, c)}, type τ = {A, ∃P } is a b-type but not a c-type in A. This is because there exists a model I of A (e.g., the model obtained by seeing A as a complete interpretation) such that τbI = τ ; and for each model I of A, cI ∈ (∃P − )I but ∃P − 6∈ τ . Let T M (b, A) be the set consisting S of all the b-types in A. T M (A) is the set of instance types in A, i.e., T M (A) = b occurs in A T M (b, A). The following proposition says that a TBox T is consistent with an ABox A iff for each individual b occurring in A, there exists a T-model of T that is a b-type. Proposition 2. Given a TBox T and an ABox A in DL-Litecore , T ∪ A is consistent iff T M (T ) ∩ T M (b, A) 6= ∅ for each individual b occurring in A. Without conjunction and disjunction, DL-Litecore cannot capture the full proposi- tional logic. As a result, given a set M of types, M is not always expressible by DL- Litecore TBoxes, i.e., M may not be the set of T-models of any DL-Litecore TBox. Also, the set of T-models of a DL-Litecore TBox T needs to be role balanced. Formally, a set of types is called role balanced if it includes a type containing ∃R whenever it includes a type containing ∃R− for all R ∈ R. Proposition 3. T M (T ) is role balanced for each DL-Litecore TBox T . For a given set M of types, we define a corresponding TBox for M to be one that has the minimal set of T-models that includes M . Formally, a DL-Litecore TBox T is a corresponding TBox to M if M ⊆ T M (T ) and there is no DL-Litecore TBox T 0 such that M ⊆ T M (T 0 ) ⊂ T M (T ). Tcore (M ) denotes a corresponding TBox for M . The corresponding TBoxes are not unique in general, as intuitively often multiple role-balanced minimal supersets exist. For example, suppose M consists of only one type τ = {∃P }. There are two corresponding TBoxes for M that are {∃P − v ∃P } and {∃P − v ¬∃P }, with the T-models (other than τ ) {∃P, ∃P − } and {∃P − }, re- spectively. Intuitively, Definition 1 enforces that a corresponding TBox T of M cannot infer ∃P − v ⊥, and a DL model of T must instantiate ∃P − with at least one mem- ber e. The above two TBoxes correspond to the cases where e is and is not a member of ∃P , respectively. The following proposition shows that role-balance guarantees the uniqueness. Proposition 4. Each role balanced set of types has a unique corresponding TBox (up to semantic equivalence). When a unique corresponding TBox exists, the TBox has the same set of logical consequences in DL-Litecore as the set of types. Lemma 3. Let M be a role balanced set of types and T be its unique corresponding TBox. For each inclusion B v C, M ⊆ P M (B v C) iff T |= B v C. 4 TBox Revision In this section, we use our new semantic characterisation to define a specific TBox revision operator. In classical model-based revision, to revise a propositional knowl- edge base φ by a propositional formula ψ, it is sufficient to select the models of ψ that have minimal distances to those of φ, and to define the propositional knowledge base corresponding to the selected models to be the result of revision. Inspired by classical model-based revision, we first introduce a notion of distance between T-models, and then define a selection function that selects from a set of types those types having min- imal distances to the T-models of the initial TBox. As we will see later, however, a simple adoption of the classical approach to DL-Lite is insufficient to ensure the result of revision has desired properties. We present our novel revision approach tailored for instance-driven TBox revision applications. We adopt a prominent notion of model distance in classical model-based revision introduced by Satoh [21], where the distance between two propositional models (seen as sets of propositional atoms) is defined as the symmetric difference between the two models. The distance between two types τ and τ 0 is their symmetric difference sd(τ, τ 0 ) = (τ \ τ 0 ) ∪ (τ 0 \ τ ). Intuitively, a pair of types τ1 , τ10 are considered to be (strictly) closer than another pair τ2 , τ20 if sd(τ1 , τ10 ) ⊂ sd(τ2 , τ20 ). While we adopt Satoh’s distance, we note that other notions of distance can also be applied in our re- vision framework. Further, given two sets M and M 0 of types, a selection function γ selects the types in M that are closest to those in M 0 , based on the notion of distance. In particular, γ(M, M 0 ) = {τ0 ∈ M | τ00 ∈ M 0 exists s.t. for all τ ∈ M and τ 0 ∈ M 0 , sd(τ, τ 0 ) 6⊂ sd(τ0 , τ00 )} For a TBox T and an ABox A, we could define the revision of T by A to be a TBox corresponding to γ(T M (A), T M (T )), as a straightforward adoption of Satoh’s model- based revision to DL-Lite. However, a result of revision defined in this manner may not be coherent, and moreover, the result of revision is not guaranteed to be consistent with the ABox A. For example, let T = {A v B, A v ¬B} and A = {A(b), B(c)}. Then, γ(T M (A), T M (T )) = T M (A) ∩ T M (T ) consists of a single type {B}. The corre- sponding TBox {A v ⊥} is incoherent and is inconsistent with A. Note that from the above example, to achieve coherence and to ensure consistency with the ABox are not necessarily two separate goals. That is, in many cases like T , the TBox is inconsistent with the ABox because it is incoherent. Hence, if the inconsistency is caused by an un- satisfiable concept or role, then both consistency between the TBox and the ABox and the coherence of the TBox can be recovered simultaneously by revising only the TBox (without changing the ABox). To this end, we introduce the coherence closure A∗ of an ABox A, which extends A with A(cA ) for each A ∈ SC such that no assertion A(a) occurs in A, where cA is a fresh individual name not occurring in A, and extends A with P (cP , dP ) for each P ∈ SR such that no assertion P (a, b) occurs in A, where cP , dP are fresh individual names not occurring in A. In the above example, A∗ = A. Lemma 4. For a TBox T and an ABox A, T is coherent and T ∪ A is consistent iff T ∪ A∗ is consistent. The lemma show that the task of maintaining both the consistency of KB T ∪ A and the coherence of TBox T can be reduced to that of maintaining only the consistency of KB T ∪ A∗ . If T ◦ A is the result of revising T by A, by Proposition 2, the consistency of KB (T ◦ A) ∪ A∗ can be guaranteed by the condition T M (T ◦ A) ∩ T M (b, A∗ ) 6= ∅ for each b occurring in A∗ , i.e., the set of T-models of T ◦A must contain at least one b-type for each individual b in A∗ . It is clear that γ(T M (A∗ ), T M (T )) does not necessarily satisfy this condition, as can be seen from the above example: There are two b-types in A∗ , {A, B} and {A}, and γ(T M (A∗ ), T M (T )) = γ(T M (A), T M (T )) does not contain either of them. Intuitively, for T ◦ A to be consistent with A∗ , the T-models of T ◦ A needs to contain at least one of the b-types. In the example, both b-types have the same distance to the T-models of T (types {B} and ∅) and both b-types should be selected as T-models of T ◦ A. In general, for each individual b occurring in A∗ , the b-types in A∗ that are closest to T M (T ) should be selected. Also, when T is already coherent and is consistent with A, the revision operation should not change T . To this end, all the initial T-models of T are also added as T-models of T ◦ A. Based on the above intuitions, we define our TBox revision operator as follows. Definition 2. Let T be a TBox and A be an ABox in DL-Litecore . The revision of T by A is T ◦ A = Tcore (T M (T ) ∪ MA∗ ) where [ MA∗ = γ(T M (b, A∗ ), T M (T )). b occurs in A∗ Intuitively, MA∗ is constituted by, for each individual b occurring in A∗ , a set of b-types that are closest to the T-models of T . MA∗ is constructed as such in order that the result of revision is consistent with A∗ ; and the result of revising T by A is defined to be a corresponding TBox of T M (T ) ∪ MA∗ . It is not hard to see that T M (T ) ∪ MA∗ is role balanced: For each P ∈ SR , assertion P (b, c) occurs in A∗ for some b, c ∈ SI , and as a result, a b-type containing ∃P and a c-type containing ∃P − are contained in MA∗ . From Proposition 4, T ◦ A is uniquely defined (up to semantic equivalence). Consider the following example adapted from the NCI ontology [9]. Example 1. Let TBox T consists of the following inclusions Heart Disease v ∃has Site, (1) − ∃has Site v Cardiovascular System, (2) − ∃has Site v Respiratory System, (3) Respiratory System v Organ System, (4) Cardiovascular System v Organ System, (5) Respiratory System v ¬Cardiovascular System, (6) Heart Disease v ¬Organ System. (7) The following two inclusions in the original NCI ontology are not DL-Litecore axioms and thus they are replaced with inclusions (1)–(3) . While this is not a precise transla- tion, it is sufficient to demonstrate the application of our new revision in handling such medical ontologies. Heart Disease v ∃has Site.Cardiovascular System, Heart Disease v ∃has Site.Respiratory System. The TBox T is incoherent, as both concept Heart Disease and role has Site are unsat- isfiable. Given A = {Heart Disease(hd1), has Site(hd1, s1), Organ System(s1)}. Then, by Definition 2, T ◦ A consists of inclusions (1), (4)–(7), and the following inclusion ∃has Site− v Organ System. (8) The inclusion (8) can be seen as a revision from axioms (2)–(5). The example shows that our TBox revision operator allows modification of axioms, in contrast to most existing TBox repair approaches that only support axiom removal. Furthermore, the revision operator satisfies the following desired properties pre- sented as AGM-style postulates [12]. Note that our revision operator is different from the classical AGM ones in nature. The classical AGM approach concerns revision be- tween propositional formulas of the same type, whereas our revision approach addresses revising TBox axioms by ABox assertions, which is between different types of first- order formulas. As a result, the following postulates are specially tailored for instance- driven TBox revision. Proposition 5. Let T be a TBox and A be an ABox in DL-Litecore . The following properties hold. (R1) T ◦ A is coherent. (R2) (T ◦ A) ∪ A is consistent. (R3) If T is coherent and T ∪ A is consistent, then T ◦ A ≡ T . (R4) If T1 ≡ T2 and A1 ≡ A2 , then T1 ◦ A1 ≡ T2 ◦ A2 . The first two properties (R1) and (R2) show that the result of revision is coherent and is consistent with the new ABox as required. Then, (R3) says that no revision is needed if the initial TBox is already coherent and consistent with the new ABox. Finally, (R4) shows that the revision operator is syntax-independent, i.e., revising equivalent TBoxes with equivalent new ABoxes results in equivalent revision. 5 Computational Aspects In this section, we first look into the computational complexity of the entailment prob- lem for revision, i.e., the problem of deciding whether T ◦A entails a given TBox axiom B v C. We show that the entailment can be checked without first computing T ◦ A, and is achieved through a reduction to propositional logic. After that, we will provide an algorithm to compute T ◦ A through entailment checking. We show that when the size of A is bounded, the computation can be done in polynomial time. We first show that the entailment problem in DL-Lite can be reduced to one in propositional logic. To this end, we introduce a propositional transformation for DL- Lite TBoxes. This allows us to build essentially a connection between our revision operator and propositional belief revision, and to make use of the existing belief revision results and algorithms in propositional logics, e.g., [7]. The transformation is inspired by [1], which introduces a transformation from a DL-Lite TBox into a theory in the one variable fragment of first order logic. Using type semantics instead of classical DL models allows us to obtain a novel transformation to propositional logic, which is much simpler than theirs. To achieve this, each basic concept in B is assigned a distinct propositional atom, each A to pA and each ∃R to p∃R . Function φ(·) maps each basic concept in B to its corresponding propositional atom, and a general concept to a propositional literal as follows. φ(⊥) = ⊥, φ(A) = pA , φ(∃R) = p∃R , φ(¬B) = ¬φ(B). Then, φ(·) can be extended to map a DL-Litecore TBox T to a propositional formula as follows ^ ^ ¬φ(∃R) ∧ ¬φ(∃R− ) .   φ(T ) = φ(B) → φ(C) ∧ BvC∈T R∈R,T |=∃Rv⊥ Further, to encode the instance types of an ABox, a pair of a DL-Litecore ABox A and an individual name b occurring in A is mapped to a propositional formula as follows. ^ ^ ^ φ(b, A) = φ(A) ∧ φ(∃P ) ∧ φ(∃P − ) A(b)∈A P (b,c)∈A P (c,b)∈A Note that the mapping does not translate an ABox into a propositional formula. Instead, formula φ(b, A) is used to capture the b-types in A. Intuitively, the models of φ(T ) correspond to the T-models of T , and the models of φ(b, A) correspond to the b-types in A, as shown in the following lemma. Let ωτ = {φ(B) | B ∈ τ } for a type τ . mod(φ) denotes the set of models of propositional formula φ. Lemma 5. Let T be a TBox and A be an ABox in DL-Litecore . Then, 1. mod(φ(T )) = {ωτ | τ ∈ T M (T )}; 2. mod(φ(b, A)) = {ωτ | τ ∈ T M (b, A)}. Let ◦s be Satoh’s revision operator in propositional logic. The following connection between our revision operator and Satoh’s holds. Proposition 6. Let T be a TBox andWA be an ABox in DL-Litecore . Given a TBox axiom B v C, T ◦A |= B v C iff φ(T )∨ b occurs in A∗ φ(T )◦s φ(b, A∗ ) ` φ(B) → φ(C).  Proposition 6 allows us to reduce the entailment problem in DL-Litecore to a corre- sponding problem in propositional logic, and thus to make use of existing complexity results for propositional revision. Note that φ(T ) and φ(b, A) are both Horn proposi- tional formulas, and the sizes of them are polynomial in the size of T ∪ A. From the complexity results in [7], it is easy to conclude the following complexity results. In par- ticular, our TBox revision operator for DL-Litecore does not shift the complexity of the propositional case. Theorem 1. For a TBox T , an ABox A, and a TBox axiom B v C in DL-Litecore , deciding T ◦ A |= B v C is in coNP. If the size of A is bounded, i.e., a constant k exists s.t. |A| ≤ k, then deciding T ◦ A |= B v C is in PT IME. The coNP upper bound is not necessarily tight, but mainly shows the connection of our revision operator with the propositional ones. We leave a tight complexity result for the entailment problem in DL-Litecore (with inputs of unbounded sizes) open. Hav- ing a bound on the size of A and the PT IME complexity are practically relevant, as in ontology learning, the newly added example data is often small. The proof is not straightforward as |A| being bounded does not necessarily implies that |A∗ | is bounded. Indeed, the PT IME complexity result holds as long as the number of assertions about each individual in A is bounded. Algorithm 1: Revision Input: TBox T and ABox A in DL-Litecore Output: a DL-Litecore TBox T 0 T 0 := ∅; foreach B1 , B2 ∈ B s.t. B1 6= B2 do if T ◦ A |= B1 v B2 then T 0 := T 0 ∪ {B1 v B2 } ; end if T ◦ A |= B1 v ¬B2 then T 0 := T 0 ∪ {B1 v ¬B2 } ; end end return T 0 ; We provide an algorithm to compute T ◦ A using entailment checking as a sub- method. The algorithm verifies each possible entailment and add those entailed axioms to the result. Proposition 7. Let T be a TBox, A be an ABox in DL-Litecore , and T 0 be the TBox returned by the algorithm Revision. Then, T 0 ≡ T ◦ A. Although DL-Lite ontologies are often associated with large ABoxes, the input ABox A consists of only updated data and thus can be expected to be small. If the size of A is bounded, the algorithm Revision runs in PT IME in the size of T ∪ A. In particular, the number of possible inclusions in DL-Litecore is quadratic to the number of basic concepts in T ∪ A, and the entailment check is in PT IME as discussed. 6 Conclusion We have presented a novel approach to revise a DL-Lite TBox according to newly added ABox instances, and the revision incurs only minimal change to the initial TBox measured in a model-theoretic manner. To the best of our knowledge, our work is the first attempt to address particularly the revision of a TBox by ABox assertions. To tackle this problem, we have introduced the type semantics for DL-Litecore TBoxes, which is superior over the classical DL semantics in that each TBox has a finite number of type models and the new semantics still preserves most of major reasoning forms for DLs. Based on this new semantics, we have developed an operator for revising a TBox by an ABox. We show that the proposed revision operator possesses several desired properties and have also developed an efficient algorithm for computing the revision. We are currently working on extending our approach to DL-LiteR . To address this issue, a key task is to extend the type semantics to DL-LiteR , which needs to take into account the additional non-propositional inferences introduced by role inclusions. It would be also interesting to look into practical applications of our revision approach in ontology learning. References 1. Artale, A., Calvanese, D., Kontchakov, R., Zakharyaschev, M.: The DL-Lite family and re- lations. Journal of Artificial Intelligence Research 36, 1–69 (2009) 2. Baader, F., Calvanese, D., McGuinness, D.L., Nardi, D., Patel-Schneider, P.F.: The Descrip- tion Logic Handbook. Cambridge University Press (2003) 3. Baader, F., Ganter, B., Sertkaya, B., Sattler, U.: Completing description logic knowledge bases using formal concept analysis. In: Proceedings of the 20th International Joint Confer- ence on Artificial Intelligence (IJCAI-07). pp. 230–235 (2007) 4. Calvanese, D., Giacomo, G.D., Lembo, D., Lenzerini, M., Rosati, R.: Tractable reasoning and efficient query answering in description logics: The DL-Lite family. Journal of Auto- matic Reasoning 39(3), 385–429 (2007) 5. Calvanese, D., Kharlamov, E., Nutt, W., Zheleznyakov, D.: Evolution of DL-Lite knowledge bases. In: Proceedings of the 9th International Semantic Web Conference (ISWC-10). pp. 112–128 (2010) 6. Cuenca Grau, B., Ruiz, E.J., Kharlamov, E., Zhelenyakov, D.: Ontology evolution under semantic constraints. In: Proceedings of the 13th International Conference on Principles of Knowledge Representation and Reasoning (KR-12). pp. 137–147 (2012) 7. Eiter, T., Gottlob, G.: On the complexity of propositional knowledge base revision, updates, and counterfactuals. Artificial Intelligence 57, 227–270 (1992) 8. Haase, P., Stojanovic, L.: Consistent evolution of OWL ontologies. In: Proceedings of the 2nd European Semantic Web Conference (ESWC-05). pp. 182–197 (2005) 9. Hartel, F.W., de Coronado, S., Dionne, R., Fragoso, G., Golbeck, J.: Modeling a descrip- tion logic vocabulary for cancer research. Journal of Biomedical Informatics 38(2), 114–129 (2005) 10. Horridge, M., Parsia, B., Sattler, U.: Laconic and precise justifications in OWL. In: Proceed- ings of the 7th International Semantic Web Conference (ISWC-08). pp. 323–338 (2008) 11. Kalyanpur, A., Parsia, B., Sirin, E., Cuenca Grau, B.: Repairing unsatisfiable concepts in OWL ontologies. In: Proceedings of the 3rd European Semantic Web Conference (ESWC- 06). pp. 170–184 (2006) 12. Katsuno, H., Mendelzon, A.: Propositional knowledge base revision and minimal change. Artificial Intelligence 52(3), 263–294 (1991) 13. Konev, B., Lutz, C., Wolter, F.: Exact learning of tboxes in EL and DL-Lite. In: Informal Proceedings of the 26th International Workshop on Description Logics (DL-13). pp. 341– 352 (2013) 14. Kontchakov, R., Wolter, F., Zakharyaschev, M.: Logic-based ontology comparison and mod- ule extraction, with an application to DL-Lite. Artificial Intelligence 174(15), 1093–1141 (2010) 15. Lehmann, J., Hitzler, P.: Concept learning in description logics using refinement operators. Machine Learning 78(1-2), 203–250 (2010) 16. Nikitina, N., Rudolph, S., Glimm, B.: Interactive ontology revision. Journal of Web Seman- tics 12, 118–130 (2012) 17. Qi, G., Du, J.: Model-based revision operators for terminologies in description logics. In: Proceedings of the 21st International Joint Conference on Artificial Intelligence (IJCAI-09). pp. 891–897 (2009) 18. Qi, G., Haase, P., Huang, Z., Ji, Q., Pan, J.Z., Völker, J.: A kernel revision operator for terminologies - algorithms and evaluation. In: Proceedings of the 7th International Semantic Web Conference (ISWC-08). pp. 419–434 (2008) 19. Qi, G., Yang, F.: A survey of revision approaches in description logics. In: Proceedings of the 2nd International Conference of Web Reasoning and Rule Systems (RR-08). pp. 74–88 (2008) 20. Ribeiro, M.M., Wassermann, R.: Base revision for ontology debugging. Journal of Logic Computation 19(5), 721–743 (2009) 21. Satoh, K.: Nonmonotonic reasoning by minimal belief revision. In: Proceedings of the Inter- national Conference on Fifth Generation Computer Systems. pp. 455–462 (1988) 22. Schlobach, S., Huang, Z., Cornet, R., van Harmelen, F.: Debugging incoherent terminologies. Journal of Automated Reasoning 39(3), 317–349 (2007) 23. Spackman, K.A.: M. d. computing. SNOMED RT and SNOMED CT. Promise of an inter- national clinical terminology 17(6), 29 (2000) 24. Staab, S., Studer, R. (eds.): Handbook on Ontologies. Springer-Verlag, 2. edn. (2009) 25. Wang, Z., Wang, K., Topor, R.: A new approach to knowledge base revision in DL-Lite. In: Proceedings of the 24th National Conference on Artificial Intelligence (AAAI-10). pp. 369–374 (2010) 26. Zheleznyakov, D., Calvanese, D., Kharlamov, E., Nutt, W.: Updating TBoxes in DL-Lite. In: Proceedings of the 23rd International Workshop on Description Logics (DL-10) (2010)