# dllite_contraction_and_revision__bc9e5761.pdf Journal of Artificial Intelligence Research 56 (2016) 329-378 Submitted 12/15; published 06/16 DL-Lite Contraction and Revision Zhiqiang Zhuang z.zhuang@griffith.edu.au Institute for Integrated and Intelligent Systems Griffith University, Australia Zhe Wang zhe.wang@griffith.edu.au School of Information and Communication Technology Griffith University, Australia Kewen Wang k.wang@griffith.edu.au School of Information and Communication Technology Griffith University, Australia Guilin Qi gqi@seu.edu.cn School of Computer Science and Engineering Southeast University, China State Key Lab for Novel Software Technology Nanjing University, China Two essential tasks in managing description logic knowledge bases are eliminating problematic axioms and incorporating newly formed ones. Such elimination and incorporation are formalised as the operations of contraction and revision in belief change. In this paper, we deal with contraction and revision for the DL-Lite family through a model-theoretic approach. Standard description logic semantics yields an infinite number of models for DL-Lite knowledge bases, thus it is difficult to develop algorithms for contraction and revision that involve DL models. The key to our approach is the introduction of an alternative semantics called type semantics which can replace the standard semantics in characterising the standard inference tasks of DL-Lite. Type semantics has several advantages over the standard one. It is more succinct and importantly, with a finite signature, the semantics always yields a finite number of models. We then define model-based contraction and revision functions for DL-Lite knowledge bases under type semantics and provide representation theorems for them. Finally, the finiteness and succinctness of type semantics allow us to develop tractable algorithms for instantiating the functions. 1. Introduction Description logic (DL) (Baader, Calvanese, Mc Guinness, Nardi, & Patel-Schneider, 2003) knowledge bases (KBs) are subject to frequent change. For instance, outdated or incorrect axioms have to be eliminated from the KBs and newly formed ones have to be incorporated into them. Therefore a mandatory task for managing DL KBs is to deal with such changes. In the field of belief change, extensive work has been done on formalising various kinds of changes over KBs. In particular, elimination of old knowledge is called contraction and incorporation of new knowledge is called revision. To deal with changes to DL KBs, it makes sense to take advantage of the existing techniques in belief change. In fact, many have investigated contraction and revision over DL KBs (DL contraction and DL revision c 2016 AI Access Foundation. All rights reserved. Zhuang, Wang, Wang, & Qi for short) (Qi et al., 2006; Qi & Du, 2009; Qi et al., 2008; Ribeiro & Wassermann, 2009; Wang et al., 2015). The dominant approach in belief change is the so called AGM framework (Alchourr on, G ardenfors, & Makinson, 1985; G ardenfors, 1988). In this framework, the KB to which changes are made is called a belief set which is a logically closed set of formulas. An AGM contraction function . takes as input a belief set K and a formula φ and returns as output a belief set K . φ that does not entail φ. Taking the same inputs, an AGM revision function returns a belief set K φ that entails φ. The framework also provides rationality postulates which capture the intuitions behind rational contraction and revision. The hallmark of this framework is that the so called representation theorems are proved which ensure that AGM contraction and revision functions are not only sound but also complete with respect to the rationality postulates. Regardless of its wide acceptance, a limitation of the AGM framework is that it has a minimal requirement on the underlying logic, that the logic subsumes classical propositional logic. This means the underlying logic must fully support all the truth functional logical connectives such as negation and disjunction. Since most DLs are not so, the AGM framework is incompatible with DLs and cannot be applied directly to deal with changes over DLs KBs. The incompatibility is the major difficulty in defining DL contraction and revision. Additionally, DL revision is more involved than AGM revision. AGM revision aims to resolve any inconsistency caused while incorporating a new formula. Since a meaningful DL KB has to be both consistent and coherent (i.e, absence of unsatisfiable concepts), DL revision has to resolve not only inconsistency but also incoherence. Finally, despite its mathematical elegance, the AGM framework has been grappled with the issue of computational efficiency which is crucially important for DL KBs. Therefore, DL contraction and revision should lead to tractable instantiations and at the same time respecting the rationality postulates of AGM contraction and revision. Due to the many difficulties, existing works on DL contraction and revision are not fully satisfactory. None of them provides representation theorem for their contraction or revision function except the work by Ribeiro and Wassermann (2009) which inherits the representation results from a more general work (Hansson & Wassermann, 2002).1 In defining DL revision, many did not appreciate its incoherence resolving nature, as their revisions cannot guarantee coherence of the outputs (Qi et al., 2006; Ribeiro & Wassermann, 2009; Wang et al., 2015). Qi and Du (2009) appreciate the incoherence resolving nature, but the postulates they provided for capturing properties of their revision function are not formulated appropriately to capture the rationales behind incoherence resolving. In this paper, we provide DL contraction and revision that overcome these limitations. Specifically, we define contraction and revision functions for logically closed DL-Litecore and DL-Lite R KBs. DL-Litecore and DL-Lite R are the main languages of the DL-Lite family (Calvanese et al., 2007). In defining the functions we take a model-theoretic approach 1. Hansson and Wassermann (2002) proved a series of representation theorems for contraction and revision functions under monotonic and compact logics. Since Ribeiro and Wassermann (2009) considered the same contraction and revision functions for DLs which are monotonic and compact, the representation results of Hansson and Wassermann (2002) also hold for these contraction and revision functions. Since our approach in defining contraction and revision are different from Hansson and Wassermann (2002), we can not inherit their representation results and have to prove them from scratch. DL-Lite Contraction and Revision similar to that of Katsuno and Mendelzon (1992). Instead of DL models the functions are based on models of a newly defined semantics for DL-Lite called type semantics. Given that type semantics is equivalent to DL semantics with respect to major DL-Lite reasoning tasks, models of type semantics (i.e., type models) are more succinct than DL models. More importantly, given a finite signature, any DL-Lite KB has a finite number of type models, whereas it usually has an infinite number of DL models. We fully appreciate the incoherence resolving nature of DL revision and reflect it in both the definition of the revision functions and the postulates capturing their properties. We are able to prove AGM-style representation theorems for all our contraction and revision functions. Such theorems are crucial because they guarantee the functions defined in our method behave properly (in the sense of satisfying a set of commonly accepted postulates) and all properly behaved functions can be defined through our method. In addition to the rigorous mathematical properties, we provide tractable algorithms for instantiating the contraction and revision functions. Some of the material in this paper was presented previously by Zhuang, Wang, Wang, and Qi (2014). DL-Litecore is the core language of the DL-Lite family. It has the following syntax B A | R C B | B R P | P E R | R where A denotes an atomic concept; P an atomic role, P the inverse of the atomic role P; B a basic concept which is either an atomic concept or an unqualified existential quantification; C a general concept which is either a basic concept or its negation; R a basic role which is either an atomic role or its inverse; and E a general role which is either a basic role or its negation. We also include in the language the nullary predicates and that denote universal false and universal truth respectively. We assume the set of all basic concepts, denoted as B, and the set of all basic roles, denoted as R, are finite. For an inverse role R = P , we write R to represent P. A DL-Litecore KB consists of a TBox and an ABox. We sometime denote a KB as (T , A) where T is the TBox of the KB and A is the ABox of the KB. A TBox is a finite set of concept inclusions of the form B C, B , and C. That is only basic concept or can appear on the left-hand side of a concept inclusion. 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 is an atomic concept, P an atomic role, and a, b individuals. We assume the set of all individuals, denoted as D, is finite. Throughout the paper, individual names are denoted by lower case Roma letters (a, b, . . .). A major extension of DL-Litecore is DL-Lite R. It extends DL-Litecore with role inclusions of the form R E. That is only basic roles can appear on the left-hand side of a role inclusion. A concept or role inclusion is also called a TBox axiom and a concept or role assertion is also called an ABox axiom. Throughout the paper, TBox and ABox axioms are denoted by lower case Greek letters (φ, ψ, . . .). The semantics of a DL-Lite language is given in terms of interpretations. An interpretation I = ( I, I) consists of a nonempty domain I and an interpretation function I Zhuang, Wang, Wang, & Qi that assigns to each atomic concept A a subset AI of I, to each atomic role P a binary relation P I over I, and to each individual a an element a I of I. The interpretation function is extended to general concept, general roles, and special symbols as follows: (P )I = {(b, a) | (a, b) P I} ( R)I = {a | b.(a, b) RI} ( B)I = I \ BI ( R)I = I I \ RI The set of all interpretations is denoted as Ω. An interpretation I satisfies a concept inclusion B C if BI CI, a role inclusion R E if RI EI, a concept assertion A(a) if a I AI, and a role assertion P(a, b) if (a I, b I) P I. I satisfies a KB K (a TBox T or an ABox A) if I satisfies all axioms in K (resp. T , A). I is a model of a KB K (a TBox T , an ABox A, or an axiom φ) written I |= K, (resp. I |= T , I |= A, I |= φ) if it satisfies K (resp. T , A, or φ). We denote the models of a KB K (a TBox T , an ABox A, or an axiom φ) as |K| (resp. |T |, |A|, or |φ|). Two axioms φ and ψ are logically equivalent, written φ ψ, if they have identical set of models. A KB K (a TBox T , an ABox A, or an axiom ψ) entails an axiom φ, written K |= φ (resp. T |= φ, A |= φ, or ψ |= φ), if all models of K (resp. T , A, or ψ) are also models of φ. A KB (a TBox, an ABox or an axiom) is consistent if it has at least one model and inconsistent otherwise. We use K , T , A to denote respectively the (unique) inconsistent KB, TBox, and ABox. We use |= φ to denote that φ is a tautology (e.g., A A) and |= φ that φ is not one. The closure of a TBox T , denoted as cl(T ), is the set of all TBox axioms φ such that T |= φ. We say that a TBox T is closed if T = cl(T ). The closure of a DL-Lite TBox is finite. Actually, the size of cl(T ) is quadratic with respect to the size of T (Pan & Thomas, 2007). The closure of an ABox A with respect to a TBox T , denoted as cl T (A), is the set of all ABox axioms φ such that (T , A) |= φ. We say that an ABox A is closed with respect to T if A = cl T (A). The closure of an ABox with respect to a TBox in DL-Lite is finite and can be computed efficiently through a chase procedure (Calvanese et al., 2007). In Section 4 and Section 5, all TBoxes and ABoxes are assumed to be closed. A basic concept B is satisfiable with respect to a TBox T if there is a model I of T such that BI is non-empty and unsatisfiable otherwise. It is easy to see that B is unsatisfiable with respect to T if and only if B cl(T ). A TBox is coherent if all basic concepts are satisfiable and incoherent otherwise.2 In defining contraction and revision functions for DL-Lite KBs, we need to refer to the notion of conjunction of axioms. Given a set of axioms {φ1, . . . , φn}, their conjunction is denoted as φ1 φn. An interpretation is a model of φ1 φn if it satisfies all the conjuncts that is |φ1 φn| = |φ1| |φn|. 2. In DL literatures, often coherence comes with the absence of unsatisfiable atomic concepts. Since in DL-Lite unsatisfiable non-atomic concepts like R are also unexpected we use the stricter condition for coherence. DL-Lite Contraction and Revision 3. Type Semantics In this section, we provide an alternative semantics for DL-Lite, namely type semantics. In short, type semantics takes the semantics underlying propositional logic (i.e., propositional semantics) as the basis and equips it with extra facilities to take care of the nonpropositional behaviours of DL-Lite. We first introduce a simplified version of type semantics called ct-type semantics ( ct stands for Core TBox ), which is sufficient for characterising the standard inference tasks of DL-Litecore TBoxes. An important consideration in defining the semantics is succinctness, that is the defined semantics should avoid any redundancy. With this consideration, cttype semantics has no facility other than those required for characterising the inference tasks of DL-Litecore TBoxes. Accordingly, as DL-Litecore TBoxes do not allow inferences that involve role inclusions or ABox axioms, ct-type semantics is incapable of characterising such inferences. Next, we extend ct-type semantics with the facilities for role inclusions which results in another simplified version of type semantics called t-type semantics ( t stands for TBox ). The semantics is sufficient for characterising the standard inference tasks of DL-Lite R TBoxes. Again, for the sake of succinctness, t-type semantics is intended to capture the inference tasks for DL-Lite R TBoxes only, thus is incapable of characterising those involving ABox axioms. For these inferences, we introduce a-type semantics ( a stands for ABox ). The semantics is sufficient for DL-Lite R ABoxes (with a background TBox). It is also a simplified version of type semantics, but is not built upon ct-type or t-type semantics. Finally, we introduce the full version of type semantics, which is sufficient for DL-Lite R KBs. The semantics includes all facilities of t-type and a-type semantics. Figure 1 shows the hierarchy of type semantics. Figure 1: Each rectangle represents a semantics, with the largest representing type semantics. A rectangle containing one or more smaller ones indicates the represented semantics of the larger rectangle subsumes those of the smaller ones. Zhuang, Wang, Wang, & Qi The propositional origin and the assumption of finite signature guarantee the finiteness of type semantics. As mentioned, an important consideration in defining type semantics is succinctness. The more succinct a semantics is the more efficient the computations involving its models. Type semantics can replace ct-type semantics, t-type semantics, and a-type semantics in characterising DL-Litecore TBoxes, DL-Lite R TBoxes, and DL-Lite R ABoxes; t-type semantics can replace ct-type semantics in characterising DL-Litecore TBoxes. However, it will be a waste of computational power to use type semantics to characterise for instance DL-Lite R TBoxes as its facilities for ABox axioms are redundant for DL-Lite R TBoxes. The same holds in using t-type semantics for characterising DL-Litecore TBoxes as the facilities of t-type semantics for role inclusions are redundant for DL-Litecore TBoxes. The finiteness and succinctness are significant advantages of type semantics over DL semantics when DL-Lite KBs need to be represented model-theoretically and the related computational tasks involve their models. Depending on the application scenarios, changes to DL-Lite KBs may be applied to (1) the whole KB or restricted to either (2) the TBox or (3) the ABox with a background (unchanged) TBox. If we take a model-theoretic approach in addressing the changes, then the most suitable semantics for scenario (1) is type semantics; that for scenario (2) is ct-type or t-type semantics; and that for scenario (3) is a-type semantics. 3.1 Characterising DL-Litecore TBoxes We start with ct-type semantics. Standard inference tasks for DL-Lite TBoxes such as checking satisfiability, subsumption, equivalence, disjointness, and consistency can be reduced to that of checking whether an entailment relationship holds between some TBox axioms. Given a TBox T , a basic concept B is satisfiable in T if and only if T does not entail B ; A is subsumed by B in T if and only if T entails A B; A and B are equivalent in T if and only if T entails A B and B A; A is disjoint with B in T if and only if T entails A B; and T is inconsistent if and only if T |= . For this reason, in defining ct-type (t-type) semantics, it suffices to focus on the entailment relationships between DL-Litecore (resp. DL-Lite R) TBox axioms. In propositional semantics or standard DL semantics, we have the notion of interpretations. Analogously, in type semantics, the central notion is that of types.3 The definition of type will be given in Section 3.4. For ct-type semantics, we only need a simplified version, called ct-type. A ct-type τ is a possibly empty set of basic concepts (i.e., τ B). For example, if B = { R, R , A}, then { R, A} is a ct-type and for simplicity we sometimes write it as RA.4 We denote the set of all ct-types as Ωt c. If we consider basic concepts as propositional atoms, and concept inclusion B C as propositional formula B C, then a ct-type is nothing but an interpretation (represented by atoms interpreted as true) in propositional logic. Given a DL-Litecore TBox T , we use T t c to denote the set of propositional models of the corresponding propositional formulas of T . Note that T t c Ωt c. Many entailment relationships between DL-Litecore TBox axioms are propositional in the sense that the entailments also hold when we treat the axioms as propositional formulas 3. The notion of types is mentioned in the work of Kontchakov et al. (2010), which have similar structures as ct-types in this paper but cannot capture role inclusions or ABox axioms. 4. We work with DL-Lite throughout the paper. Since DL-Lite does not allow quantified existential quantifications such as R.C, the ct-type RA cannot be confused with the concept R.A DL-Lite Contraction and Revision and consider propositional semantics. For example, the entailment from A B and B C to A C also holds for the corresponding propositional formulas A B, B C, and A C, under propositional semantics. As expected there are entailments that are not propositional. The following example shows a common pattern of the non-propositional entailments. Note that, R and R entail one another but, under propositional semantics, the corresponding propositional formulas R and R do not. The reason is simple. For DLs, a role R represents a binary relation and the axiom R and R both indicate the relation is empty. Propositional logic does not have the facility for binary relations and entailments involving such relations, thus can not characterise the entailments. Then it is clear, for ct-type semantics, we need all facilities of propositional semantics to characterise the propositional entailments and an extra one to characterise the nonpropositional ones. We capture such facilities by the conditions under which a ct-type satisfies a DL-Litecore TBox. In DL semantics, interpretations satisfying a TBox is called models of the TBox. Analogously, a ct-type satisfying a DL-Litecore TBox is called a ctmodel of the TBox. Definition 1 A ct-model τ of a DL-Litecore TBox T is a ct-type such that 1. τ T t c and 2. if T |= R then R τ. For a ct-type to satisfy a TBox T , firstly it has to be a propositional model of T and secondly if T entails R , then it can not contain the basic concept R. The first condition guarantees the proper handling of propositional entailments and the second guarantees that of non-propositional entailments. Example 1 Consider a fragment of (slightly modified) NCI KB concerning heart diseases and their associated anatomic locations, which consists of concepts Heart Disease (HD), Cardiovascular System (CS), Respiratory System (RS), and Organ System (OS), as well as a role that relates diseases to their primary locations Disease Has Primary Anatomic Site (Loc). Let DL-Litecore TBox T consist of the following concept inclusions: HD Loc, Loc CS, HD OS, RS OS, CS OS, and RS CS. Some ct-models of T are τ1 = {HD, Loc}, τ2 = { Loc , CS, OS}, and τ3 = {RS, OS}. If concept inclusion Loc RS is in T , then T |= Loc and T |= Loc , and neither τ1 nor τ2 is a ct-model of T . We denote the set of ct-models of a TBox T as |T |t c. The ct-models of a conjunction of axioms φ1 φ2 φn, denoted as |φ1 φ2 φn|t c, is defined as |φ1 φ2 φn|t c = |{φ1, φ2, . . . , φn}|t c. The ct-models of a negated (conjunctions of) axiom(s) φ, denoted | φ|t c, is defined as Ωt c \ |φ|t c. Zhuang, Wang, Wang, & Qi The notions of entailment, logical equivalence, and consistency under ct-type semantics are defined in the same manner as DL semantics. Under ct-type semantics, a TBox T entailing a conjunction φ of axioms is written as T |=t c φ. To make the non-propositional behaviour of ct-type semantics explicit, we propose the following notion of role-complete set of ct-types. A set of ct-types M is role-complete if, for all R R, whenever there is a ct-type τ in M such that R τ, then there is a ct-type τ in M such that R τ (τ and τ may be identical). Roughly speaking, role-completeness indicates that the set of ct-types M have complete information about each role R. We can show that the set of ct-models for any DL-Litecore TBox is role-complete. Proposition 1 Let T be a DL-Litecore TBox. Then |T |t c is role-complete. Now we show some connections between the DL models and the ct-models of a DLLitecore TBox. Let I be a DL interpretation. For each element d in the domain of I, d induces a unique ct-type as follows τ(I, d) = {B B | d BI}. We call τ(I, d) the ct-type induced by d in I. I is a model of some TBox if and only if each ct-type induced by I is a ct-model of the TBox. Proposition 2 Let T be a DL-Litecore TBox and I a DL interpretation. Then I |T | iff τ(I, d) |T |t c for each d I. Moreover, for each ct-model τ of a TBox, a DL model of the TBox can be constructed from τ by reversing the inducing process. Proposition 3 Let T be a DL-Litecore TBox and τ a ct-model of T . Then there are I |T | and d I such that τ(I, d) = τ. Through these connections, we can prove that the entailments over DL-Litecore TBoxes axioms induced by ct-type semantics are identical to those induced by DL semantics. Theorem 1 Let T be a DL-Litecore TBox and φ a conjunction of DL-Litecore TBox axioms. Then T |= φ iffT |=t c φ. Thus ct-type semantics is as effective as DL semantics in characterising the standard inferences tasks of DL-Litecore TBoxes. In comparison with DL semantics, ct-type semantics has the clear advantage of being finite and more succinct. While a DL-Litecore TBox usually has an infinite number of DL models it always has a finite number of ct-models. Proposition 4 Let T be a DL-Litecore TBox. Then T has at most 2n ct-models, for n the number of basic concepts. If we are working with a coherent TBox T , then ct-type semantics shares one more property with DL semantics, that is the set of ct-models of T is identical to the intersection of the set of ct-models of each axiom in T . The property turns out to be essential for developing algorithms for eliminating and incorporating axioms over DL-Lite KBs. It allows us to deal with each axiom one by one in a model-theoretic setting. DL-Lite Contraction and Revision Theorem 2 Let T be a DL-Litecore TBox such that T = {φ1, . . . , φn}. If T is coherent, then |T |t c = |φ1|t c |φn|t c. As we have shown, ct-type semantics shares many crucial properties with DL semantics, however it differs from the DL one in dealing with unions of axioms. Theorem 3 Let T be a DL-Litecore TBox and φ, ψ DL-Litecore TBox axioms. If |T | |φ| |ψ| then |T |t c |φ|t c |ψ|t c but the converse does not necessarily hold. For a counter example, suppose B is {A, B, C, D}, T is {A D}, φ is A B, and ψ is C D. Let s work out their ct-models. A ct-type does not satisfy A D only if it contains A but not D, so we can get the ct-models of T by eliminating all such unsatisfying ct-types from the set of ct-types, that is |T |t c = Ωc \ {AB, AC, ABC}. Similarly, a ct-type does not satisfy both A B and C D only if it contains A and C but not B or D, so |φ|t c |ψ|t c = Ωc \ {AC}. Note that we have |T |t c |φ|t c |ψ|t c. Now let a DL interpretation I be such that I = {a, b}, AI = {a}, BI = {b}, CI = {b}, and DI = {a}. Since I |= T , I |= A B, and I |= C D, we have |T | |φ| |ψ|. Roughly speaking, the reason for such behaviour is that type semantics (and all its simplified versions) is a variant of propositional semantics and it lacks the first-order structure in DL semantics. Identification of such behaviour turns out to be crucial in proving the representation theorem for our contraction functions. Most DLs have the inexpressibility problem that some sets of DL interpretations have no syntactic representation. It is no exception for DL-Litecore under ct-type semantics. Given a set of ct-types M, there may not be a DL-Litecore TBox T whose set of ct-models is M. In such cases, we define a corresponding DL-Litecore TBox for M to be one that has the minimal set of ct-models including M. Definition 2 Let M be a set of ct-types. A DL-Litecore TBox T is a corresponding DLLitecore TBox for M iffM |T |t c and there is no DL-Litecore TBox T such that M |T |t c |T |t c. Given a set of ct-types, we may have several corresponding TBoxes. Let B consists of { R, R , A} and M a set of ct-types consists of A, , and R. Note that there is a ct-type in M that contains R but none of them contains R . By Proposition 1, any TBox whose set of ct-models contains M must have a ct-model that contains R . Since, for the current set of basic concepts B, there are four ct-types containing R which are R , R A, R R, and R A R, we have four corresponding TBoxes for M which are {A R, A R , R R }, {A R, R A, R R }, {A R, A R , R R}, and { R A, R R}, each having M and one of the above ct-types as its ct-models. As shown in the example, if R is in some ct-types of M but R is not, then we have several ways of generating a corresponding TBox. Intuitively if M has both of the concepts, then we don t have that many choices but one for generating a corresponding TBox. Clearly, such M is role-complete and we can show that role-completeness is sufficient to guarantee the uniqueness of corresponding TBox. Theorem 4 Let M be a set of ct-types. If M is role-complete, then there is a unique corresponding DL-Litecore TBox for M. Zhuang, Wang, Wang, & Qi 3.2 Characterising DL-Lite R TBoxes Ct-type semantics is able to characterise the entailments over DL-Litecore TBox axioms, but not those over DL-Lite R ones, as they involve role inclusions. In this subsection, we present t-type semantics which is able to do so. To characterise entailments involving role inclusions, we need to introduce the copy B of the set of basic concepts B and the copy R of the set of basic roles R. So, if B = {A, R, R } and R = {R, R }, then B = {A , ( R) , ( R ) } and R = {R , (R ) }. We also need the notion of extension of a DL-Lite R TBox. Let T be a DL-Lite R TBox. Then its extension, denoted as T , is the TBox obtained by adding to T a new concept inclusion for each concept inclusion B C in T and a new role inclusion R E for each role inclusion R E in T . Note that if C = B, then C denotes B ; and if E = R, then E denotes R . A t-type τ is a possibly empty set of basic concepts, basic roles, and their copies (i.e., τ B R B R ). Intuitively, a t-type combines two ct-types (for pairs of individuals) and a set of roles (between these pairs of individuals). For any pair of individuals a, b such that (a, b) is a relation captured by a role R, the B part of a t-type aims to characterise the constraints to a (in the same way as a ct-type characterises the constraints to each individual); the B part aims to characterises the constraints to b (in the same way as a ct-type characterises the constraints to each individual); and the R R part aims to characterise the constraints to R (which a ct-type does not have to consider). We denote the set of all t-types as Ωt r. If we consider basic concepts, basic roles, and their copies as propositional atoms, and concept inclusion B C and role inclusion R E as propositional formulas B C and R E, then a t-type is nothing but an interpretation (represented by atoms interpreted as true) in propositional logic. For a DL-Lite R TBox T , we use T t r to denote the set of propositional models of the corresponding propositional formulas of T . Note that T t r Ωt r. DL-Litecore permits non-propositional entailments, so does DL-Lite R. While there is only one group of non-propositional entailments for DL-Litecore, four more can be identified for DL-Lite R. (1) Apart from implying R , R also implies R R and R R . (2) The role inclusion R S implies the concept inclusion R S, R S , and the role inclusion R S . (3) The role inclusion R S implies R S . (4) The concept inclusion R S implies the role inclusion R S. In the following, we give the conditions under which a t-type satisfies a DL-Lite R TBox T . We call such t-types t-models of the TBox. Definition 3 A t-model τ of a DL-Lite R TBox T is a t-type such that 1. τ T t r; 2. if T |= R then R τ and ( R) τ; 3. if T |= R S then R τ implies S τ, and ( R) τ implies ( S) τ; 4. if R τ then R τ and ( R ) τ; 5. R τ iff(R ) τ for each R R. DL-Lite Contraction and Revision For a t-type to satisfy T , firstly it has to be a propositional model of T , this takes care of the propositional entailments. Then conditions 2 5 take care of the four groups of nonpropositional entailments summarised earlier. Conditions 4 and 5 are required for any t-type to be a t-model (independent from the TBox), and are referred to as model conditions for t-type semantics. Note that the use of copies of basic concepts and basic roles are necessary. Consider a TBox T with two axioms R A and A S . T entails R S and R S (by (3) and (4)). We would expect the t-models of T also satisfy R S. If copies are discarded, a t-type τ = { R, S, R, S} would be a t-model of T (omitting R and ( R) in Definition 3), yet τ clearly does not satisfy R S. This cannot be resolved by adding a condition in Definition 3 (for details refer to the proof of Lemma 7 in Appendix B). Example 2 (cont d Example 1) Consider another role that associates diseases to some anatomic sites, Disease Has Associated Anatomic Site (Das), and the DL-Lite R TBox T obtained by adding the role inclusion Loc Das to T . Some t-models of T are τ 1 = {HD, Loc, Das, Loc, Das, (Loc ) , (Das ) , ( Loc ) , ( Das ) , (CS) , (OS) }, τ 2 = { Loc , Das , CS, OS, Das , (Das) , ( Das) }, and τ 3 = {RS, OS}. Given a DL-Lite R TBox T , we denote the set of t-models of T as |T |t r. The t-models of a conjunction of DL-Lite R TBox axioms are denoted and defined in the same manner as ct-type semantics. The t-models of a negated (conjunction of) axiom(s) φ,5 denoted as | φ|t r, is defined as {τ Ωt r \ |φ|t r | τ satisfies model conditions}. The notions of entailment, logical equivalence, and consistency under t-type semantics are defined in the same manner as DL semantics. Under t-type semantics, a TBox T entailing a conjunction φ of axioms is written as T |=t r φ. As for DL-Litecore, we can establish a connection between the DL models and t-models of a DL-Lite R TBox. Let I be a DL interpretation and d, e a pair of (not necessarily distinct) elements in the domain of I. Then I, d and e induce a t-type as follows τ(I, d, e) ={B B | d BI} {R R | (d, e) RI} {B B | e BI} {R R | (e, d) RI}. We call τ(I, d, e) the t-type induced by d and e in I. We can show that for each DL interpretation I, I is a DL model of some TBox if and only if each t-type induced by I is a t-model of the TBox. Proposition 5 Let T be a DL-Lite R TBox T and I a DL interpretation. Then I |T | iffτ(I, d, e) |T |t r for each pair of d, e I. Moreover, given a t-model τ of a TBox T , a DL model of T can be constructed from τ by reversing the inducing process. 5. For simplicity, we assume that Definition 3 does not apply to tautologies and define, for any tautological axiom φ, |φ|t r = Ωt r and | φ|t r = . Zhuang, Wang, Wang, & Qi Proposition 6 Let T be a DL-Lite R TBox and τ a t-model of T . Then there is I |T | and d, e I such that τ(I, d, e) = τ. Through these connections, we can prove that t-type semantics induces the same set of entailments over DL-Lite R TBox axioms as that induced by DL semantics. Theorem 5 Let T be a DL-Lite R TBox and φ a conjunction of DL-Lite R TBox axioms. Then T |= φ iffT |=t r φ. Extended with roles and copies of basic concepts, the number of t-types is more than that of ct-types. However, compared with DL semantics, t-type semantics still has the advantage of being finite and more succinct. Proposition 7 Let T be a DL-Lite R TBox. Then T has at most 22n+2m t-models, for n the number of basic concepts and m that of basic roles. For sets of ct-types, we proposed a condition called role-complete. The condition characterises the property of ct-type semantics such that the set of ct-models for any DL-Litecore TBox is role-complete, and any role-complete set of ct-types corresponds to a unique DLLitecore TBox. Now we give the corresponding role-complete condition for sets of t-types. A set of t-types M is role-complete if all t-types in M satisfy the model conditions for t-type semantics, and for all R R, whenever there is a t-type τ in M such that R τ or ( R) τ, then there is a t-type τ in M such that {R, R } τ = (τ and τ may be identical). For a set of t-types M, the corresponding DL-Lite R TBoxes of M are defined in the same way as for a set of ct-types. Also it can be shown analogously that |T |t r is role-complete for any DL-Lite R TBox T and M being role-complete guarantees the existence of a unique corresponding DL-Lite R TBox. Theorem 6 Let M be a set of t-types. If M is role-complete, then there is a unique corresponding DL-Lite R TBox for M. Moreover, properties of ct-type semantics on conjunctions and unions of axioms (i.e., Theorem 2 and Theorem 3) also hold for t-type semantics. So far we have shown that t-type semantics possesses every property of ct-type semantics, except the number of possible models. What about their connections? In fact, t-type semantics generalises ct-type semantics in the sense that for a DL-Litecore TBox T , the ct-models of T are exactly the B-projections of the t-models of T . Proposition 8 Let T be a DL-Litecore TBox. Then |T |t c = {τ B | τ |T |t r}. Hence, t-types contain more information than ct-types, and they are more than enough to capture the semantics of DL-Litecore TBoxes. Finally, we extend the notion of coherence to sets of t-types. A set of t-types M is coherent if and only if all t-types in M satisfy the model conditions for t-type semantics, and M does not satisfy B or R R for each B in B and each R in R (i.e., M |B |t r and M |R R|t r). If M is a coherent set of t-types, then every basic DL-Lite Contraction and Revision concept and role are contained in some t-types of M. Therefore a coherent set of t-types is always role-complete. It will be clear that, in defining contraction and revision functions for DL-Lite R TBoxes, the sets of t-types we will encounter are always coherent thus are role-complete which means we always have unique corresponding TBoxes. We let Tr be a function that takes as input a set of t-types M and is such that if M is coherent, then Tr(M) is the closure of the corresponding DL-Lite R TBox, otherwise Tr(M) = T . 3.3 Characterising DL-Lite R ABoxes (with a Background TBox) T-type semantics extends ct-type semantics with the ability of characterising entailments involving role inclusions. Both of them, however, are incapable of characterising entailments over ABox axioms. In this subsection, we introduce a-type semantics which is able to do so. As for TBoxes, we can also reduce the standard inferences tasks of ABoxes to that of checking an entailment relationships between some ABox axioms. Thus in defining a-type semantics, it suffices to focus on such entailment relationships. Although our focus is on entailments over ABox axioms, it is important to note that such entailments are induced by a background TBox. For example, if A(a) entails B(a), then it must be that the background TBox entails A B. For the sake of simplicity, we sometimes denote an ABox A as AT to indicate that the background TBox is T . A TBox captures subsumption relationships between concepts (i.e., concept inclusions) and those between roles (i.e., role inclusions) whereas an ABox captures assertions over individuals (i.e., concept assertions) and pairs of individuals (i.e., role assertions). In an ABox, an individual can be asserted to be an element of a basic concept and a pair of individuals can be asserted to an element of a basic role. To this end, we introduce a copy Ba of B for each a in D and a copy Rab of R for each pair of a, b in D. So, if B = {A, R, R }, R = {R, R }, and D = {a, b}, then Ba = {Aa, Ra, ( R )a}, Bb = {Ab, Rb, ( R )b}, Rab = {Rab, (R )ab}, Rba = {Rba, (R )ba}, Raa = {Raa, (R )aa}, and Rbb = {Rbb, (R )bb}. An a-type τ is a possibly empty set of such copies of basic concepts and roles (i.e., τ S a D Ba S a,b D Rab). We denote the set of all a-types as Ωa r. For any DL-Lite R TBox T , we let T a be the TBox that consists of for each concept inclusion B C in T and each individual a in D, a concept inclusion Ba Ca, and for each role inclusion R E in T and each pair of individuals a, b in D, a role inclusion Rab Eab. If we consider copies of basic concepts and roles as propositional atoms, concept inclusion B C as propositional formula B C, role inclusion R E as propositional formula R E, concept assertion A(a) as propositional formula Aa, (i.e., an atomic formula) and role inclusion P(a, b) as propositional formula P ab, (i.e., an atomic formula) then an a-type is nothing but an interpretation (represented by atoms interpreted as true) in propositional logic. For a DL-Lite R ABox AT we use AT a r to denote the set of propositional models of the corresponding propositional formulas of T a and A. Note that AT a r Ωa r. Since entailments over axioms of an ABox AT have a lot to do with axioms of the background TBox T , we have to embed some facilities of t-type semantics6 into a-type semantics. With these considerations, the conditions under which an a-type satisfies a DL-Lite R ABox AT is defined as follows and we call such a-types a-models of the ABox. 6. Note that conditions 1 5 in Definition 4 are adapted from those in Definition 3. Zhuang, Wang, Wang, & Qi Definition 4 An a-model τ of a DL-Lite R ABox AT is an a-type such that 1. τ AT a r; 2. if T |= R then ( R)a τ for each a D; 3. if T |= R S then ( R)a τ implies ( S)a τ for each a D; 4. if Rab τ then ( R)a τ and ( R )b τ; 5. Rab τ iff(R )ba τ for each R R and each pair of a, b D. Similarly, conditions 4 and 5 are referred to as model conditions for a-type semantics. Example 3 (cont d Example 2) Consider DL-Lite R KB K = (T , A) where A consists of a concept assertion HD(d) and a role assertion Loc(d, s). An a-model of AT is τ = {HDd, ( Loc)d, ( Das)d, Locds, Dasds, (Loc )sd, (Das )sd, ( Loc )s, ( Das )s, CSs, OSs}. We denote the set of a-models of a DL-Lite R ABox AT as |AT |a r. The a-models of a conjunction φ1 φ2 φn of DL-Lite R ABox axioms with respect to a background TBox T , denoted as |(φ1 φ2 φn)T |a r, is defined as |(φ1 φ2 φn)T |a r = |{φ1, φ2, . . . , φn}T |a r. The a-models of a negated (conjunction of) axiom(s) φ with respect to a background TBox T , denoted as | φT |a r, is defined as | T |a r \ |φT |a r where | T |a r is the set of a-models of an empty ABox when the background TBox is T . The notions of entailment, logical equivalence, and consistency under a-type semantics are defined in the same manner as DL semantics. Under a-type semantics, an ABox AT entailing a conjunction φ of ABox axioms is written as AT |=a r φ. We can establish a connection between the DL models and the a-models of a DL-Lite R ABox, and this connection is a tighter one. Compared with ct-type and t-type semantics, atype semantics contains information about individuals, thus is closer to a DL interpretation. For this reason, each DL interpretation I induces exactly one a-type. The inducing process is as follows. τ a(I) ={Bc Bc | c D, c I BI} {Rcb Rcb | c, b D, (c I, b I) RI}. We call τ a(I) the a-type induced by I. We can show that for each DL interpretation I, I is a model of a KB K = (T , A) if and only if I is a model of T and the a-type induced by I is an a-model of the ABox AT . Proposition 9 Let K = (T , A) be a DL-Lite R KB and I a DL interpretation. Then I |K| iffI |T | and τ a(I) |AT |a r. Moreover, given an a-model τ of a ABox AT , a DL model of the KB K = (T , A) can be constructed from τ by reversing the inducing process. DL-Lite Contraction and Revision Proposition 10 Let K = (T , A) be a DL-Lite R KB and τ an a-type. If τ |AT |a r, then there is I |K| such that τ a(I) = τ. Through these connections, we can show that a-type semantics induces the same set of entailments over DL-Lite R ABox axioms (with a background TBox) as that induced by DL semantics. Theorem 7 Let K = (T , A) be a DL-Lite R KB, φ a conjunction of DL-Lite R ABox axioms. Then K |= φ iffAT |=a r φ. Although we include multiple copies of basic concepts and roles to capture DL-Lite R ABoxes, the semantics is still more superior than DL semantics in terms of finiteness and succinctness. Proposition 11 Let A be a DL-Lite R ABox. Then AT has at most 2nm+n2l a-models, for n the number of individuals, m that of basic concepts, and l that of basic roles. Moreover properties of ct-type and t-type semantics on conjunctions and unions of TBox axioms also hold for a-type semantics on ABox axioms. It is important to note that, if the TBoxes T and T are not equivalent, then the amodels of AT may be different from those of AT (i.e., |AT |a r = |AT |a r). Thus to identify the corresponding ABoxes for a set of a-types we have to fix the background TBox. Definition 5 Let T be a DL-Lite R TBox and M a set of a-types. Then a corresponding DL-Lite R ABox for M with respect to T is a DL-Lite R ABox A such that M |AT |a r and there is no DL-Lite R ABox A such that M |A T |a r |AT |a r. Note that if an ABox A is an empty set, then the set of a-models of AT is not the set of all a-types, as we still have the background TBox to restrict the set of satisfying a-types. For a set of a-types M and a DL-Lite R TBox T , we say M is consistent with T if all a-types in M are a-models of the empty ABox with T as the background TBox (i.e., M | T |a r). We can show that for a set of a-types M, consistency with the background TBox ensures the existence and uniqueness of corresponding DL-Lite R ABox for M with respect to T . Theorem 8 Let T be a DL-Lite R TBox T and M a set of a-types. If M is consistent with T , then there is a unique corresponding DL-Lite R ABox for M with respect to T . We let AT r be a function that takes as input a set of a-types M and is such that if M is consistent with T , then AT r (M) is the closure of the corresponding DL-Lite R ABox with respect to T , otherwise AT r (M) is the inconsistent ABox A . 3.4 Characterising DL-Lite R KBs We have shown that t-type and a-type semantics are capable of characterising respectively entailments over the TBox of a KB and those over the ABox. Intuitively, by combining the two we can characterise entailments over the KB. In fact this is how the full version of type semantics is defined. Zhuang, Wang, Wang, & Qi Recall that a t-type is any subset of B B R R where B and R are copies of B and R and an a-type is any subset of S a D Ba S a,b D Rab where Ba and Rab are copies of B and R for each individual a and each pair of individuals a, b. A type τ is the union of a pair of t-type and a-type, that is τ B B R R S a D Ba S a,b D Rab. We denote the set of all types as Ωr. Note that for any type τ, its t-type part τt can be obtained by intersecting τ with B B R R and its a-type part τa can be obtained by intersecting τ with S a D Ba S a,b D Rab. A type τ satisfies a KB K = (T , A) if and only if τt is a t-model of T and τa is an a-model of AT . We call such types type models of K. Definition 6 A type model τ of a DL-Lite R KB K = (T , A) is a type such that τt |T |t r and τa |AT |a r. We denote the set of type models of a DL-Lite R KB K as |K|r. The type models of a conjunction and a negation of DL-Lite R axioms7 are denoted and defined in the same manner as ct-type semantics. The notions of entailment, logical equivalence, and consistency under type semantics are defined in the same manner as DL semantics. Under type semantics, a KB K entailing an DL-Lite R axiom φ is written as K |=r φ. We can establish a connection between the DL models and the type models of a KB. Let I be a DL interpretation. For each pair of (not necessarily distinct) elements d, e in the domain of I, d and e induce a type as follows. τ (I, d, e) = τ(I, d, e) τ a(I). We call τ (I, d, e) the type induced by d and e in I. Note that τ(I, d, e) induces a t-type and τ a(I) induces an a-type which forms receptively the t-type and the a-type part of the induced type. We can show that for each DL interpretation I, I is a model of some KB if and only if each type induced by I is a type model of the KB. Proposition 12 Let K be a DL-Lite R KB and I a DL interpretation. Then I |K| iff τ (I, d, e) |K|r for each pair d, e I. Also we can construct a DL model of some KB from each type model of the KB. Proposition 13 Let K be a DL-Lite R KB. If τ |K|r, then there is I |K| and d, e I such that τ (I, d, e) = τ. Through these connections, we can show that type semantics induces the same set of entailments over DL-Lite R axioms as that induced by DL semantics. Theorem 9 Let K be a DL-Lite R KB and φ a conjunction of DL-Lite R axioms. Then K |= φ iffK |=r φ. Since type semantics is obtained by combining t-type and a-type semantics, it inherits the finiteness and succinctness properties from the two. 7. A DL-Lite R axioms is either a DL-Lite R TBox axiom or DL-Lite R ABox axiom. DL-Lite Contraction and Revision Proposition 14 Let K be a DL-Lite R KB. Then K has at most 2(n+2)m+(n2+2)l type models, for n the number of individuals, m that of basic concepts, and l that of basic roles. Now we give the corresponding role-complete condition for sets of types. A set of types M is role-complete if all types in M satisfy the model conditions for t-type semantics and a-type semantics, and for any R R, whenever there is a type τ in M such that R τ, ( R) τ, or ( R)a τ for some a D, then there is a type τ in M such that {R, R , Rbc} τ = for some b, c D (τ and τ may be identical, and any pair among a, b, c may be identical). For a set of types M, the corresponding KB is defined in the same way as ct-type semantics. Also it can be shown analogously that |K|r is role-complete for any DL-Lite R KB K and M being role-complete guarantees the existence of a unique corresponding DLLite R KB. Theorem 10 Let M be a set of types. If M is role-complete, then there is a unique corresponding DL-Lite R KB for M. By now we have introduced all versions of type semantics, ranging from the simplest ct-type to the most comprehensive one presented in this subsection. Assuming the same signature, we have Ωt c Ωt r, Ωa r Ωr, and Ωa r Ωt r Ωr. Their characterising abilities which are depicted in Figure 1 match these subset relationships. 4. Axiom Elimination In this section, we deal with the elimination of axioms from DL-Lite KBs. There are several application scenarios for such elimination, which are (1) to eliminate axioms from a TBox while no ABox is considered; (2) to eliminate axioms from an ABox while a background TBox is assumed and remains unchanged; and (3) to eliminate axioms from a KB while both of its TBox and ABox are considered and subject to change. As discussed in the previous section, although type semantics can be used in all scenarios, it will be a waste of computational power to use it for scenarios (1) and (2) for which the simpler ct-type, t-type and a-type semantics can be used. We will only pursue scenario (1) as the other two can be handled in the same manner. The only difference is that in those scenarios we have to switch the underlying semantics to a-type and to type semantics. Our strategy for axiom elimination is to define a contraction function . that takes as input a logically closed TBox T and a conjunction of TBox axioms φ and returns as output a TBox T . φ such that φ is not entailed. For convenience, T is called the original TBox, φ the contracting axiom, and T . φ the contracted TBox. In defining the contraction functions, our approach is inspired by that of Katsuno and Mendelzon (1992). However, we take a more general approach in which no explicit ordering over models is assumed and instead of propositional models we work with t-type models. Also we assume the original TBox is coherent. We only present contraction functions for DL-Lite R TBoxes as those for DL-Litecore ones can be defined and instantiated analogously. Thus KBs, TBoxes, ABoxes, and axioms are assumed to be DL-Lite R ones throughout this section. Zhuang, Wang, Wang, & Qi 4.1 Eliminating Axioms from a TBox Intuitively, if the model set of a TBox contains some counter-models of an axiom φ (i.e, models of φ) then the TBox does not imply φ. Thus, to eliminate an axiom φ from a TBox T we can first add some counter-models of φ to those of T to form an intermediate model set then obtain the corresponding TBox of the model set. Since the intermediate model set contains counter-models of φ, we can be sure that the obtained TBox does not entail φ. Note that to apply this approach, a decision has to be made on which counter-models to add. The extralogical information required for making the decision could be provided by a domain expert of the KB. To study the theoretical properties we assume there is a selection function that plays the role of decision making. A limiting case is when the set of counter-models is empty that is the contracting axiom is a tautology. As it is not possible to stop a TBox from implying a tautology, a convenient and reasonable way is to do nothing and return the original TBox. In line with this intuition, a selection function should return the empty set in such cases. Formally, γ is a selection function if and only if for any set of t-types M, γ(M) is a non-empty subset of M unless M is empty. Selection function has to be further restricted to handle the special case when T does not entail φ. In this case, the model set of T contains counter-models of φ. Intuitively, if asked to eliminate an axiom that is not entailed by the TBox then nothing has to be done and the original TBox should be returned as the outcome. In line with this intuition, a selection function is required to be faithful such that if the intersection of models of T and those of φ is not empty, then the selection function picks the intersecting models and no others. Formally, a selection function γ is faithful with respect to a TBox T if γ(M) = |T |t r M whenever |T |t r M = , for any set of t-types M. With the above considerations, our contraction function called T-contraction function is defined as follows. Recall that Tr is a function that takes as input a set of t-types M and is such that if M is coherent, then Tr(M) is the closure of the corresponding DL-Lite R TBox, otherwise Tr(M) = T . Definition 7 A function . is a T-contraction function for a TBox T ifffor all conjunctions of TBox axioms φ T . φ = Tr(|T |t r γ(| φ|t r)) where γ is a faithful selection function for T . Note that each r-model in the intermediate model set |T |t r γ(| φ|t r) satisfies the model conditions for t-type semantics, and since the original TBox T is assumed to be coherent, |T |t r γ(| φ|t r) which includes models of T must be coherent. Now we present properties of T-contraction functions. It is commonly accepted that the AGM postulates for contraction best capture the desirable properties of contraction functions. In the following, we adapt the AGM postulates and some of their alternatives to the current contraction problem where T is a closed TBox and φ, ψ are conjunctions of TBox axioms. (T . 1) T . φ = cl(T . φ) (T . 2) T . φ T DL-Lite Contraction and Revision (T . 3) If T |= φ, then T . φ = T (T . 4) If |= φ, then T . φ |= φ (T . 5) T cl((T . φ) {φ}) (T . de) If T |= ψ and |T . φ|t r |φ|t r |ψ|t r then T . φ |= ψ (T . 6) If φ ψ, then T . φ = T . ψ According to the postulates, a contraction function is syntax-insensitive (T . 6) and produces a closed TBox (T . 1) which does not entail the contracting axiom unless it is a tautology (T . 4). The produced TBox is not larger than the original one (T . 2). If the contracting axiom is not entailed, then nothing has to be done (T . 3). The AGM origin of (T . 5) is called Recovery and is the main postulate for formalising the minimal change principle for contraction. It requires the information loss during contraction to be minimal such that the original TBox can be recovered through expanding the contracted TBox by the contracting axiom. Recovery has been criticised by many researchers among which Hansson (1991) argued that it is an emerging property rather than a fundamental postulate for contraction. One evidence is that other than the contraction itself, its satisfaction relies also on properties (viz, AGM-compliance) of the underlying logic (Ribeiro et al., 2013). In particular most of the DLs including DL-Lite are incompatible with Recovery. Due to the controversy of Recovery, many have proposed alternative postulates for capturing the minimal change principle. In the quest of a proper postulate for DL-Lite, we notice that Recovery can be replaced by the following postulate of Disjunctive Elimination (Ferm e et al., 2008): If ψ K and φ ψ K . φ then ψ K . φ. Disjunctive Elimination captures the principle of minimal change by stating the condition for retaining a formula during a contraction. That is if a formula is in the original belief set and its disjunction with the contacting formula is retained during the contraction then the formula is retained. Since disjunction of axioms is not permitted in DL-Lite, in adapting the postulate we describe the disjunction in terms of their models, thus the postulate (T . de). Notice that we use t-models instead of DL models in (T . de). Due to the property of t-type semantics on unions of axioms, we have |T . φ| |φ| |ψ| implies |T . φ|t r |φ|t r |ψ|t r but not vice versa. Thus using DL models instead of t-models enforces a stricter condition for retaining ψ which means less number of axioms will be retained after the contraction. It is obvious that the principle of minimal change favours the use of t-models. We can show that a T-contraction function satisfies (T . 1) (T . 4), (T . de), and (T . 6) and all functions satisfying these postulates are T-contraction functions. In other words, the set of postulates fully characterises the properties of a T-contraction function. Theorem 11 A function . is a T-contraction function for a TBox T iff. satisfies (T . 1) (T . 4), (T . de), and (T . 6). Zhuang, Wang, Wang, & Qi By now we have presented the definition of T-contraction functions and their properties. It is should be clear that a T-contraction function cannot be seen as an update operator in KB update literatures. Such operators (e.g., Winslett s operator, see Winslett, 1990) usually apply a fixed rule or update semantics (e.g., WIDTIO) in determining the update outcome. For T-contraction functions, the rule for deciding the contraction outcome is simulated by the associated selection function. It is important to note that, we intentionally leave open the details of the selection function except that we require it to be faithful. Thus it is flexible enough to simulate any rules that respect the faithfulness condition. In fact, our T-contraction function represents a general framework for dealing with changes to DL KBs and it subsumes many update operators in the sense that the rules such operators applied can be simulated by some faithful selection functions. In the remaining of this section, we provide an algorithm called TCONT which implements one such operator. Algorithm 1: TCONT Input: TBox T and conjunction of TBox axiom φ Output: TBox T φ 1 if φ is a tautology or T |= φ then 2 return T φ := T ; 3 Let τ = Pick Counter Model(φ); 4 foreach ψ T do 5 if τ |=t r ψ then 6 T := T \ {ψ}; 7 return T φ := T ; TCONT takes as input a TBox T and a conjunction of TBox axioms φ, and return as output a TBox. TCONT first checks if φ is a tautology or not implied by T (line 1) in which case T is returned (line 2). Otherwise the procedure Pick Counter Model is applied which picks a counter-model τ of φ (line 3). Then TCONT checks the counter-model against each axiom in T (line 4). If an axiom is not satisfied by τ (line 5) then it is removed from T (line 6). Finally, whatever is left of T is returned (line 7). The procedure Pick Counter Model takes a conjunction of TBox axioms φ and return a counter-model of φ. Essential, its goal is to obtain a t-model τ of φ and this can be achieved for example through the following two steps: (1) Consider one conjunct φ1 in φ, and if φ1 = B D with B, D B, let τ contain B but not D; otherwise if φ1 = B D (or φ1 = R S with R, S R), let τ contain both B and D (resp., both R and S); otherwise if φ1 = R S, let τ contain R but not S (or contain R but not S). (2) Add other elements to τ so that it satisfies model conditions for t-type semantics. TCONT runs in polynomial time with respect to the size of T and φ. In particular, checking whether φ is a tautology or T entails φ takes polynomial time (line 1), the procedure Pick Counter Model as shown above runs in linear time, and each satisfiability check (line 5) runs in linear time. Proposition 15 Let T be a TBox and let φ be a conjunction of TBox axioms. Then TCONT(T , φ) terminates and returns a TBox in polynomial time with respect to the size of DL-Lite Contraction and Revision T and φ and if . is a function such that T . φ = TCONT(T , φ), then . is a T-contraction function. Example 4 (cont d Example 2) The logical closure of T contains axiom, among others, Loc RS, which is derived from Loc CS and RS CS. To contract φ := Loc RS from T , TCONT takes both T and φ as input. In line 3, suppose a counter-model τ = { Loc , Das , CS, RS, OS} is selected. τ does not satisfy Loc RS or RS CS, and hence these two axioms (and only these two) are eliminated from the closure. 5. Axiom Incoporation In this section, we deal with the incorporation of axioms into DL-Lite KBs. Similar to axioms elimination, there are three application scenarios that are often encountered, which are (1) to incorporate axioms into a TBox while no ABox is considered; (2) to incorporate axioms into an ABox while a background TBox is assumed and remains unchanged; and (3) to incorporate axioms into a KB while both of its TBox and ABox are considered and subject to change. From previous discussions, it is best to use ct-type or t-type semantics for scenario (1), a-type semantics for scenario (2), and for scenario (3) we have to use the full version of type semantics. We will focus on the scenarios (1) and (2). In managing DL KBs, scenario (3) is less common and it has been handled in (Wang et al., 2015) through a similar approach.8 Similar to axiom elimination, our strategy is to define a revision function that takes as input a logically closed TBox T (or ABox AT ) and a conjunction of TBox axioms (resp. ABox axioms) φ and returns as output a TBox T φ (resp. ABox AT φ) such that φ is entailed. For convenience, T (or AT ) is called the original TBox (resp. ABox), φ the revising axiom, and T φ (resp. AT φ) the revised TBox (resp. ABox). In defining such functions, we assume the original TBox is coherent; the original ABox is consistent with the background TBox9 and the background TBox is itself coherent. In the AGM framework, revision can be constructed indirectly through contraction via the Levi identity (Levi, 1991). Formally, let . be a contraction function for a belief set K, a revision function for K can be defined as K φ = Cn((K . φ) {φ}) for all formulas φ. Since the syntax of DL-Lite does not permit axiom negation the approach is not applicable for DL-Lite. We will define revision functions directly in a model-theoretic approach. As for contraction the approach is inspired that of Katsuno and Mendelzon (1992) and is based on type semantics. We only present revision functions for DL-Lite R as those for DL-Litecore can be defined and instantiated analogously. Thus KBs, TBoxes, ABoxes, and axioms are assumed to be DL-Lite R ones throughout the section. 8. They also proposed an alternative semantic characterisation for DL-Lite but used structures that could be exponentially larger than a type. Hence, a polynomial time algorithm is not available. 9. To be consistent with the background TBox, the ABox itself has to be consistent. Zhuang, Wang, Wang, & Qi 5.1 Incorporating Axioms into a TBox We start with the revision function for incorporating axioms into a TBox. Before presenting the function, we need to clarify a fundamental difference between AGM revision and revision over DL TBoxes (TBox revision for short). AGM revision aims to incorporate new beliefs while resolving any inconsistency. TBox revision goes beyond inconsistency resolving. In addition to consistency, meaningful DL TBoxes have to be coherent, thus TBox revision has to resolve both the inconsistency and incoherence caused in incorporating new axioms.10 Now we give the intuitions behind our revision function. If the model set of a TBox T is the subset of that of an axiom φ then T entails φ. Thus to incorporate an axiom φ into a TBox T , we can pick some models of φ to form an intermediate model set then obtain its corresponding TBox. Since the intermediate model set is the subset of that of φ, we can be sure that the obtained TBox entails φ. Note that to apply this approach, a decision has to be made on which models of φ to pick. As for contraction, a selection function is assumed. Previously, for contraction, a selection function returns the empty set in the limiting case when the contracting axiom is a tautology. Now the limiting case is when the revising axiom is incoherent. As it is not possible to return a coherent TBox that entails an incoherent axiom, a convenient and reasonable way is to do nothing and return the inconsistent TBox. Formally, we define that, a function γ is a selection function if and only if for any set of t-types M, γ(M) is a non-empty subset of M unless M is incoherent. To illustrate the new definition of selection function, suppose in revising T by φ, φ is an incoherent axiom. As discussed, in this case, the revision fails. Since φ is incoherent, its set of t-models must be incoherent. The definition of selection function guarantees that an empty set of t-types is picked which means the revision outcome is the expected inconsistent TBox for indicating failure of the revision. The faithfulness condition also has to be modified from the contraction case. A selection function γ is faithful with respect to a TBox T if it satisfies 1. if M is coherent, then |T |t r M γ(M), and 2. if |T |t r M is coherent, then γ(M) = |T |t r M. In revising T by φ, condition 1 deals with the case when models of T overlaps with those of φ which means T {φ} is consistent. In line with the principle of minimal change, in this case, the selection function has to pick all the overlapping models to preserve as many as possible the original TBox axioms. Condition 2 deals with the case that not only the overlapping exists but also it is coherent. Since in this case T {φ} is not only consistent but also coherent, the revision boils down to a set union operation (i.e., cl(T {φ})). The selection function therefore picks all the overlapping models and no others. To illustrate the new notion of faithfulness, suppose in revising T by φ, the t-models of φ overlap with those of T (i.e., |φ|t r |T |t r) and the set of overlapping t-models is coherent. Since there is no incoherence to resolve, the most intuitive way to deal with this revision is to add φ to T without making any further change, that is to have the union of φ and T as 10. In fact we can concentrate on incoherence resolving when ABox is not considered. By its definition, a coherent TBox must be consistent. Inconsistency resolving is thus a part of incoherence resolving. DL-Lite Contraction and Revision the revision outcome. Since the set of t-models of this union is |φ|t r |T |t r and the revision outcome is obtained by taking the corresponding TBox of the t-types picked by a selection function, it is clear that in this revision the more intuitive selection function should picked all t-types in |φ|t r |T |t r and no other. In our terms, we call such a selection function faithful. In addition to faithfulness, the selection function has to guarantee the t-types picked are coherent, thus we introduce the following condition. We say a selection function γ is coherent preserving if for all coherent sets of t-types M, γ(M) is coherent. With the above considerations, our revision function called T-revision function is defined as follows. Definition 8 A function is a T-revision function for a TBox T ifffor all conjunctions of TBox axioms φ T φ = Tr(γ(|φ|t r)) where γ is a faithful and coherent preserving selection function. Now we present properties of T-revision functions. Since AGM revision deals with inconsistency, AGM revision postulates are formulated to capture the rationale behind the inconsistency resolving process. TBox revision also deals with incoherence, thus the postulates for TBox revision have to capture the rationale behind not only inconsistency but also incoherence resolving. By replacing conditions on consistency with coherence, AGM revision postulates are reformulated as follows for TBox revision, where T is a closed TBox and φ, ψ conjunctions of TBox axioms. (T 1) T φ = cl(T φ) (T 2) T φ |= φ (T 3) If φ is coherent, then T φ cl(T {φ}) (T 4) If T {φ} is coherent, then cl(T {φ}) T φ (T 5) If φ is coherent, then T φ is coherent (T 6) If φ ψ, then T φ = T ψ (T f) If φ is incoherent, then T φ = T According to the postulates, the revised TBox is closed (T 1), it entails the revising axiom (T 2); if the revising axiom is coherent, then the revised TBox entails no axiom other than those entailed by the original TBox and the revising axiom (T 3); if the revising axiom causes no incoherence then the revised TBox is the closure of the original TBox and the revising axiom (T 4). The revised TBox is coherent whenever the revising axiom is so (T 5); Also the revision function is syntax-insensitive (T 6). Since the revising axiom has to be in the revised TBox, if the revising axiom is itself incoherent then the revised TBox must be so. The failure postulate (T f) requires that in such case we simply return the inconsistent TBox. The purpose of TBox revision is to incorporate an axiom and resolve any incoherence caused. If the input axiom is itself incoherent, then the revision is doomed Zhuang, Wang, Wang, & Qi to be a failure. When it fails there is no ground to argue what a proper revision outcome is, so it comes down to what convention to take. Following AGM revision, we take the convention of returning the inconsistent TBox. The AGM origin of (T f) which states if the revising formula is inconsistent then return the inconsistent belief set, is deducible from the other AGM postulates thus is not postulated explicitly in the AGM framework. We can show that a T-revision function satisfies (T 1) (T 6), and (T f) and all functions satisfying these postulates are T-revision functions. In other words, the set of postulates fully characterises the properties of a T-revision function. Theorem 12 A function is a T-revision function for a TBox T iff satisfies (T 1) (T 6) and (T f). As for T-contraction function, a T-revision function is not an update operator, rather it represents a general framework for incorporating axioms into DL-Lite TBox. As with T-contraction function, a T-revision function subsumes many update operators. In the following, we provide an algorithm called TREVI which implements one such operator. Algorithm 2: TREVI Input: TBox T and conjunction of TBox axioms φ Output: TBox T φ 1 if φ is incoherent then 2 return T φ := T ; // N is the set of atomic concepts and atomic roles in B R 3 foreach F N do 4 if T {φ} |= F F then 5 Let τ = Pick Sat Model(φ, F); 6 foreach ψ T do 7 if τ |=t r ψ then 8 T := T \ {ψ}; 9 return T φ := cl(T {φ}); TREVI takes as input a TBox T and a conjunction of TBox axioms φ, and return as output a TBox. TREVI starts by checking whether φ is incoherent (line 1), and if so it returns the inconsistent TBox (line 2). Otherwise, it checks for each atomic concept and each atomic role if it is unsatisfiable under the union of T and φ (line 3 4). The union is incoherent if and only if one such concept or role is unsatisfiable. For each unsatisfiable concept or role F, the procedure Pick Sat Model is applied which picks a t-model τ of φ that includes F (line 5). Then TREVI checks τ against each axiom in T (line 6). If an axiom is not satisfiable under τ (line 7), then it is removed from T (line 8). Finally, the closure of the union of whatever are left of T and φ is returned (line 9). The procedure Pick Sat Model takes a conjunction of TBox axiom φ and an atomic concept or role F and return a t-model of φ that includes F. This can be achieved for example through the following four steps: (1) Let τ contain F, and extend τ so that it satisfies {φ} 11 11. Recall that given a TBox T , T represents the extension of T . DL-Lite Contraction and Revision propositionally. (2) If φ |= R S for some R, S R and τ contains R (or ( R) ), then let τ contain S (resp., ( S) ). (3) Further extend τ so that it satisfies model conditions for t-type semantics. (4) Repeat steps (1) (3) till τ no longer changes. TREVI runs in polynomial time with respect to the size of T and φ. In particular, checking coherence of φ (line 1) takes polynomial time, each concept or role satisfiability check (line 4) takes polynomial time, procedure Pick Sat Model as shown above takes polynomial time, and each satisfiability check (line 7) takes linear time. Proposition 16 Let T be a TBox and let φ be a conjunction of TBox axioms. Then TREVI (T , φ) terminates and computes a TBox in polynomial time with respect to the size of T and φ and if is a function such that T φ = TREVI (T , φ), then is a T-revision function. Example 5 (cont d Example 2) Adding φ = Das RS to T introduces incoherence, i.e., T {φ} |= Loc , due to Loc CS, RS CS, and Loc Das in T . To revise T with φ, TREVI takes both T and φ as input. In line 5, suppose t-type τ = { Loc , Das , CS, RS, OS} is picked. τ does not satisfy Loc RS or RS CS, and hence these two axioms (and only these two) are eliminated from the closure of T to achieve a coherent union with φ. 5.2 Incorporating Axioms into an ABox Now we turn to the revision function for incorporating axioms into an ABox. When dealing with TBox revision, we argued that since meaningful TBox is coherent, an essential task of the revision is incoherence resolving. Coherence is no longer an issue here, as we assume the background TBox is coherent and it remains unchanged throughout the revision process. Therefore we only need to concern with inconsistency resolving. Also note that we are working with a-type semantics now. The idea for defining T-revision function can also be used here. First, we pick some models of the revising ABox axiom to form an intermediate model set, then return its corresponding ABox as the revised ABox. The decision making on which models to pick is again modelled by a selection function. Formally, a function γ is a selection function if and only if for any set of a-types M, γ(M) is a non-empty subset of M unless M is empty. Recall that by AT we mean an ABox A with a background TBox T . In revising AT by an axiom φ, a special case is when the models of AT overlap with those of φ indicating the KB (T , A {φ}) is consistent. Since there is no inconsistency to resolve, we can simply return the union AT {φ} as the revised ABox. In line with this intuition, a selection function has to pick all the overlapping models and no other and we say the selection function is faithful. Formally, a selection function γ is faithful with respect to an ABox AT if γ(M) = |AT |a r M whenever |AT |a r M = . With the above considerations, our revision function called A-revision function is defined as follows. Recall that AT r is a function that that takes as input a set of a-types M and is such that if M is consistent with T , then AT r (M) is the closure of the corresponding DL-Lite R ABox with respect to T , otherwise AT r (M) is the inconsistent ABox A . Zhuang, Wang, Wang, & Qi Definition 9 A function is an A-revision function for an ABox AT ifffor all conjunctions of ABox axioms φ AT φ = AT r (γ(|{φ}T |a r)) where γ is a faithful selection function. Now we present properties of A-contraction functions. The AGM postulates for revision are commonly accepted to capture the desirable properties of revision. In the following, we adapt them to the current revision problem where AT is a closed ABox, and φ, ψ are conjunctions of ABox axioms. (A 1) AT φ = cl T (AT φ) (A 2) AT φ |=a r φ (A 3) AT φ cl T (AT {φ}) (A 4) If |(A {φ})T |a r = , then cl T (AT {φ}) AT φ (A 5) If |{φ}T |a r = , then |(AT φ)T |a r = (A 6) If φ ψ, then AT φ = AT ψ (A f) If |{φ}T |a r = , then AT φ = A As incoherence resolving is out of the picture, the adapted postulates are like their AGM origins concern with inconsistency resolving. According to the postulates, the revised ABox is closed (A 1); it entails the revising axiom (A 2); it entails no axiom other than those entailed by the original ABox and the revising axiom (A 3); it is the closure of the union of the original ABox and the revising axiom if the revising axiom causes no inconsistency (A 4), and it is consistent whenever the revising axiom is so (A 5); Also the revision function is syntax-insensitive (A 6). In the limiting case that the revising axiom φ is itself inconsistent, since it is not possible to have a revised ABox that entails φ and at the same time be consistent, we take the convention to return the inconsistent ABox as the revised ABox (A f). We can show that an A-revision function satisfies (A 1) (A 6) and (A f) and all functions satisfying these postulates are A-revision functions. In other words, the set of postulates fully characterises the properties of an A-revision function. Theorem 13 A function is an A-revision function for an ABox AT iff satisfies (A 1) (A 6), and (A f). As for T-contraction and T-revision functions, an A-revision function is not an update operator, rather it represents a general framework for incorporating axioms into DL-Lite ABoxes. As with T-contraction and T-revision functions, an A-revision function subsumes many update operators. In the following, we provide an algorithm called AREVI which implements one such operator. AREVI takes as input a TBox T , an ABox A, and a conjunction of ABox axioms φ, and return as output an ABox. AREVI first checks if φ is inconsistent with T (line 1) in DL-Lite Contraction and Revision Algorithm 3: AREVI Input: TBox T , ABox A, and conjunction of ABox axioms φ Output: ABox A φ 1 if φ is inconsistent with T then 2 return A φ := A ; 3 if φ is consistent with (T , A) then 4 return A φ := cl T (A {φ}); 5 Let τ = Pick Model(φ); 6 foreach ψ A do 7 if τ |=a r ψ then 8 A := A \ {ψ} 9 return A φ := cl T (A {φ}); which case the inconsistent ABox is returned (line 2). Otherwise, if the revising axiom is consistent with the original ABox and the background TBox then the union of the axiom and the original ABox is returned (lines 3 4). Otherwise the procedure Pick Model is applied which picks an a-model τ of φ (line 5). Then AREVI checks the a-model against each axiom in A (line 6). If an axiom is not satisfied by τ (line 7) then it is removed from A (line 8). Finally, whatever is left of A is combined with φ and their logical closure is returned (line 9). The procedure Pick Model takes an ABox axiom φ and returns an a-model of φ. This can be achieved for example through the following five steps: (1) Let τ contain the propositional forms of all conjuncts of φ (recall that the propositional form of an ABox axiom A(a) is Aa). (2) Extend τ so that it satisfies T a propositionally. (3) If T |= R S for some R, S R and τ contains ( R)a for some a D, then let τ contain ( S)a. (4) Further extend τ so that it satisfies model conditions for a-type semantics. (5) Repeat steps (2) (4) till τ no longer changes. Proposition 17 Let AT be an ABox and φ be a conjunction of ABox axioms. Then AREVI (T , A, φ) terminates and computes an ABox in polynomial time with respect to the size of A T and φ and if is a function such that AT φ = AREVI (T , A, φ), then is an A-revision function. AREVI runs in polynomial time with respect to the size of T , A and φ. In particular, checking consistency between φ and T (line 1) and between φ and (T , A) (line 3) both take polynomial time. The procedure Pick Model as shown above runs in polynomial time, and each satisfiability check (line 7) takes linear time. Example 6 (cont d Example 3) Adding φ = RS(s) to A introduces inconsistency, due to axioms Loc(d, s) in A, Loc CS and RS CS in T . To revise AT with φ, AREVI takes T , A, and φ as inputs. In line suppose a-type τ = {HDd, ( Loc)d, ( Das)d, Dasds, (Das )sd, ( Das )s, RSs, OSs} is picked. τ does not satisfy Loc(d, s), and hence this assertion (and only this one) are eliminated from the closure of AT to achieve a consistent union with φ. Zhuang, Wang, Wang, & Qi 6. Related Work In dealing with changes to DL KBs, many are like us considering it as a belief change problem (Qi et al., 2006; Qi & Du, 2009; Qi et al., 2008; Ribeiro & Wassermann, 2009; Wang et al., 2015). Qi et al. (2006) gave a weakening based approach for revising ALC KBs. The idea is to weaken the TBox axioms until all inconsistencies are resolved. Qi and Du (2009) and Wang et al. (2015) adapted Dalal s (1988) and Satoh s operators (1988) respectively for revising DL KBs. The main issue with these works is that their revision postulates are not formulated appropriately to capture the rationales of incoherence resolving. Moreover, the adapted revision operators cannot guarantee coherence of the revision outcome. In contrast to our approach, Qi et al. (2008) and Ribeiro and Wassermann (2009) studied contraction and revision over TBoxes and KBs that are not necessarily closed. In particular, Qi et al. (2008) adapted kernel revision (Hansson, 1994). Ribeiro and Wassermann (2009) adapted partial meet contraction and revision (Hansson, 1999) kernel contraction and revision (Hansson, 1994), and semi-revision (Hansson, 1997). Due to the popularity of DL-Lite, many have worked on the problem of updating DLLite KBs (De Giacomo et al., 2009; Calvanese et al., 2010; Kharlamov & Zheleznyakov, 2011; Kharlamov et al., 2013; Lenzerini & Savo, 2011, 2012). The update however has very different meaning from the update operation in belief revision literatures (Katsuno & Mendelzon, 1991). In these works, it can be interpreted as both contraction and revision and they mainly focused on issues with the expressibility of the update outcome. We also tackled the expressibility issues while assuming type semantics. Due to the succinctness and finiteness of type semantics, the issue can be settled relatively easy. Of these works that are more comparable to ours, Lenzerini and Savo (2011) dealt with instance level update, that is the TBox remains unchanged and the ABox undergoes changes. Later Lenzerini and Savo (2012) extended the approach to updating inconsistent KBs. The main idea is to first obtain ABoxes (called repairs) that are consistent with the background TBox; differ minimally from the original ABox; and accomplish the insertion or deletion of certain axioms. Then the intersection of these repairs are taken as the update outcome. The problem setting is similar to that for A-revision functions. Although they targeted a more expressive DL-Lite (i.e., DL-Lite A,id), when considering DL-Lite R their idea can be simulated by our A-revision function. By restricting the associated selection function, an A-revision function can always return the same outcome as their approach. Grau et al. (2012) studied operations that contract and revise at the same time. A constraint which states the set of axioms to be incorporated and those to be eliminated is first specified. Then the operation maps a KB to another that satisfies the constraint. The operation reduces to a revision and contraction function after making empty the so called eliminating set and the incorporating set respectively. However, they did not identify the postulates that characterise the contraction and revision functions. When working with DL-Lite, such functions can be simulated by our T-contraction and T-revision function. In a more general setting, Ribeiro et al. (2013) identified properties of a monotonic logic under which a contraction function can be defined that satisfies the Recovery postulate. By their result, DL-Lite is not one such logic, which is consistent with ours (i.e., Theorem 11). Axiom negation is not supported by most DLs but is required in defining revision functions through contraction functions via the Levi identity. Flouris, Huang, Pan, Plexousakis, and DL-Lite Contraction and Revision Wache (2006) proposed several notions of negated axioms for DLs. They also explored the notions of inconsistent and incoherent TBoxes and emphasised the importance of resolving incoherence in addition to inconsistency. Similar to T-revision function, a group of works usually referred to as ontology debugging also deals with unsatisfiable concepts (e.g., Kalyanpur et al., 2006). The method they used are based on the notion of Minimal Unsatisfiability Preserving Sub-TBoxes (MUPS). For each unsatisfiable concept B, the MUPS based method first computes all the MUPSs for B, then it computes a minimal hitting set for the MUPSs. The incoherence is then resolved by removing axioms in the minimal hitting set. TREVI deals with the same problem in a more efficient way. Roughly speaking each minimal hitting set for the MUPSs corresponds to a t-model formed in line 5 of TREVI , thus we can avoid the computations of the MUPSs and their minimal hitting sets which is a significant saving in computational power. 7. Conclusion Due to the diversity of DLs, it is difficult if not impossible to come up with generalised contraction and revision functions that work best for all DLs. Each DL is unique that they deserve to be treated individually to make the most out of their uniqueness. A distinguishing feature of DL-Lite is that it only allows a restricted version of existential and universal quantifiers. By taking advantage of this feature, we developed type semantics for DL-Lite that resembles the underlying semantics for propositional logic. We then defined and instantiated contraction and revision functions for DL-Lite KBs whose outcomes are obtained by manipulating type models of the KBs and the contracting and revising axioms. Our first contribution is the development of type semantics for DL-Lite. Given that type semantics is equivalent to DL semantics in characterising the standard inference tasks of DL-Lite, it outperforms DL semantics in terms of finiteness and succinctness. Our second contribution is the axiomatic characterisation for the contraction and revision functions. The key in obtaining the result for T-revision functions is the reformulation of AGM revision postulates from inconsistency centred to incoherence centred. As TBox revision deals not only with inconsistency but also incoherence, postulates for TBox revision must capture the rationales behind incoherence resolving. Our third contribution is providing tractable algorithms that instantiate the contraction and revision functions. For future work, we plan to study contraction and revision for DLs that are more expressive than DL-Lite. Since these DLs may allow unrestricted existential and universal quantifiers, concepts can be formed through unbound nesting of quantifies. The semantic characterisation of this kinds of concepts through type semantics may not be possible. We need some other techniques that are tailored to these DLs. Acknowledgement We thank the anonymous reviews for their comments which helped improve the paper substantially. Zhuang, Wang, Wang, & Qi Before presenting the proofs for the technical results, we introduce some notions that will simplify the presentation of the proofs. First, given an ABox A, we write P (a, b) A to mean P(b, a) A. Now we present the notion of chase. Given a DL-Lite R (DL-Litecore) ABox A and TBox T , the chase of A w.r.t. T , denoted chase T (A) is defined procedurally as follows: initially take chase T (A) := A, then exhaustively apply the following rules: if A(s) chase T (A), A A T , and A (s) chase T (A), then chase T (A) := chase T (A) {A (s)}; if A(s) chase T (A), A R T , and there is no t such that R(s, t) chase T (A), then chase T (A) := chase T (A) {R(s, v)} where v is a fresh constant that has not appeared in chase T (A) before; if R(s, t) chase T (A), R A T , and A(s) chase T (A), then chase T (A) := chase T (A) {A(s)}; if R(s, t) chase T (A), R S T , and there is no t such that S(s, t) chase T (A), then chase T (A) := chase T (A) {S(s, v)} where v is a fresh constant that has not appeared in chase T (A) before; if R(s, t) chase T (A), R S T , and S(s, t) chase T (A), then chase T (A) := chase T (A) {S(s, t)}. Note that in the above rules, R and S can be a role or the inverse of a role. It is well known that an ABox A induces a unique interpretation IA such that the domain of IA consists of all the constants in A; for each concept name A, AIA = {d | A(d) A}; and for each role name P, P IA = {(e, f) | P(e, f) A}. In the proofs, we slightly misuse the notation to let A denote also the interpretation induced by A. In this way, chase T (A) can also be used to denote an interpretation. Finally, we present the notions of positive inclusions, negative inclusions, and closures of negative inclusions. We call TBox axioms of the forms B D and R S positive inclusions (PIs), and call axioms of the forms B D and R S negative inclusions (NIs), where B, D B and R, S R. Given a DL-Lite R (DL-Litecore) TBox T , the closure of NIs for T , denoted cln(T ), is defined inductively as follows: All NIs in T are in cln(T ); If B1 B2 T and B2 B3 or B3 B2 is in cln(T ), then B1 B3 cln(T ); If R1 R2 T and R2 B or B R2 is in cln(T ), then R1 B cln(T ); If R1 R2 T and R 2 B or B R 2 is in cln(T ), then R 1 B cln(T ); If R1 R2 T and R2 R3 or R3 R2 is in cln(T ), then R1 R3 cln(T ); If R R or R R or R R is in cln(T ), then all three are in cln(T ). DL-Lite Contraction and Revision It is clear from the above definition that T |= cln(T ). The following result is shown in (Calvanese et al., 2007) which provides a method to build DL models using chase. The result will be used to prove Propositions 3 and 6. Lemma 1 Let (T , A) be a DL-Lite R (DL-Litecore) KB. If A is a model of cln(T ), then chase T (A) is a model of (T , A). Proof for Proposition 1 If there is τ |T |t c such that R τ for some R R, then by condition 2 of Definition 1, T |= R . Thus, there is a model I of T such that RI = . Suppose (d, e) RI, let τ = τ(I, e). Then, R τ . Also, by Proposition 2, τ |T |t c. Proof for Proposition 2 For the if direction, it suffices to show for each d I and each axiom B C in T , d BI implies d CI. Let τ = τ(I, d). Suppose d BI, then by the definition of τ we have B τ. Since τ is a ct-model of T , τ satisfies B C propositionally. If C is a basic concept, then B τ implies C τ; otherwise C = D is a negated basic concept, and B τ implies D τ. In both cases, by the definition of τ, d CI. For the only if direction, let τ = τ(I, d) for an arbitrary d I. We first show that τ T t c. For each concept inclusion B C in T , assume B τ, then d BI. If C is a basic concept, I being a model of T implies d CI, which in turn implies C τ. If C = D is a negated basic concept, then with a similar argument, d DI and D τ. That is, τ satisfies B C propositionally. That is, τ T t c. For the second half of Definition 1, if T |= R then RI = . Clearly, R τ. We have shown that τ |T |t c. Before proving Proposition 3, we first show the following lemma as a preparation. Lemma 2 For a DL-Litecore TBox T , each ct-model τ of T satisfies τ cln(T ) t c. Proof : Towards a contradiction, suppose there exists a ct-model τ of T and an NI α in cln(T ) such that τ does not satisfy α propositionally. We show that τ must violate some NI in T (which contradicts to the fact that τ is a ct-model of T ). We prove this through induction. For convenience, we assume the inclusions in cln(T ) are added inductively following the definition. For initialization, if α is in T then τ violates some NI in T . For induction steps, we show that if α is added to cln(T ) due to another axiom β already in cln(T ), τ violates β. There are two cases: (1) Suppose α is B1 B3, added due to PI B1 B2 in T and NI B2 B3 (or B3 B2) in cln(T ). Then, by the fact that τ does not satisfy α propositionally, {B1, B3} τ. Also, as τ satisfies B1 B2 in T , B2 τ. Hence, τ violates NI B2 B3 (B3 B2). (2) Suppose α is R R, added due to R R in cln(T ). Then, by the fact that τ does not satisfy α propositionally, R τ. As R R |= R , by condition 2 in Definition 1, τ violates NI R R . Proof for Proposition 3 Zhuang, Wang, Wang, & Qi We construct an interpretation Iτ from τ using chase: Let d be a constant, NC be the set of all concept names, and Aτ ={A(d) | A NC τ} {R(d, ed,R) | R τ, ed,R is a fresh constant}. Take Iτ = chase T (Aτ). We want to show that Iτ is a model of T and τ(Iτ, d) = τ. To show the former, by Lemma 1, we only need to show that Aτ is a model of cln(T ). Towards a contradiction, suppose it is not the case, then there is an axiom B D in cln(T ) that is violated by Aτ. This is the case when Aτ |= B(s) and Aτ |= D(s) for some constant s in Aτ. There are essentially four cases (note that B and D are symmetric): (i) Suppose B and D are both concept names, then Aτ |= B(s) and Aτ |= D(s) only if s = d, B(d) Aτ, and D(d) Aτ. From the construction of Aτ, {B, D} τ and thus τ does not propositionally satisfy B D. That is, τ cln(T ) t c, which violates Lemma 2. (ii) Suppose B = R for some R and D is a concept name, then Aτ |= B(s) only if s = d and R(d, t) Aτ for some t, and Aτ |= D(d) only if B(d) Aτ. Thus, {B, R} τ and thus τ does not propositionally satisfy B R. Again, τ cln(T ) t c, which violates Lemma 2. (iii) Suppose B = R for some R and D = S for some S with R = S, then Aτ |= B(s) and Aτ |= D(s) only if R(s, t) Aτ and S(s, u) Aτ for some t, u. This is only when s = d and t, u are fresh constants. In this case, { R, S} τ and τ does not propositionally satisfy R S, which again violates Lemma 2. (iv) Suppose B = R for some R and D = R, then Aτ |= B(s) only if R(s, t) Aτ for some t. This is only when s = d and t is a fresh constant; or t = d and s is a fresh constant. In the former case, R τ, and in the latter case, R τ. Since R cln(T ), T |= R and T |= R . Both cases violate the fact that τ |T |t c and condition 2 in Definition 1. We have shown that Aτ is a model of cln(T ), and thus Iτ is a model of T . Now it remains to show that τ(Iτ, d) = τ. Since it is clear that τ(Aτ, d) = τ, from the definition of chase, τ(Aτ, d) τ(Iτ, d). We only need to show that τ(Iτ, d) τ(Aτ, d). This is equivalent to show that Iτ \ Aτ does not contain any assertion of the form A(d) or R(d, s) such that no assertion R(d, t) Aτ (as otherwise, A or R, respectively, will be in τ(Iτ, d)\τ(Aτ, d) according to the definition of τ(Iτ, d)). Towards a contradiction, suppose there is such an assertion in Iτ \Aτ. From the chase rules, it can happen only if some chase rule is applicable to an assertion g of the form B(d) or S(d, t). Let g be the first of such assertions that triggers a chase rule. By the chase rules, we observe that g must be in Aτ. Suppose g = B(d), then from the construction of Aτ, B τ. If g triggers a chase rule with B A T , then by condition 1 in Definition 1, τ propositionally satisfies B A, and hence A τ and A(d) Aτ, which is a contradiction to (the applicability of) the chase rule; otherwise, g triggers a chase rule with B R T , then by condition 1 in Definition 1, τ B R t c, and thus R τ and R(d, u) Aτ for some u, which again contradicts the chase rule. Suppose g = S(d, t), then from the construction of Aτ, S τ. If g triggering a chase rule with S A, then by condition 1 in Definition 1, τ propositionally satisfies DL-Lite Contraction and Revision S A. As S τ, A τ and A(d) Aτ, which contradicts to the chase rule. If g triggering a chase rule with S R, then τ propositionally satisfies S R, and thus R τ and R(d, u) Aτ for some u, which is again a contradiction. We have shown that Iτ \ Aτ does not contain any assertion of the form A(d) or R(d, s). Thus, τ(Iτ, d) = τ(Aτ, d) = τ. Proof for Theorem 1 If |T | = , then there is a model I |T |. Let d I, and τ = τ(I, d). From Proposition 2, τ |T |t c. That is, |T |t c = . Conversely, suppose |T |t c = , let τ |T |t c. From Proposition 3, there is a model I of T . That is, |T | = . Thus, |T | is empty if and only if |T |t c is empty. If |T | and |T |t c are both empty, the statement trivially holds. In what follows, we assume that |T | and |T |t c are both non-empty. For the if direction, we want to show that if T |= φ then |T |t c |φ|t c. Then, there is a model I of T such that I does not satisfy φ. That is, there is a TBox axiom in the conjunction φ that is not satisfied by I. Without loss of generality, assume φ contains only this (single) TBox axiom. Suppose φ is B C. Then, there is an domain element d I such that d BI and d CI. Let τ = τ(I, d). Since I is a model of T , from Proposition 2, τ is a ct-model of T . If C is a basic concept, then B τ implies d BI and d CI, which in turn implies C τ. If C = D is a negated basic concept, then with a similar argument, B τ implies D τ. That is, τ does not propositionally satisfy B C and τ φ t c. We have shown that |T |t c |φ|t c. For the only if direction, we want to show that if |T |t c |φ|t c then T |= φ. Since |T |t c |φ|t c, there is a ct-type τ |T |t c and τ |φ|t c. From Proposition 3, there exists a model I of T and a domain elements d I such that τ(I, d) = τ. We only need to show that I is not a model of φ. Suppose otherwise, I is a model of φ, then by Proposition 2, τ must be a ct-model of φ, which contradicts the fact τ |φ|t c. Thus, I is not a model of φ, and we have shown that T |= φ. Proof for Theorem 2 For each τ |T |t c, by condition 1 in Definition 1, τ propositionally satisfies φi for i = 1, . . . , n. Moreover, as T is coherent, by the monotonicity of DL-Lite, there exists no R R such that φi |= R . Hence, τ |φi|t c for i = 1, . . . , n. That is, |T |t c |φ1|t c |φn|t c. Conversely, for each τ |φ1|t c |φn|t c, by condition 1 in Definition 1, τ T t c. Further, as T is coherent, there exists no R R such that T |= R . Hence, τ |T |t c. That is, |φ1|t c |φn|t c |T |t c. Proof for Theorem 3 For each τ |T |t c, by Proposition 3, there is a model I |T | and some d I such that τ(I, d) = τ. Since |T | |φ| |ψ|, I |φ| or I |ψ|. Suppose without loss of generality that I |φ|, then by Proposition 2, τ(I, d) |φ|t c. That is, τ |φ|t c. We have shown that |T |t c |φ|t c |ψ|t c. Before presenting the proof for Theorem 4, we first show Lemmas 3 and 4 regarding the union of TBoxes (or equivalently, conjunction of TBox axioms). In a similar way as Zhuang, Wang, Wang, & Qi for Lemma 2, we can show the following lemma. The difference is that we cannot assume each ct-type τ |T1|t c |T2|t c satisfies τ |T1 T2|t c, and thus cannot apply condition 2 in Definition 1 in the proof. Lemma 3 For two DL-Litecore TBox T1 and T2, and a role-complete set M of ct-types with M |T1|t c |T2|t c, it holds that M cln(T1 T2) t c. Proof : Towards a contradiction, suppose there exists a ct-type τ M and an NI α in cln(T1 T2) such that τ does not satisfy α propositionally. We show that some ct-type τ M exists that violates some NI in T1 T2, which contradicts to the fact that M |T1|t c |T2|t c (as τ |T1|t c |T2|t c implies that τ satisfies all the NIs in T1 T2 propositionally). Similar as the proof of Lemma 2, we prove this through induction. For initialization, if α is in T1 T2 then let τ = τ and τ violates some NI in T1 T2. For induction steps, we show that if α is added to cln(T1 T2) due to another axiom β already in cln(T1 T2), we show that some τ M exists that violates β (and eventually take τ = τ when β is in T1 T2). There are two cases: (1) Suppose α is B1 B3, added due to PI B1 B2 in T1 T2 and NI B2 B3 (or B3 B2) in cln(T1 T2). Then, by the fact that τ does not satisfy α propositionally, {B1, B3} τ. Also, as τ satisfies B1 B2 in T1 T2, B2 τ. Hence, let τ = τ and τ violates NI B2 B3 (B3 B2). (2) Suppose α is R R, added due to R R in cln(T1 T2). Then, by the fact that τ does not satisfy α propositionally, R τ. As M is role-complete, there exists some τ M with R τ . Hence, τ violates NI R R . Lemma 4 Let M be a set of ct-types, and φ1, φ2 be two conjunctions of DL-Litecore TBox axioms. Suppose M is role-complete, then M |φ1|t c |φ2|t c implies M |φ1 φ2|t c. Proof : For each τ M, we want to show that τ |φ1 φ2|t c. To this end, we construct a model of φ1 φ2. Let Ti be the set of axioms (as conjuncts) in φi for i = 1, 2, Aτ be as in the proof of Proposition 6, and Iτ = chase T1 T2(Aτ). We can show that Iτ is a model of T1 T2 and τ(Iτ, d) = τ in a similar way as in the proof of Proposition 3 (by using Lemma 3 instead of Lemma 2). Except for case (iv): Suppose Aτ violates R R cln(T1 T2). Note that, different from the proof of Proposition 3, we cannot assume either R R cln(T1) nor R R cln(T2) (That is, we cannot apply condition 2 in Definition 1). Yet we can still derive contradiction. Aτ violates R R only if R(d, t) Aτ with t being a fresh constant or R(s, d) Aτ with s being a fresh constant. In the former case, R τ, and τ does not propositionally satisfy R R. That is, τ cln(T1 T2) t c, which violates Lemma 3. In the latter case, R τ. Since M is role-complete, R τ for some τ M. Hence, τ does not propositionally satisfy R R. That is, τ cln(T1 T2) t c, which again violates Lemma 3. Now, we have shown that Iτ is a model of φ1 φ2 and τ(Iτ, d) = τ. By Proposition 2, τ |φ1 φ2|t c. Proof for Theorem 4 Suppose there are two TBoxes T1 and T2 corresponding to M. That is, M |T1|t c and M |T2|t c. From Lemma 4, M |T1 T2|t c. By the minimality requirement of a DL-Lite Contraction and Revision corresponding TBox, |T1 T2|t c |Ti|t c for i = 1, 2. That is, |T1 T2|t c = |Ti|t c for i = 1, 2. By Theorem 1, T1 is equivalent to T2. Proof for Proposition 5 For the if direction, it suffices to show for each d I and each concept inclusion B C in T , d BI implies d CI; and additionally, for each e I (not necessarily d = e) and each role inclusion R E in T , (d, e) RI implies (d, e) EI. Let τ = τ(I, d, e). Suppose d BI, then by the definition of τ we have B τ. Since τ is a t-model of T , τ propositionally satisfies B C. If C is a basic concept, then B τ implies C τ; otherwise C = D is a negated basic concept, and B τ implies D τ. In both cases, by the definition of τ, d CI. For role inclusion R E, suppose (d, e) RI, then by the definition of τ we have R τ. As τ is a t-model of T , τ propositionally satisfies R E. If E is a role then E τ; otherwise E = S is a negated role and S τ. In both cases, by the definition of τ, (d, e) EI. For the only if direction, let τ = τ(I, d, e) for some arbitrary d, e I. We first show that τ satisfies condition 1 of Definition 3. For each concept inclusion B C in T , assume B τ, then by the definition of τ, d BI. If C is a basic concept, I being a model of T implies d CI, which in turn implies C τ. If C = D is a negated basic concept, then with a similar argument, d DI and D τ. That is, τ propositionally satisfies B C. In a similar way, for each concept inclusion B C in T with B , C B , we can show that τ satisfies B C . For each role inclusion R E in T , assume R τ. Then, by the definition of τ, (d, e) RI. Since I is a model of T , (d, e) EI. If E is a role then E τ; otherwise E = S is a negated role and S τ. Thus, τ propositionally satisfies R E. Similarly, τ satisfies R E for each role inclusion R E in T . We haven shown that τ T t r. We next show that τ satisfies conditions 2 5 of Definition 3. For condition 2, if T |= R then RI = . Clearly, d ( R)I and e ( R )I. By the definition of τ, R τ and ( R ) τ. For condition 3, if T |= R S then ( R)I ( S)I. Suppose R τ, which by the definition of τ implies d ( R)I. Then, d ( S)I, and thus S τ. Similarly, suppose ( R) τ, which implies e ( R)I. Hence, e ( S)I, and thus ( S) τ. For condition 4, if R τ then by the definition of τ, (d, e) RI, which implies d ( R)I and e ( R )I. By the definition of τ, R τ and ( R ) τ. Condition 5 is clearly satisfied by the definition of τ(I, d, e). We have shown that τ satisfies all the conditions in Definition 3, that is, τ |T |t r. Before proving Proposition 6, we first show Lemma 5. Note that cln(T ) is obtained from cln(T ) by adding a copy for each axiom in cln(T ), and cln(T ) t r is the set of t-types that are the propositional models of cln(T ) . Lemma 5 For a DL-Lite R TBox T , each t-model τ of T satisfies τ cln(T ) t r. Proof : Towards a contradiction, suppose there exists a t-model τ of T and an NI α in cln(T ) such that τ does not propositionally satisfy α. We show that τ must violate some NI in T , through induction. Here we only consider α being a NI in cln(T ), and the case of α being a copy of some NI in cln(T ), i.e., α cln(T ) \ cln(T ), can be shown similarly. Zhuang, Wang, Wang, & Qi For initialization, if α is in T then τ violates some NI in T . For induction steps, we show that if α is added to cln(T ) due to another axiom β already in cln(T ), τ violates β. (1) Suppose α is B1 B3, added due to PI B1 B2 in T and NI B2 B3 (or B3 B2) in cln(T ). Then, by the fact that τ does not propositionally satisfy α, {B1, B3} τ. Also, as τ satisfies B1 B2 in T , B2 τ. Hence, τ violates NI B2 B3 (B3 B2). (2) Suppose α is R1 B, added due to PI R1 R2 in T and NI R2 B (or B R2) in cln(T ). Then, by the fact that τ does not propositionally satisfy α, { R1, B} τ. Also, by condition 3 in Definition 3, R2 τ. Hence, τ violates NI R2 B (B R2). (3) Suppose α is R 1 B, added due to PI R1 R2 in T and NI R 2 B (or B R 2 ) in cln(T ). Then, by the fact that τ does not propositionally satisfy α, { R 1 , B} τ. Also, by condition 3 in Definition 3, R 2 τ. Hence, τ violates NI R 2 B (B R 2 ). (4) Suppose α is R1 R3, added due to PI R1 R2 in T and NI R2 R3 (or R3 R2) in cln(T ). Then, by the fact that τ does not propositionally satisfy α, {R1, R3} τ. Also, as τ satisfies R1 R2 in T , R2 τ. Hence, τ violates NI R2 R3 (R3 R2). (5) Suppose α is R R, added due to NI R R (or R R) in cln(T ). Then, by the fact that τ does not propositionally satisfy α, R τ. As R R |= R (R R |= R ), by condition 2 in Definition 3, τ violates NI R R (R R). (6) Suppose α is R R, added due to NI R R (or R R ) in cln(T ). Then, by the fact that τ does not propositionally satisfy α, R τ. Also, by condition 4 in Definition 3, R τ. As R R |= R ( R R |= R ), by condition 2 in Definition 3, τ violates NI R R ( R R ). Proof for Proposition 6 We construct an interpretation Iτ from τ using chase: Let d, e be two distinct constants, NC and N C be the set of concept names in B and B , respectively, and Aτ ={A(d) | A NC τ} {A(e) | A N C τ} {R(d, e) | R R τ} {R(d, fd,R) | R B τ, R τ, fd,R is a fresh constant} {R(e, fe,R) | ( R) B τ, R τ, fe,R is a fresh constant}. Take Iτ = chase T (Aτ). We want to show that Iτ is a model of T and τ(Iτ, d, e) = τ. To show the former, by Lemma 1, we only need to show that Aτ is a model of cln(T ). Towards a contradiction, suppose it is not the case, then there is an axiom B D or R S in cln(T ) that is violated by Aτ. (1) Suppose Aτ violates B D, this is the case when Aτ |= B(s) and Aτ |= D(s) for some constant s in Aτ. There are essentially four cases: DL-Lite Contraction and Revision (i) Suppose B and D are both concept names, then Aτ |= B(s) and Aτ |= D(s) only if s = d or s = e, B(s) Aτ, and D(s) Aτ. If s = d then from the construction of Aτ, {B, D} τ and thus τ does not propositionally satisfy B D; otherwise if s = e then {B , D } τ and τ does not propositionally satisfy B D . Both cases violate Lemma 5. (ii) Suppose B = R for some R and D is a concept name, then Aτ |= B(s) only if s = d or s = e, and R(s, t) Aτ for some t. Aτ |= D(s) only if D(s) Aτ. Suppose without loss of generality that s = d (similar as in (i), the case where s = e can be shown in the same way). If t = e then from the construction of Aτ, R τ, and by condition 4 in Definition 3, R τ; otherwise, t is a fresh constant, and R τ. In both cases, {B, R} τ and thus τ does not propositionally satisfy B R, which again violates Lemma 5. (iii) Suppose B = R for some R and D = S for some S such that R = S, then Aτ |= B(s) and Aτ |= D(s) only if R(s, t) Aτ and S(s, u) Aτ for some t, u. This is only when (a) s = d or s = e, and t, u are fresh constants; or (b) s = d and t = u = e; or (c) s = e and t = u = d. In case (a), suppose w.o.l.g s = d, then { R, S} τ and τ does not propositionally satisfy R S, which violates Lemma 5. In case (b), {R, S} τ, and by condition 4 in Definition 3, { R, S} τ, which again violates Lemma 5. In case (c), {R , S } τ. By condition 4 in Definition 3, {( R) , ( S) } τ, and hence τ does not propositionally satisfy ( R) ( S) . It again violates Lemma 5. (iv) Suppose B = R for some R and D = R, then Aτ |= B(s) only if R(s, t) Aτ for some t. This is only when (a) s = d or s = e, and t is a fresh constant; or (b) t = d or t = e, and s is a fresh constant; or (c) s = d and t = e; or (d) s = e and t = d. In case (a), suppose w.l.o.g. s = d, then R τ. In case (c), R τ, and by condition 4 in Definition 3, R τ. In both cases, τ does not propositionally satisfy R R, which violates Lemma 5. In case (b), suppose w.l.o.g. t = d, then R τ. In case (d), R τ, and by condition 4 in Definition 3, R τ. Since T |= R , it violates condition 2 in Definition 3. (2) Suppose Aτ violates R S, this is the case when Aτ |= R(s, t) and Aτ |= S(s, t) for some constants s, t in Aτ. This is the case only if (a) s = d and t = e, (b) s = e and t = d, (c) R = S and s = d or s = e with t a fresh constant, or (d) R = S and t = d or t = e with s a fresh constant. In case (a), {R, S} τ, and τ does not propositionally satisfy R S. In case (b), {R , S } τ, and by condition 5 in Definition 3, {R , S } τ. Hence, τ does not propositionally satisfy R S . In neither case, τ cln(T ) t r and it violates Lemma 5. In case (c), T |= R R, that is, T |= R . If s = d then R τ, and otherwise if s = e then ( R) τ, it violates condition 2 in Definition 3. Similarly, in case (d), T |= R . If t = d then R τ, and otherwise if t = e then ( R ) τ, it again violates condition 2 in Definition 3. We have shown that Aτ is a model of cln(T ), thus Iτ is a model of T . Now it remains to show that τ(Iτ, d, e) = τ. Since it is clear that τ(Aτ, d, e) = τ, from the definition of chase, τ(Aτ, d, e) τ(Iτ, d, e). We only need to show that τ(Iτ, d, e) τ(Aτ, d, e). This is equivalent to show that Iτ \ Aτ does not contain any assertion of the form A(d), A(e), R(d, e), R(d, s) or R(e, s) with s being a fresh constant such that no assertion R(d, t) Aτ or respectively R(e, t) Aτ (as otherwise, A, A , R, R, ( R) , respectively, will be in τ(Iτ, d, e) \ τ(Aτ, d, e) according to the definition of τ(Iτ, d, e)). Towards a contradiction, suppose there is such an assertion in Iτ \ Aτ. From the chase rules, it can happen only if some chase rule is applicable to an assertion g of the form B(d), Zhuang, Wang, Wang, & Qi B(e), S(d, e), S(d, t) or S(e, t) with t being a fresh constant in the chase. Let g be the first of such assertions that triggers a chase rule, then by the chase rules, g must be in Aτ. Suppose g = B(d), then from the construction of Aτ, B τ. If g triggers a chase rule with B A T , then by condition 1 in Definition 3, τ propositionally satisfies B A, and hence A τ and A(d) Aτ, which is a contradiction to (the applicability of) the chase rule; otherwise, g triggers a chase rule with B R T , then by condition 1 in Definition 3, τ propositionally satisfies B R, and thus R τ and R(d, u) Aτ for some u, which is again contradicts the chase rule. The case of g = B(e) is shown similarly, by replacing τ propositionally satisfying B A with τ propositionally satisfying B A , and τ propositionally satisfying B R with τ propositionally satisfying B ( R) . Suppose g = S(d, e), then from the construction of Aτ, S τ. From conditions 4 and 5 in Definition 3, S τ, ( S ) τ, and (S ) τ. If g triggers a chase rule with S R T , then by condition 1 in Definition 3, τ propositionally satisfies S R, R τ and R(d, e) Aτ, which contradicts the chase rule. If g triggers a chase rule with S R T , then by condition 1 in Definition 3, τ propositionally satisfies (S ) R , and R τ. By condition 5 in Definition 3, R τ and R (d, e) Aτ, which contradicts the chase rule. If g triggers a chase rule with S A, then τ propositionally satisfies S A. As S τ, A τ and A(d) Aτ, which contradicts the chase rule. If g triggers a chase rule with S A, then τ propositionally satisfies ( S ) A . As ( S ) τ, A τ and A(e) Aτ, which contradicts the chase rule. If g triggers a chase rule with S R, then τ propositionally satisfies S R. As S τ, R τ. Hence, R(d, u) Aτ for some u, which again is a contradiction. Similarly we can show the case of g triggering a chase rule with S R. Suppose g = S(d, t) with t being a fresh constant, then from the construction of Aτ, S τ. If g triggers a chase rule with S R T , then R(d, t) is added. By condition 3 in Definition 3, R τ, and again by the construction of Aτ, R(d, u) Aτ for some u. From the chase rules, R(d, t) behaves not differently from R(d, u) in the chase. Thus, we could equally consider g = R(d, u) for our discussion. That is, the application of the chase rule with S R T has no effect to the proof. If g triggering a chase rule with S A, then by condition 1 in Definition 3, τ propositionally satisfies S A. As S τ, A τ and A(d) Aτ, which contradicts to the chase rule. If g triggering a chase rule with S R, then τ propositionally satisfies S R, and thus R τ and R(d, u) Aτ for some u, which is again a contradiction. The case of g = S(e, t) can be shown in a similarly way. DL-Lite Contraction and Revision We have shown that Iτ \ Aτ does not contain any assertion of the form A(d), A(e), R(d, e), R(e, d), R(d, s) or R(e, s). Thus, τ(Iτ, d, e) = τ(Aτ, d, e) = τ. Proof for Theorem 5 If |T | = then there is a model I |T |. Let d, e I and τ = τ(I, d, e). By Proposition 5, τ |T |t r. That is, |T |t r = . Conversely, suppose |T |t r = , let τ |T |t r. By Proposition 6, there is a model I of T . That is, |T | = . If both |T | and |T |t r are empty, the statement trivially holds. In what follows, we assume both |T | and |T |t r are non-empty. For the if direction, we want to show that if T |= φ then |T |t r |φ|t r. Then, there is a model I of T such that I does not satisfy φ. Similar as in the proof of Theorem 1, we can assume w.l.o.g. that φ contains a single TBox axiom. If the axiom is of the form B C. Then, there is an domain element d I such that d BI and d CI. Let τ = τ(I, d, d). Since I is a model of T , from Proposition 5, τ |T |t r. If C is a basic concept, then B τ implies d BI and d CI, which in turn implies C τ. If C = D is a negated basic concept, then with a similar argument, B τ implies D τ. That is, τ does not propositionally satisfy B C. By condition 1 of Definition 3, τ |φ|t r. Suppose φ is of the form R E. Then, there are domain elements d, e I such that (d, e) RI and (d, e) EI. Let τ = τ(I, d, e). Again, from Proposition 5, τ |T |t r. If E is a role, then R τ implies (d, e) RI and (d, e) EI, which in turn implies E τ. If E = S is a negated role, then with a similar argument, R τ implies S τ. That is, τ does not propositionally satisfy R E. By condition 1 of Definition 3, τ |φ|t r. We have shown that in both cases |T |t r |φ|t r. For the only if direction, we want to show that if |T |t r |φ|t r then T |= φ. Since |T |t r |φ|t r, there is a t-type τ |T |t r such that τ |φ|t r. From Proposition 6, there exist a model I of T and domain elements d, e I such that τ(I, d, e) = τ. We only need to show that I is not a model of φ. Suppose otherwise, I is a model of φ, then by Proposition 5, τ must be a t-model of φ, which contradicts to the fact τ |φ|t r. Hence, I is not a model of φ, and we have shown that T |= φ. Before presenting the proof for Theorem 6, we first show Lemma 6 and Lemma 7. The two lemmas extend Lemma 3 and Lemma 4 respectively to DL-Lite R. Lemma 6 For two DL-Lite R TBox T1 and T2, and a role-complete set M of t-types with M |T1|t r |T2|t r, it holds that M cln(T1 T2) t r. Proof : Towards a contradiction, suppose there exists a t-type τ M and an NI α in cln(T1 T2) such that τ does not propositionally satisfy α. We show that some t-type in M exists that violates some NI in T 1 T 2 , which contradicts to the fact that M |T1|t r |T2|t r. Similar as the proof of Lemma 5, we prove this through induction. Here we only present the case where α is a NI in cln(T1 T2), and the case of α being a copy of some NI in cln(T1 T2), i.e., α cln(T1 T2) \ cln(T1 T2), can be shown similarly. Without loss of generality, we assume axioms are added to cln(T1 T2) incrementally according to the definition and copies (e.g., B C ) are added immediately after the original axioms (B B) are added. For initialization, if α is in T 1 T 2 then τ violates some NI in T 1 T 2 . For induction steps, we show that if α is added to cln(T1 T2) due to another axiom β already in Zhuang, Wang, Wang, & Qi cln(T1 T2) , we show that some τ M exists that violates β. The proof for cases (1) (4) are the same as the proof of Lemma 5, where we simply let τ = τ. For cases (5), suppose α is R R, added due to NI R R (or R R) in cln(T1 T2) . Note that ( R ) ( R ) (resp., R R ) is also in cln(T1 T2) . Then, by the fact that τ does not propositionally satisfy α, R τ. As M is role balance, there exists τ M with R τ or R τ . If R τ , by conditions 4 and 5 in Definition 3, ( R ) τ , and τ violates NI ( R ) ( R ) (resp., R R). If R τ , by conditions 4 and 5 in Definition 3, R τ and R τ , and again τ violates NI R R (resp., R R ). For case (6), suppose α is R R, added due to NI R R (or R R ) in cln(T1 T2) . Note that ( R) ( R) (resp., ( R ) ( R ) ) is also in cln(T1 T2) . Then, by the fact that τ does not propositionally satisfy α, R τ. By conditions 4 and 5 in Definition 3, R τ and ( R ) τ. Hence, τ violates NI R R (resp., ( R ) ( R ) ). Lemma 7 Let M be a set of t-types and φ1, φ2 be two conjunctions of DL-Lite R TBox axioms. Suppose M is role-complete, then M |φ1|t r |φ2|t r implies M |φ1 φ2|t r. Proof : For each τ M, we want to show that τ |φ1 φ2|t r. To this end, we construct a model of φ1 φ2 from τ in the same way as in the proof of Proposition 6. Let Ti be the set of axioms in φi for i = 1, 2, Aτ be constructed in the same way as in the proof of Proposition 6, and take Iτ = chase T1 T2(Aτ). We can show that Iτ is a model of T1 T2 and τ(Iτ, d, e) = τ in a similar way as in the proof of Proposition 6 (using Lemma 6 instead of Lemma 5), except for cases (1) (iv) and (2). In case (1) (iv), suppose Aτ violates R R in cln(T1 T2). Different from the proof of Proposition 6, we cannot assume R R in either cln(T1) or cln(T2), and thus cannot apply condition 2 in Definition 3. Yet we can still derive contradiction. Aτ violates R R only if R τ or R τ. In the former case, τ does not propositionally satisfy R R. That is, τ cln(T1 T2) t r, which violates Lemma 6. In the latter case, since M is role-complete, R τ for some t-type τ M. Hence, τ does not propositionally satisfy R R, which again violates Lemma 6. In case (2), suppose Aτ violates R S in cln(T1 T2). This is the case when {R, S} τ, {R , S } τ, or R = S and { R, R , ( R) , ( R ) } τ = . The first two cases can be shown in the same way as in the proof of Proposition 6. For the third case where R = S, different from the proof of Proposition 6, we cannot assume R R in either cln(T1) or cln(T2), and thus cannot apply condition 2 in Definition 3. Note that from the facts that { R, R , ( R) , ( R ) } τ = and that M is role-complete, there exists some t-type τ M with R τ or R τ . If R τ then τ does not propositionally satisfy R R; otherwise if R τ , τ does not propositionally satisfy R R . In both cases, Lemma 6 is violated. Now, we have shown that Iτ is a model of T1 T2 and τ(Iτ, d, e) = τ. By Proposition 5, τ |φ1 φ2|t r. Proof for Theorem 6 DL-Lite Contraction and Revision The theorem be proved similarly to Theorem 4, and the proof is based on Lemmas 6 and 7. Proof for Proposition 8 For each ct-type τ |T |t c, by Proposition 3, there is a model I of T and some d I such that τ(I, d) = τ. Let τ be the t-type such that τ = τ(I, d, d). Then, from the definitions of τ(I, d) and τ(I, d, d), τ = τ B. Also, by Proposition 5, τ |T |t r. That is, τ {τ B | τ |T |t r}, and hence |T |t c {τ B | τ |T |t r}. Conversely, for each ct-type τ {τ B | τ |T |t r}, there is a t-type τ |T |t r such that τ = τ B. By Proposition 6, there is a model I of T and some d, e I such that τ(I, d, e) = τ . It is easy to see that τ = τ(I, d) from the definitions of τ(I, d) and τ(I, d, e). By Proposition 2, τ |T |t c. That is, {τ B | τ |T |t r} |T |t c. The following theorem generalises Theorem 2 to DL-Lite R. Theorem 14 Let T be a DL-Lite R TBox such that T = {φ1, . . . , φn}. If T is coherent then |T |t r = |φ1|t r |φn|t r. Proof : For each τ |T |t r, τ satisfies conditions 4 and 5 in Definition 3. Also, for i = 1, . . . , n, by condition 1 in Definition 3 w.r.t. T , τ propositionally satisfies φi. That is, τ satisfies condition 1 w.r.t. φi. Further, as T is coherent, by the monotonicity of DL-Lite, there exists no R R such that φi |= R , and τ trivially satisfies condition 2 w.r.t. φi. Moreover, if φi |= R S, then T |= R S, and by condition 3 in Definition 3 w.r.t. T , τ satisfies condition 3 w.r.t. φi. Hence, τ |φi|t r for i = 1, . . . , n. That is, |T |t r |φ1|t r |φn|t r. Conversely, for each τ |φ1|t r |φn|t r, we can construct a model I of T from τ in the same way as in the proofs of Proposition 6 and Lemma 7 such that I induces τ. By Proposition 5, τ |T |t r. That is, |φ1|t r |φn|t r |T |t r. Proof for Proposition 9 For the if direction, since I is a model of T , it suffices to show that I is a model of A, i.e., for each concept assertion A(a) A, a I AI, and for each role assertion P(a, b) A, (a I, b I) P I. Let τ = τ a(I), then τ AT a r and τ propositionally satisfies Aa. That is, Aa τ. From the definition of τ, a I AI. Similarly, τ propositionally satisfies P ab and P ab τ, and hence (a I, b I) P I. We have shown I |K|. For the only if direction, we only need to show the second half of the statement since I |K| implies I |T |. Let τ = τ a(I), and we want to show that τ |AT |a r. For condition 1 of Definition 4, we can show τ satisfies T a in the same way as in the proof of Proposition 5. For each A(a) A and each P(a, b) A, since a I AI and (a I, b I) P I, Aa τ and P ab τ. That is, τ propositionally satisfies A. We haven shown that τ AT a r. Further, it can be shown that τ satisfies conditions 2 5 of Definition 4 in a similar manner as in the proof of Proposition 5 (roughly, by replacing Definition 3 with Definition 4, d with each a D, e with each b D, B with Ba, B with Bb, R with Rab, R with ( R)a, ( R) with ( R)b, and so on). Before presenting the proof for Proposition 10, we first show Lemma 8. The lemma can be proved in the same manner as Lemma 5. Note that cln(T )a is the TBox that consists Zhuang, Wang, Wang, & Qi of a copy of each concept inclusion in cln(T ) for each individual in D, and a copy of each role inclusion in cln(T ) for each pair of individuals in D. Lemma 8 For a DL-Lite R KB K = (T , A), each a-model τ of AT is a propositional model of cln(T )a. Proof for Proposition 10 Similar as before, we construct an interpretation Iτ from τ using chase: Let Na C be the set of concept names in Ba (with a D), and Aa τ ={A(a) | a D, Aa Na C τ} {R(a, b) | a, b D, Rab Rab τ} {R(a, fa,R) | a D, ( R)a Ba τ, Rab τ for any b D, fa,R is a fresh constant}. Take Iτ = chase T (Aa τ). We want to show that Iτ is a model of K and τ a(Iτ) = τ. To show the former, we first show that A Aa τ. For each concept assertion A(a) A, as τ is an a-model of K, τ propositionally satisfies Aa. That is, Aa τ and hence A(a) Aa τ. Similarly, for each role assertion P(a, b) A, P ab τ and P(a, b) Aa τ. We have shown that A Aa τ. To show that Iτ is a model of K, we want to show that Iτ is a model of (T , Aa τ). By Lemma 1, we only need to show that Aa τ is a model of cln(T ). This can be shown in a similar way as in the proof of Proposition 6 (roughly, by replacing Definition 3 with Definition 4, Lemma 5 with Lemma 8, d with each a D, e with each b D, B with Ba, B with Bb, R with Rab, R with ( R)a, ( R) with ( R)b, and so on). Now it remains to show that τ a(Iτ) = τ. Again, we only need to show that τ a(Iτ) τ a(Aa τ). This again can be shown in a similar way as the proof of Proposition 6. Proof for Theorem 7 If |K| = then there is a model I |K|. Let τ = τ a(I). By Proposition 9, τ |AT |a r. That is, |AT |a r = . Conversely, suppose |AT |a r = , let τ |AT |a r. By Proposition 10, there is a model I of K. That is, |K| = . If both |K| and |AT |a r are empty, the statement trivially holds. In what follows, we assume both |K| and |AT |a r are non-empty. For the if direction, we want to show that if K |= φ then |AT |a r |φ|a r. Then, there is a model I of K such that I does not satisfy φ. Let τ = τ a(I). From Proposition 9, τ |AT |a r. Similar as in the proof of Theorem 1, we can assume w.l.o.g. that φ contains a single ABox assertion. Suppose φ is of the form A(a). Then, a I AI. From the definition of τ a(I), Aa τ, and hence τ φ a r. By condition 1 of Definition 4, τ |φ|a r. Suppose φ is of the form P(a, b). Then, (a I, b I) P I. Again, from the definition of τ a(I), P ab τ, and hence τ |φ|a r. In both cases, |AT |a r |φ|a r. For the only if direction, we want to show that if |AT |a r |φ|a r then K |= φ. Since |AT |a r |φ|a r, there is an a-type τ |AT |a r such that τ |φ|a r. From Proposition 10, there exist a model I of K such that τ a(I) = τ. We only need to show that I is not a model of φ. Suppose otherwise, I is a model of φ, then by Proposition 9, τ must be an a-model of φ, which contradicts to the fact τ |φ|a r. Hence, I is not a model of φ, and we have shown that K |= φ. Proof for Theorem 8 Let A = {A(a) | Aa τ for each τ M} {P(a, b) | P ab τ for each τ M}. We want to show that A is the unique corresponding ABox for M w.r.t. T . DL-Lite Contraction and Revision We first show that A is a corresponding ABox. To show that M |AT |a r, we need to show for each a-type τ M, τ satisfies conditions 1 5 in Definition 4. As M is consistent with T , τ | T |a r. Hence, τ is a propositional model of T a, and τ satisfies conditions 2 5. Also, from the construction of A, τ satisfies Aa for each A(a) A and satisfies P ab for each P(a, b) A. That is, τ AT a r. We have shown that M |AT |a r. Further, for any ABox A such that M |A T |a r and for each a-type τ M, since τ A T a r, τ satisfies Aa for each concept assertion A(a) A and satisfies P ab for each role assertion P(a, b) A . Note that this holds for each a-type in M. From the construction of A, A A. That is, |AT |a r |A T |a r. Thus, A is a corresponding ABox. Also, based on the above observation, any corresponding ABox must be equivalent to A. The following theorem can be proved similar to Theorem 14. Since only one TBox is concerned, the proof does not require Lemmas 6 and 7. Theorem 15 Let K = (T , A) be a DL-Lite R KB such that A = {φ1, . . . , φn}. Then |AT |a r = |{φ1}T |a r |{φn}T |a r. Proof for Proposition 12 Let K = (T , A). For the if direction, it suffices to show that (i) for each d I and each concept inclusion B C in T , d BI implies d CI; (ii) for each e I (not necessarily d = e) and each role inclusion R E in T , (d, e) RI implies (d, e) EI; (iii) for each concept assertion A(a) A, a I AI, and for each role assertion P(a, b) A, (a I, b I) P I. Let τ = τ (I, d, e) = τ(I, d, e) τ a(I). Conditions (i) and (ii) are shown in the proof of Proposition 5. That is, I |T |. Then, condition (iii) is shown in the proof of Proposition 9. For the only if direction, let τ = τ (I, d, e) for some arbitrary d, e I. That is, τ = τ(I, d, e) τ a(I). We want to show that τ(I, d, e) |T |t r and τ a(I) |AT |a r, which have been shown in the proofs of Propositions 5 and 9, respectively. Proof for Proposition 13 Let K = (T , A). We construct an interpretation Iτ from τ using chase: Let Aτ and Aa τ be defined as in the proofs of Propositions 6 and 10, and Iτ = chase T (Aτ Aa τ). We want to show that Iτ is a model of K and τ (Iτ, d, e) = τ. To show the former, we have A Aa τ from the proof of Proposition 10, and we only need to show that Iτ is a model of (T , Aτ Aa τ). By Lemma 1, it suffices to show that Aτ Aa τ is a model of cln(T ), which has been shown in the proofs of Propositions 6 and 10. To show later, that is τ (Iτ, d, e) = τ, we only need to show that τ (Iτ, d, e) τ (Aτ, d, e). By the definition of τ (Iτ, d, e), it suffices to show that τ(Iτ, d, e) τ(Aτ, d, e) and τ a(Iτ) τ a(Aa τ), which again has been shown in the proofs of Propositions 6 and 10. Proof for Theorem 9 It can be shown in the same way as in the proof for Theorem 7 that |K| is empty if and only if |K|r is empty. In what follows, we assume both |K| and |K|r are both non-empty. For the if direction, we want to show that if K |= φ then |K|r |φ|r. Then, there is a model I of K such that I does not satisfy φ. Similar as in the proof of Theorem 1, we can assume w.l.o.g. that φ contains a single TBox axiom or a single ABox assertion. Suppose Zhuang, Wang, Wang, & Qi φ is of the form B C or R E, then in the same way as the proof of Theorem 5, we can construct τ = τ (I, d, e) for some d, e I such that τ |K|r and τ |φ|r. Suppose φ is of the form A(a) or P(a, b), then in the same way as the proof of Theorem 7, we can show that τ |K|r and τ |φ|r. The only if direction can be shown in the same way as in the proof for Theorem 7. Before presenting the proof for Theorem 10, we first show Lemma 9 and Lemma 10. The two extend Lemmas 6 and 7 respectively to DL-Lite R KBs. Lemma 9 For two DL-Lite R TBox T1 and T2, and a role-complete set M of types with M |T1|r |T2|r, all the types in M must satisfy cln(T1 T2) cln(T1 T2)a. Proof : Towards a contradiction, suppose there exists a type τ M and an NI α in cln(T1 T2) cln(T1 T2)a such that τ does not propositionally satisfy α. We show that some type in M exists that violates some NI in T 1 T 2 T a 1 T a 2 , which contradicts to the fact that M |T1|r |T2|r. It can be shown in a similar way as the proof of Lemma 6. When an axiom in cln(T1 T2) is concerned, the proof is as that of Lemma 6. When an axiom in cln(T1 T2)a is concerned, the proof is adapted by replacing B with Ba, B with Bb, R with Rab, R with ( R)a, ( R) with ( R)b, and so on. Lemma 10 Let M be a set of types and φ1, φ2 be two conjunctions of DL-Lite R axioms. Suppose M is role-complete, then M |φ1|r |φ2|r implies M |φ1 φ2|r. Proof : For each type τ M, we want to show that τ |φ1 φ2|r. To this end, we construct a model of φ1 φ2 from τ in the same way as in the proof of Proposition 13. Let T and A be the sets of respectively TBox axioms and ABox axioms in both φ1 and φ2, be the set of ABox axioms in Aτ and Aa τ be as in the proof of Proposition 13, and take Iτ = chase T (A Aτ Aa τ). We can show that Iτ is a model of (T , A) and τ (Iτ, d, e) = τ in a similar way as in the proofs of Lemma 7 and Proposition 13. By Proposition 12, τ |φ1 φ2|r. Proof for Theorem 10 The theorem can be proved similarly to Theorem 4 and the proof is based on Lemma 9 and Lemma 10. The following theorem can be proved similar to Theorem 14. Theorem 16 Let K be a DL-Lite R KB such that K = {φ1, . . . , φn}. If K is coherent then |K|r = |φ1|r |φn|r. Proof for Theorem 11 For one direction, suppose . is a T-contraction function for a TBox T and the associated selection function is γ. We need to show . satisfies (T . 1) (T . 4), (T . de), and (T . 6). (T . 1), (T . 2), (T . 4) and (T . 6) follow directly from the definition of T-contraction function. We only show the proof for (T . 3) and (T . de). DL-Lite Contraction and Revision (T . 3): Suppose T |= φ. Then |T |t r |φ|t r which implies |T |t r | φ|t r = . Thus by the faithfulness of γ, we have γ(| φ|t r) |T |t r. Thus T . φ = Tr(|T |t r γ(| φ|t r)) = Tr(|T |t r) = T . (T . de): We prove its contrapositive. Suppose T |= ψ and T . φ |= ψ. Then we have |T |t r |ψ|t r and |T . φ|t r |ψ|t r. It remains to show |T . φ|t r |φ|t r |ψ|t r. Assume |T . φ|t r |φ|t r |ψ|t r. Since by the definition of T-contraction function, |T |t r γ(| φ|t r) |T . φ|t r, we have |T |t r γ(| φ|t r) |φ|t r |ψ|t r which implies for each µ γ(| φ|t r), µ |ψ|. Thus |T |t r γ(| φ|t r)) |ψ|t r. It then follows from the definition of corresponding TBoxes that |T |t r γ(| φ|t r)) |T . φ|t r |ψ|t r, a contradiction! For the other direction, suppose . is a function for a TBox T that satisfies (T . 1) (T . 4), (T . de), and (T . 6). Let γ be defined as γ(| φ|t r) = | φ|t r |T . φ|t r for all conjunctions of TBox axioms φ. For a set of t-types M, if there is no conjunction of TBox axiom φ such that | φ|t r = M, then define γ(M) = M |T |t r whenever M |T |t r = and M otherwise. We need to show that (1) γ is a faithful selection function for T and (2) T . φ = Tr(|T |t r γ(| φ|t r)). Part (1): For γ to be a faithful selection function, it has to be a function first. And this follows directly from the definition of γ and (T . 6). To prove γ is a selection function, suppose M = . We need to show γ(M) = . If a TBox axiom φ is a tautology, then we have | φ|t r = = M. Thus γ(M) = γ(| φ|t r) = | φ|t r |T . φ|t r = . Now suppose M = . We need to show γ(M) = . By the definition of γ, the result trivially holds if there is no conjunction of TBox axioms φ such that | φ|t r = M. If there is φ such that | φ|t r = M, then since | φ|t r = implies |= φ, it follows from (T . 4) that |T . φ|t r | φ|t r = . Thus γ(M) = γ(| φ|t r) = | φ|t r |T . φ|t r = . To prove γ is faithful with respect to T , suppose M |T |t r = . We need to show γ(M) = M |T |t r. Again, the result trivially holds if there is no conjunction of TBox axioms φ such that | φ|t r = M. If there is φ such that | φ|t r = M, then since | φ|t r |T |t r = implies T |= φ, it follows from (T . 3) that |T . φ|t r = |T |t r. Thus γ(M) = γ(| φ|t r) = | φ|t r |T . φ|t r = | φ|t r |T |t r. Part (2): Since (T . 1) implies T . φ is closed and Tr is a function that returns closed TBoxes, it suffices to show |Tr(|T |t r γ(| φ|t r))|t r = |T . φ|t r. It follows from (T . 2) that T . φ T which implies |T |t r |T . φ|t r. It follows from the definition of γ that γ(| φ|t r) |T . φ|t r. So we have |T |t r γ(| φ|t r) |T . φ|t r which implies by the definition of corresponding TBoxes that |Tr(|T |t r γ(| φ|t r))|t r |T . φ|t r. It remains to show |T . φ|t r |Tr(|T |t r γ(| φ|t r))|t r. Assume to the contrary that |T . φ|t r |Tr(|T |t r γ(| φ|t r))|t r. Let ψ be a conjunction of TBox axioms such that |ψ|t r = |Tr(|T |t r γ(| φ|t r))|t r. Then T |= ψ and T . φ |= ψ. It follows from (T . de) that |T . φ|t r |φ|t r |ψ|t r = |φ|t r |Tr(|T |t r γ(| φ|t r))|t r. Let u |T . φ|t r, if u |φ|t r then u |φ|t r |Tr(|T |t r γ(| φ|t r))|t r and if u | φ|t r, then by the definition of γ, u γ(| φ|t r). Thus in either case, u |φ|t r |Tr(|T |t r γ(| φ|t r))|t r which implies |T . φ|t r |φ|t r |Tr(|T |t r γ(| φ|t r))|t r = |φ|t r |ψ|t r, a contradiction! Proof for Proposition 15 The complexity results have been explained earlier. Let . be a function such that T . φ = TCONT(T , φ) for any TBox T and conjunction of axioms φ. We need to show . Zhuang, Wang, Wang, & Qi is a T-contraction function. By Theorem 11 it suffices to show . satisfies (T . 1) (T . 4), (T . de), and (T . 6). (T . 2), (T . 3) and (T . 6) are trivially satisfied. Let τ be the counter-model picked in line 3 of TCONT. Since all axioms of T that violet τ are removed in line 6, we have τ |δ|t r for all δ T . φ. Suppose T . φ = {δ1, . . . , δn}. Then by Theorem 14, we have |δ1|t r |δn|t r = |T . φ|t r which implies τ |T . φ|t r. Then it is obvious that T . φ |= φ, so (T . 4) is satisfied. For (T . 1), suppose ψ T and T . φ |= ψ. We need to show ψ T . φ. Since T . φ |= ψ implies |T . φ|t r |ψ|t r and τ |T . φ|t r, we have τ |ψ|t r that is τ |=t r ψ. Thus ψ is not removed in line 6 which means ψ T . φ. For (T . de), suppose ψ T and |T . φ|t r |φ|t r |ψ|t r. Then it follows from τ |φ|t r and τ |T . φ|t r that τ |ψ|t r. Thus ψ is not removed in line 6 of TCONT which means ψ T . φ. Proof for Theorem 12 For one direction, suppose is a T-revision function for a TBox T and the associated selection function is γ. We need to show satisfies (T 1) (T 6) and (T f). (T 1), (T 2), (T 6), and (T f) follow immediately from the definition of T-revision. We only show the proof for (T 3) (T 5). (T 3): Suppose φ is coherent. It follows from the definition of T-revision function that γ(|φ|t r) |T φ|t r. Since γ is faithful with respect to T , we have |T |t r |φ|t r γ(|φ|t r). Thus |T |t r |φ|t r |T φ|t r which implies T φ cl(T {φ}). (T 4): Suppose T {φ} is coherent. Then |T |t r |φ|t r is coherent. It follows from the faithfulness of γ that γ(|φ|t r) = |T |t r |φ|t r. By the definition of T-revision function, we have γ(|φ|t r) |T φ|t r. So we have |T |t r |φ|t r |T φ|t r which implies T φ = cl(T {φ}). (T 5): Suppose φ is coherent. Since γ is coherent preserving, γ(|φ|t r) is coherent. By the definition of T-revision function, we have γ(|φ|t r) |T φ|t r. Thus |T φ|t r is also coherent which implies T φ is coherent. For the other direction, suppose is a function for a TBox T that satisfies (T 1) (T 6) and (T f). Let γ be defined as γ(|φ|t r) = |T φ|t r for all conjunctions of TBox axioms φ. For a set of t-types M, if there is no conjunction of TBox axioms φ such that |φ|t r = M, then define γ(M) = if M is incoherent; γ(M) = M |T |t r if M |T |t r is coherent; and γ(M) = M if M is coherent and M |T |t r is incoherent. We need to show that (1) γ is a faithful and coherent preserving selection function for T and (2) T φ = Tr(γ(|φ|t r)). Part (1): For γ to be a faithful and coherent preserving selection function, it has to be a function first. And this follows directly from the definition of γ and (T 6). Let M be a set of t-types. Suppose M is coherent. We need to show γ(M) = . By the definition of γ, the result trivially holds if there is no conjunction of TBox axioms φ such that |φ|t r = M. If there is φ such that |φ|t r = M, then we have by (T 5) that |T φ|t r is coherent. So we have γ(|φ|t r) = |T φ|t r = . Suppose M is incoherent. We need to show γ(M) = . By the definition of γ, the result trivially holds if there is no conjunction of TBox axioms φ such that |φ|t r = M. If there is φ such that |φ|t r = M, then it follows from (T f) that |T φ|t r = . Thus γ(|φ|t r) = |T φ|t r = . DL-Lite Contraction and Revision For faithfulness, suppose M is coherent. We need to show |T φ|t r M γ(M). By the definition of γ, the result trivially holds if there is no conjunction of TBox axioms φ such that |φ|t r = M. If there is φ such that |φ|t r = M, then it follows from (T 3) that T φ cl(T {φ}) which implies |T φ|t r |φ|t r |T φ|t r. Since γ(|φ|t r) = |T φ|t r, we have |T φ|t r |φ|t r γ(|φ|t r). Now suppose |T φ|t r M is coherent. We need to show γ(M) = |T φ|t r M. Again the result trivially holds if there is no conjunction of TBox axioms φ such that |φ|t r = M. If there is φ such that |φ|t r = M, then it follows from (T 3) and (T 4) that T φ = cl(T {φ}) which implies |T φ|t r |φ|t r = |T φ|t r. Since γ(|φ|t r) = |T φ|t r, we have |T φ|t r |φ|t r = γ(|φ|t r). For coherent preserving, suppose M is coherent. We need to show γ(M) is coherent. Again the result trivially holds if there is no conjunction of TBox axioms φ such that |φ|t r = M. If there is φ such that |φ|t r = M, then it follows from (T 5) that T φ is coherent which implies |T φ|t r is coherent. Since γ(|φ|t r) = |T φ|t r, γ(|φ|t r) is coherent. Part (2): By the definition of γ, we have γ(|φ|t r) = |T φ|t r. Since it follows from (T 1) that T φ is closed, we have by the definition of Tr that T φ = Tr(|T φ|t r) = Tr(γ(|φ|t r)). Proof for Proposition 16 The complexity results have been explained earlier. Let be a function such that T φ = TREVI (T , φ) for all TBox T and conjunction of TBox axioms φ. We need to show is a T-revision function. By Theorem 12, it suffices to show satisfies (T 1) (T 6) and (T f). (T 1), (T 2), (T 6), and (T f) are trivially satisfied. For (T 3), if T {φ} is inconsistent then cl(T {φ}) includes all axioms thus the postulates holds trivially. So suppose T {φ} is consistent. Then |T {φ}|t r = and |T {φ}|t r |T |t r. As no new axiom is added to T throughout TREVI , we have |T {φ}|t r |REV I(T , φ)|t r which implies TREVI (T , φ) cl(T {φ}). For (T 4), suppose T {φ} is coherent. Then the condition in line 4 is never fulfilled thus no axioms get removed which means TREVI (T , φ) = cl(T {φ}). Now we focus on (T 5). Given a t-type τ and an atomic concept or role F, by the definition of t-model if F τ then τ |=t r B . It is not hard to see that {τ1, . . . , τn} (|T |t r |φ|t r) |TREVI (T , φ)|t r for τi the t-models of φ picked at line 5 of TREVI . Due to line 4 8 of TREVI , if F is such that |T |t r |φ|t r |=t r F then there is τ {τ1, . . . , τn} such that F τ which means for any F we have {τ1, . . . , τn} (|T |t r |φ|t r) |=t r F which implies |TREVI (T , φ)|t r |=t r F . Thus TREVI (T , φ) is coherent. Proof for Theorem 13 For one direction, suppose is an A-revision function for AT and the associated selection function is γ. We need to show satisfies (A 1) (A 6), and (A f). (A 1), (A 2), (A 6), and (A f) follow immediately from the definition of A-revision function. We only show the proof for (A 3) (A 5). (A 3), (A 4): If |(A {φ})T |a r = , then the two postulates hold trivially. So suppose |(A {φ})T |a r = which implies |AT |a r |{φ}T |a r = . Since γ is faithful, we have |AT |a r |{φ}T |a r = γ(|{φ}T |a r). Then it follows from the definition of A-revision function that AT φ = AT r (γ(|{φ}T |a r)) = AT r (|AT |a r |{φ}T |a r) = cl(AT {φ}). (A 5): Suppose |{φ}T |a r = . Then by the definition of γ, γ(|{φ}T |a r) = . Since it follows from the definition of A-revision function that γ(|{φ}T |a r) |AT φ|a r, |AT φ|a r = . Zhuang, Wang, Wang, & Qi For the other direction, suppose is a function for an ABox AT that satisfies (A 1) (A 6), and (A f). Let γ be defined as γ(|{φ}T |a r) = |(AT φ)T |a r for all conjunctions of ABox axioms φ. For a set of a-types M, if there is no conjunction of ABox axioms φ such that |{φ}T |a r = M, then define γ(M) = M |AT |a r whenever M |AT |a r = and M otherwise. We need to show that (1) γ is a faithful selection function for AT and (2) AT φ = AT r (γ(|{φ}T |a r)). Part (1): For γ to be a faithful selection function, it has to be a function first. And this follows directly from the definition of γ and (A 6). Let M be a set of a-types. Suppose M = . We need to show γ(M) = . By the definition of γ, the result trivially holds if there is no conjunction of ABox axioms φ such that |{φ}T |a r = M. If there is φ such that |{φ}T |a r = M, then we have by (A 5) that |(AT φ)T |a r = . So we have γ(|{φ}T |a r) = |(AT φ)T |a r = . Suppose M = . We need to show γ(M) = . For any axiom φ that is inconsistent with T , we have |{φ}T |a r = . It follows from (A f) that in this case |(AT φ)T |a r = , thus γ(|{φ}T |a r) = |(AT φ)T |a r = . For faithfulness, suppose |AT |a r M = , we need to show γ(M) = M |AT |a r. The result holds trivially if there is no φ such that |{φ}T |a r = M. If there is φ such that |{φ}T |a r = M, then we have |AT |a r |{φ}T |a r = which implies |A {φ}T |a r = . So it follows from (A 3) and (A 4) that |cl T (A {φ}T )|a r = |AT φ|a r. Thus γ(|{φ}T |a r) = |(AT φ)T |a r = |cl(A {φ}T )|a r = |AT |a r |{φ}T |a r. Part (2): By the definition of γ, we have γ(|{φ}T |a r) = |(AT φ)T |a r. Since it follows from (A 1) that A φ is closed, we have by the definition of AT r that AT φ = AT r (|(AT φ)T |a r) = AT r (γ(|{φ}T |a r)). Proof for Proposition 17 The complexity results have been explained earlier. Let be a function such that AT φ = AREVI (AT , φ) for all ABox AT and conjunction of ABox axioms φ. We need to show is an A-revision function. By Theorem 13, it suffices to show satisfies (A 1) (A 6) and (A f). (A 1), (A 2), (A 6), and (A f) are trivially satisfied. For (A 3), suppose φ is inconsistent with T or is consistent with (T , A). Then line 2 and line 3 of AREVI (T , A, φ) guarantee that the postulate holds. So suppose φ is consistent with T but is inconsistent with (T , A). Since no new axiom is added to A in lines 6 8, in line 9 the returned ABox must be a subset of cl T (AT {φ}). For (A 4), suppose φ is consistent with (T , A). Then line 4 of AREVI (T , A, φ) guarantees that cl T (AT {φ}) = AT φ. For (A 5), suppose φ is consistent with T . Then if φ is consistent with (T , A), the ABox returned in line 4 must be consistent, and if φ is inconsistent with (T , A), lines 6 8 guarantee that all axioms in A that are inconsistent with φ is removed, thus the ABox returned in line 9 is also consistent. Alchourr on, C. E., G ardenfors, P., & Makinson, D. (1985). On the logic of theory change: Partial meet contraction and revision functions. The Journal of Symbolic Logic, 50(2), 510 530. DL-Lite Contraction and Revision Baader, F., Calvanese, D., Mc Guinness, D., Nardi, D., & Patel-Schneider, P. (Eds.). (2003). The Description Logic Handbook. CUP, Cambridge, UK. Calvanese, D., De Giacomo, G., Lembo, D., Lenzerini, M., & Rosati, R. (2007). Tractable reasoning and efficient query answering in description logics: The DL-Lite family. Journal of Automatic Reasoning, 39(3), 385 429. Calvanese, D., Kharlamov, E., Nutt, W., & Zheleznyakov, D. (2010). Evolution of DL-Lite knowledge bases. In Proceedings of the 9th International Semantic Web Conference (ISWC-2010), pp. 112 128. Dalal, M. (1988). Investigations into a theory of knowledge base revision. In Proceedings of the 7th National Conference on Artificial Intelligence (AAAI-1988), pp. 475 479. De Giacomo, G., Lenzerini, M., Poggi, A., & Rosati, R. (2009). On instance-level update and erasure in description logic ontologies. Journal of Logic Computation, 19(5), 745 770. Ferm e, E., Krevneris, M., & Reis, M. (2008). An axiomatic characterization of ensconcement-based contraction. Journal of Logic and Computation, 18(5), 739 753. Flouris, G., Huang, Z., Pan, J. Z., Plexousakis, D., & Wache, H. (2006). Inconsistencies, negations and changes in ontologies. In Proceedings of the 21st National Concference on Artificial Intelligence (AAAI-2006). G ardenfors, P. (1988). Knowledge in Flux: Modelling the Dynamics of Epistemic States. MIT Press. Grau, B. C., Ruiz, E. J., Kharlamov, E., & Zhelenyakov, D. (2012). Ontology evolution under semantic constraints. In Proceedings of the 13th International Conference on Principles of Knowledge Representation and Reasoning (KR-2012), pp. 137 147. Hansson, S. O. (1991). Belief Contraction Without Recovery. Studia Logica, 50(2), 251 260. Hansson, S. O. (1994). Kernel contraction. The Journal of Symbolic Logic, 59(3), 845 859. Hansson, S. O. (1997). Semi-revision. Journal of Applied Non-Classical Logics, 7(1-2), 151 175. Hansson, S. O. (1999). A Textbook of Belief Dynamics Theory Change and Database Updating. Kluwer. Hansson, S. O., & Wassermann, R. (2002). Local change. Studia Logica, 70(1), 49 76. Kalyanpur, A., Parsia, B., Sirin, E., & Cuenca-Grau, B. (2006). Repairing unsatisfiable concepts in OWL ontologies. In Proceedings of the 3rd European Semantic Web Conference (ESWC-2006), pp. 170 184. Katsuno, H., & Mendelzon, A. O. (1991). On the difference between updating a knowledge base and revising it. In Proceedings of the 2nd International Conference on Principles of Knowledge Representation and Reasoning (KR-1991), pp. 387 394. Katsuno, H., & Mendelzon, A. O. (1992). Propositional knowledge base revision and minimal change. Artificial Intelligence, 52(3), 263 294. Zhuang, Wang, Wang, & Qi Kharlamov, E., & Zheleznyakov, D. (2011). Capturing instance level ontology evolution for DL-Lite. In Proceedings of the 10th International Semantic Web Conference (ISWC2011), pp. 321 337. Kharlamov, E., Zheleznyakov, D., & Calvanese, D. (2013). Capturing model-based ontology evolution at the instance level: The case of DL-Lite. Journal of Computer and System Sciences, 79(6), 835 872. Kontchakov, R., Wolter, F., & Zakharyaschev, M. (2010). Logic-based ontology comparison and module extraction, with an application to DL-Lite. Artificial Intelligence, 174(15), 1093 1141. Lenzerini, M., & Savo, D. F. (2011). On the evolution of the instance level of DL-Lite knowledge bases. In Proceedings of the 24th International Workshop on Description Logics (DL-2011). Lenzerini, M., & Savo, D. F. (2012). Updating inconsistent description logic knowledge bases. In Proceedings of the 20th European Conference on Artificial Intelligence (ECAI-2012), pp. 516 521. Levi, I. (1991). The Fixation of Beliefs and its Udoing. Cambridge University Press. Pan, J. Z., & Thomas, E. (2007). Approximating OWL-DL ontologies. In Proceedings of the 22nd National Conference on Artificial Intelligence (AAAI-2007), pp. 1434 1439. Qi, G., & Du, J. (2009). Model-based revision operators for terminologies in description logics. In Proceedings of the 21st International Joint Conferences on Artificial Intelligence (IJCAI-2009), pp. 891 897. Qi, G., Haase, P., Huang, Z., Ji, Q., Pan, J. Z., & Volker, J. (2008). A kernel revision operator for terminologies algorithms and evaluation. In Proceedings of the 7th International Semantic Web Conference (ISWC-2008), pp. 419 434. Qi, G., Liu, W., & Bell, D. A. (2006). Knowledge base revision in description logics. In Proceedings of the 10th European Conference on Logics in Artificial Intelligence (JELIA-2006), pp. 386 398. Ribeiro, M. M., & Wassermann, R. (2009). Base revision for ontology debugging. Journal of Logic and Computation, 19(5), 721 743. Ribeiro, M. M., Wassermann, R., Flouris, G., & Antoniou, G. (2013). Minimal change: Relevance and recovery revisited. Artificial Intelligence, 201, 59 80. Satoh, K. (1988). Nonmonotonic reasoning by minimal belief revision. In Proceedings of the International Conference on Fifth Generation Computer Systems, pp. 455 462. Wang, Z., Wang, K., & Topor, R. W. (2015). DL-Lite ontology revision based on an alternative semantic characterization. ACM Transaction on Computational Logic, 16(4), 31:1 31:37. Winslett, M. (1990). Updating Logical Databases. Cambridge University Press. Zhuang, Z., Wang, Z., Wang, K., & Qi, G. (2014). Contraction and revision over DLLite TBoxes. In Proceedings of the 28th AAAI Conference on Atificial Intelligence (AAAI-2014), pp. 1149 1156.