Model-based Revision Operators for Terminologies in Description Logics

1 Introduction

scription logics (DLs) are a family of important ontology representation languages (see [Halaschek-Wiener et al., 2006; Qi et al., 2006; Flouris et al., 2006]). However, these operators are all syntax-dependent ones. That is, suppose there are two ontologies that are logically equivalent and we want to revise them with another ontology using these operators, then we may get two ontologies which are not logically equivalent. In belief revision, there is an important family of revision operators, called model-based revision operators, that are independent of the syntactical forms of the ontologies to be revised. Amodel-based revision operator in propositional logic is usually defined by the symmetric difference set between two interpretations which are a set of propositional variables. However, it is not trivial to adapt the model-based revision operators to DLs because DLs have their own features (see [Flouris et al., 2005]). For example, in DLs, we can distinguish two kinds of logical contradictions: inconsistency and incoherence. An ontology is inconsistent iff it has no model, i.e., it is inconsistent in the first-order sense. An ontology is incoherent iff there exists some unsatisfiable concept (i.e, an unsatisfiable concept stands for the empty set).

Next generation semantic applications are characterized by a large number of ontologies, some of them constantly evolving. When changing ontologies, we often confront the problem of dealing with inconsistencies [Haase and Stojanovic, 2005; Schlobach et al., 2007; Qi et al., 2008]. In [Qi et al., 2008], two scenarios have been considered where we need to deal with this problem. The first one is the ontology learning scenario where inconsistencies occur during the process of learning expressive ontologies from text corpus incrementally and the second one is the ontology mapping scenario where erroneous mappings may result in an inconsistency and need to be repaired. Inconsistencies hamper the effective use of ontologies because answers derived with standard-reasoning are completely meaningless. Therefore, inconsistency handling is an important problem for ontology change.

Inconsistency handling has been considered as a central problem in many topics of knowledge representation, such as belief revision [G¨ardenfors, 1988] which deals with the problem of accommodating newly received information consistently. The problem of revising an ontology consistently is closely related to the problem of belief revision. Many operators in belief revision have been adapted to deal with inconsistencies in description logic-based ontologies where de- In this paper, we propose three novel model-based revision operators to revise terminologies in DLs by adapting the wellknown Dalal revision operator defined in propositional logic. In Section 3, we first define a revision operator by directly adapting the notions of difference set between two interpretations and distance between two terminologies. However, this revision operator cannot deal with incoherence. To solve the problem, we propose a modified distance between two terminologies. The revision operator defined by this new distance function is still problematic because it does not differentiate satisfiable concepts and unsatisfiable concepts. Therefore, we define a modified difference set between two interpretations. We also consider the problem of computing the result of revision by this operator with the help of the notion of forgetting. In Section 4, we show that this revision operator is better than others by comparing their logical properties. Finally, we consider some computational issues of this revision operator.

2 Preliminaries on Description Logics

We introduce some basic notions of Description Logics (DLs) (more detailed of DLs can be found in [Baader et al., 2007]). In our work, we consider only terminological part of a DLbased ontology, i.e., the so-called TBox (or terminology)

which is used to express the intensional level of the ontology. A TBox T consists of concept axioms and role axioms (RBox). Concept axioms (or terminology axioms) have the form C ⊑ D where C and D are (possibly complex) concept descriptions, and role axioms are expressions of the form R⊑S, where R and S are (possibly complex) role descriptions. The signature Sig(T ) of TBox T is the set of concept and role names occur in T .

The semantics of DLs is defined via a model-theoretic semantics, which explicates the relationship between the language syntax and the model of a domain: An interpretation I = (△I , ·I ) consists of a non-empty domain set △I and an interpretation function ·I , which maps from concepts and roles to subsets of the domain and binary relations on the domain, respectively. Given an interpretation I, we say that I satisfies a concept axiom C ⊑ D (respectively, a role inclusion axiom R ⊑ S) if CI ⊆DI (respectively, RI ⊆ SI ). An interpretation I is called a model of a TBox T , written I |= T , iff it satisfies each axiom in T . We use Mod(T ) to denote all the models of a TBox T . Two TBoxes T1 and T2 are equivalent, written T1 ≡ T2, iff Mod(T1) = Mod(T2). A named concept C in a terminology T is unsatisfiable iff, for each model I of T , CI = ∅. A terminology T is inconsistent iff it does not have a model, and it is incoherent iff there exists an unsatisfiable named concept in T . Incoherence is a kind of logical contradiction which has been widely discussed (see [Flouris et al., 2006]). When there is a concept in a TBox, if the TBox is inconsistent, then it must be incoherent.

3 Model-based Revision Operators for Terminologies

In this paper, we assume that there is at least one concept in any TBox and each individual TBox is coherent (so it is consistent by the first assumption). Our revision operators are adapted from Dalal's operator [Dalal, 1988], which is an important model-based operator defined as follows: given two propositional formulas φ and ψ, we first calculate the distance between them as the minimal cardinality of the difference sets between models of φ and models of ψ, then the set of models of the result of revising φ by ψ consists of models of ψ that satisfies the following condition: there exists a model of φ such that the cardinality of the difference set between the two models is the same as the distance between φ and ψ. The difference set between two models consists of propositional variables that are interpreted differently by them.

3.1 Definitions

To adapt Dalal's revision operator to DLs, we need to define the "difference set" between two models. By treating each concept name as a propositional variable, we can define the difference between two models in DLs in a similar way as the difference set between two models in propositional logic. Suppose we want to revise a TBox T1 using another one T2. Following the idea of Dalal's revision operator, in our revision operator, we revise some models of T1 to make them as models of T2. However, we introduce a special treatment. Since logical errors in TBoxes are usually caused by incorrect concept definitions (see [Rector et al., 2004]), to revise a model I of T1, we only revise AI for some concept names A, and keep RI for all role names R intact. We will show that revising AI for some concept names A is enough to turn a model of T1 into a model of T2 (Section 4). In order to ensure that RI is not revised for role names R, the distance between T1 and T2 should not be related to role names. This can be achieved by the following definition of a difference set.

Definition 1. Let T1 and T2 be two TBoxes, and CN and RN be respectively sets of concept names and role names in Sig(T1 ∪ T2). Let I = (Δ, ·I ) and I ′ = (Δ, ·I′ ) be models of T1 and T2 respectively, which are defined on Sig(T1 ∪T2). The difference set between I and I ′ , written diff(I, I ′ ), is defined as follows:

That is, the difference set between two models is the set of all concept names if they interpret a role name differently and the set of concept names that are interpreted differently by the models otherwise. Note that if I1 and I2 do not share a common domain, then they are not comparable.

We can define the distance between two TBoxes. Throughout the paper, we use |S| to denote the cardinality of set S.

Definition 2. Let T1 and T2 be two TBoxes. The distance between T1 and T2, written d(T1 , T2), is defined as:

The distance between two TBoxes T1 and T2 is the minimal cardinality of the difference sets between models of T1 and models of T2.

We define our first revision operator.

Definition 3. Let T1 and T2 be two TBoxes. A revision operator, written ◦M, is defined in a model-theoretical way as follows:

That is, the models of the result of our revision operator ◦M are the models of TBox T2 satisfying the condition that there exists a model of T1 such that the difference between them is equal to the distance between the two TBoxes.

It is easy to see that if T1 is consistent with T2, then T1 ◦M T2 ≡ T1 ∪ T2. From this property, we have that T1 ◦M T2 is incoherent if T1 ∪ T2 is incoherent but consistent. It has been pointed out incoherence will cause trivial subsumption relation on unsatisfiable concepts so that it should be resolved after revision (see [Schlobach et al., 2007] and [Flouris et al., 2006]). The problem of the revision operator is caused by the distance between two TBoxes. That is, when T1 ∪ T2 is incoherent but consistent, their distance is 0. So any interpretation that is a model of T1 ∪T2 is a model of T1 ◦M T2. To solve this problem, we need to give a special treatment of unsatisfiable concepts in T1 ∪ T2.

Definition 4. Let T1 and T2 be two TBoxes and CN be the set of concept names in Sig(T1 ∪T2). The modified distance between T1 and T2, written d′ (T1 , T2), is defined as:

When model I ′ of T2 is used to define the new distance function, it cannot interpret any concept as an empty set. This will exclude the case that there exists model I of T2 such that both I and I ′ interpret an unsatisfiable concept as an empty set. Note that the existence of model I ′ of T2 that does not interpret any concept as an empty set is justified by the assumption that T2 is coherent. By replacing d in Definition 3 with d′ we can get a new revision operator, which is denoted as ◦M′ . The following example shows that we do not have T1 ◦M T2 ≡ T1 ∪ T2 anymore even if T1 ∪ T2 is incoherent but consistent.

Example 1. Let T1 = {A ⊑ B ⊓ D, A ⊑ C, B ⊑ C} and T2 = {A ⊑ ¬B,A ⊑ ¬C}. A is an unsatisfiable concept in T1 ∪ T2. Consider a model I of T2 and a model I ′ of T1 such that ΔI′ = {a, b, c, d}, AI′ = {a}, BI′ = {a, b, c}, CI′ = {a, b, c} and DI′ = {a, c}, and ΔI = {a, b, c, d}, AI = {d}, BI = {a, b, c}, CI = {a, b, c} and DI = {a, c}. We have diffS(I, I ′ ) = {A}. Therefore |diff(I, I ′ )| = 1 and d′ (T1 , T2) = 1. We show that Mod(T1 ◦M′ T2) = Mod(T2 ∪{B ⊑ C}). Suppose I |= T1 ◦M′ T2, then I |= T2 and there exists a model I ′ of T1 such that |diff(I, I ′ )| = 1. It is not difficult to see that we must have diff(I, I ′ ) = {A}. Therefore, BI = BI′ and CI = CI′ . Therefore, I |= B ⊑ C. Conversely, suppose I |= T2 ∪ {B ⊑ C}. Then I |= T2. Suppose I ′ is an interpretation such that ΔI′ = ΔI , BI′ = BI and CI = CI′ , AI′ = ∅ and DI′ = DI . We have diff(I, I ′ ) = {A}. Therefore, I is a model of T1 ◦M′ T2.

From Example 1, to resolve an unsatisfiability, the revision operator ◦M′ may remove all the unsatisfiable concepts in the original TBox. This is not the standard way to deal with unsatisfiability because it does not debug the ontology to find the cause of the contradiction (see [Schlobach et al., 2007]). In Example 1, one of the reasons that concept A becomes unsatisfiable is that it is claimed to be a subconcept of both B and ¬B. To resolve an unsatisfiability, we should change those concepts or axioms that are involved in the contradiction and keep the unsatisfiable concept if possible.

The problem of the revision operator ◦M′ is caused by the definition of difference set. That is, it gives the same priority to the satisfiable concepts and the unsatisfiable concepts in a difference set between two interpretations. To solve this problem, we introduce a notion of stratified set to define a new difference set. Given n sets of concept names S1 , ..., Sn, by S = (S1 , ..., Sn) we denote a stratified set such that elements in Si (i = 1, ..., n) have the same priority but elements in Sj are preferred to those in Sk for any j < k. The cardinality of the stratified set S = (S1 , ..., Sn) is defined as an ordered set of numbers |S| = (|S1|, ..., |Sn|). Let S = (S1 , ..., Sn) and S′ = (S′1 , ..., S′n ), |S| < |S′ | iff there exists an i ∈ {1, ..., n}, such that |Si| < |S′ i | and |Sj| = |S′j | for any j < i, and |S| = |S′ | iff |Si| = |S′ i | for any i ∈ {1, ..., n}. We now define a stratified difference set between two interpretations. We assume that the set CN of concept names in signature Sig(T1 ∪ T2) has been stratified such that some concept names are more important than others. When defining the stratified difference set between interpretations I and I ′ , we first give higher priority to concept names in diff(I, I ′ ) that are unsatisfiable in T1 ∪ T2 than those that are satisfiable in T1 ∪ T2, then further stratify these two sets of concept names using the stratified set on CN. Formally, we have the following definition.

Definition 5. Let T1 and T2 be two TBoxes. Suppose (S1 , ..., Sn) is a stratified set on all concept names in Sig(T1 ∪ T2). Let I = (Δ, ·I ) and I ′ = (Δ, ·I′ ) be two interpretations. Let U = {A ∈ diff(I, I ′ ) | A is unsatisfiable in T1 ∪ T2} and W = diff(I, I ′ ) \ U. The stratified difference set between I and I ′ , written diffS(I, I ′ ), is defined as follows: diffS(I, I ′ ) = (U ∩ S1 , ..., U ∩ Sn, W ∩ S1 , ..., W ∩ Sn)

Similarly, we can define dS(T1 , T2) through replacing diff by diffS in Definition 4 and then define a new revision operator through replacing diff by diffS and replacing d by dS in Definition 3, which is denoted as ◦S. We need some further explanations of the stratified set on concept names in Sig(T1 ∪ T2) in Definition 5. There are some benefits of defining the stratified difference set by this stratified set. First, based on different stratified sets, we can define different difference sets, thus different revision operators. We allow users to order the signature of the language and decide which concept names are more important than others. Therefore, our revision operator is more flexible than those defined previously. Second, in Section 5, we will provide a special stratified set on concept names in Sig(T1 ∪ T2) such that the result of the revision operator defined by the stratified difference set can be computed in polynomial time for a lightweight DL. A naive stratified set is to give all concept names in Sig(T1 ∪ T2) the same priority. In this case, n = 1 in Definition 5 and diffS(I, I ′ ) = (U, S1 \ U). We illustrate the new revision operator using Example 1, by taking this naive stratified set.

Example 2. Consider model I of T2 and model I ′ of T1 such that ΔI′ = {a, b, c, d}, AI′ = {a}, BI′ = {a, b, c}, CI′ = {a, b, c} and DI′ = {a, c}, and ΔI = {a, b, c, d}, AI = {a}, BI = {b, c}, CI = {b, c} and DI = {a, c}. We have diffS(I, I ′ ) = (∅, {B,C}). So |diffS(I, I ′ )| = (0, 2). We must have d(T1 , T2) = (0, 2) based on the following observations: (1) for any pair of interpretations I1 and I ′1 , we must have AI1 = AI′1 ̸= ∅, (2) for any pair of interpretations I1 and I ′1 , if |diffS(I1 , I ′1 )| = (0,m), where m is an integer, then we must have m ≥ 2. Therefore, a model I of T2 is a model of T1 ◦S T2 iff there exists a model I ′ of T1 such that ΔI = ΔI′ and |diffS(I, I ′ )| = (0, 2).

3.2 Syntactical counterpart of revision operator ◦S

We show that the result of our revision operator ◦S can be computed with the help of the notion of concept forgetting.

It has been shown in [Lang and Marquis, 2002] that Dalal's revision operator is a special case of a general framework based on variable forgetting, where a propositional variable forgotten in a propositional formula will result in another formula which is logically strongest consequence of the original formula that is independent of the variable. This inspires us to provide an approach for computing our revision operator ◦S syntactically by using the notion of forgetting in DLs.

We first introduce the relation ∼A and the notion of concept forgetting given in [Wang et al., 2008]: let A be a concept name in a DL language L, and I and I ′ interpretations of L. We define I ∼A I ′ iff I and I ′ agree on all concept names and role names except possibly on A. The result of forgetting about A in T , denoted as forget(T ,A), is defined in a model-theoretical way as follows: forget(T , A) is a TBox on the signature Sig(T ) \ {A} and any interpretation I ′ is a model of forget(T ,A) iff there is a model I of T such that I ∼A I ′ . It has been shown in [Wang et al., 2008] that when we forget a set A = {A1 , ...,An} of concept names, the order of concept forgetting will not influence the final result of forgetting. Therefore, we can define forget(T ,A) = forget(...(forget(T , A1), ...), An). In [Wang et al., 2008], an algorithm is given to compute the result of concept forgetting in DL-Lite, a family of DLs that provide tractable reasoning. However, for more expressive DLs, the result of concept forgetting may not be expressed in the same language [Konev et al., 2008]. In the following, we define a revision operator by using the notion of forgetting and show that this operator corresponds to the revision operator ◦S.

We define the notion of recovery set, which is a set of concept names in the original TBox that will be forgotten to restore coherence.

Definition 6. Given two TBoxes T1 and T2, a recovery set of T1 w.r.t. T2 is a set V of concept names in T1 ∪ T2 such that forget(T1 , V ) ∪ T2 is coherent.

We use RT2 T1 to denote all the recovery sets of T1 w.r.t. T2. A trivial recovery set is the set CN of all concept names in T1 ∪ T2 as forget(T1 ,CN) = ∅ and T2 is assumed to be coherent. In Example 1, {A} and {B,C} are recovery sets of T1 w.r.t. T2. Among all the recovery sets of T1 w.r.t. T2, some are preferred to others. In the following, we define a preference relation on RT2 T1 . We first stratify a recovery set by giving priority to unsatisfiable concepts in it and further stratify these unsatisfiable concepts and other concepts by a pre-defined stratified set. We then compare two recovery sets by comparing the cardinality of their stratified sets.

Definition 7. Let T1 and T2 be two TBoxes. Suppose (S1 , ..., Sn) is a stratified set on all concept names in Sig(T1 ∪ T2). A preference relation on RT2 T1 , called a lexicographic relation and is denoted as ⪯lex, is defined as follows: for any two recovery sets V1 and V2, let Ui = {A ∈ Vi | A is unsatisfiable in T1 ∪ T2} and Wi = Vi \ Ui for i = 1, 2. V1 ⪯lex V2 iff |(U1 ∩S1 , ..., U1 ∩Sn, W1 ∩S1 , ...,W1 ∩Sn)| ≤ |(U2 ∩ S1 , ..., U2 ∩ Sn, W2 ∩ S1 , ...,W2 ∩ Sn)|.

We call a recovery set V ∈ RT2 T1 preferred if for all recovery sets V ′ ∈ RT2 T1 , V ⪯lex V ′ . By Pre(RT2 T1 ) we denote the set of all preferred recovery sets in RT2 T1 .

Definition 8. Let T1 and T2 be two TBoxes. Suppose (S1 , ..., Sn) is a stratified set on all concept names in Sig(T1 ∪ T2). A forgetting-based revision operator, denoted as ◦f , is defined as follows:

T1 ◦f T2 consists of the union of T2 and the knowledge bases 1 obtained from T1 by forgetting preferred recovery sets. Therefore, the result of revision is a set of knowledge bases. In [Meyer et al., 2005], a set of knowledge bases is called a disjunctive knowledge base (DKB). Its semantics is given as follows: A DKB B is satisfied by an interpretation I iff I is a model of at least one of elements of B.

Example 3. (Example 1 continues) Suppose the stratified set on {A,B,C} is {{A,B,C}}. There are several recovery sets of T1 w.r.t. T2, such as {A}, {B,C}, {A,B,C}, etc. It is easy to check that V = {B, C} is the only preferred recovery set. Therefore, T1 ◦f T2 = {forget(T1 , V ) ∪ T2} = {{A ⊑ D} ∪ T2}. That is, we get a unique TBox T = {A ⊑ D, A ⊑ ¬B, A ⊑ ¬C} as the result of revision.

One may notice that our revision operator drops more information than necessary to restore coherence because B ⊑ C can be added to T without causing a contradiction. This kind of problem can be fixed, for example, by taking another step to restore unnecessary removals by a syntax-based revision after we apply the forgetting-based revision operator. The detailed discussion of this problem will be left as future work.

We are able to show that revision operators ◦S and ◦f are semantically equivalent. Due to page limit, proofs of propositions in this paper are either omitted or sketched. Full proofs can be found in a technical report at http://www.aifb.unikarlsruhe.de/WBS/gqi/papers/IJCAI09QD.pdf.

Proposition 1. Let T1 and T2 be two TBoxes. Suppose (S1 , ..., Sn) is a stratified set on all concept names in Sig(T1 ∪ T2). If both ◦S and ◦f are defined by (S1 , ..., Sn), then we have Mod(T1 ◦S T2) = Mod(T1 ◦f T2).

Proof sketch. We first show that Mod(T1 ◦S T2) ⊆ Mod(T1 ◦f T2).

Suppose I |= T1 ◦S T2, then there exists a model I ′ of T2 such that diffS(I, I ′ ) = dS(T1 , T2), RI = RI′ for any R ∈ RN, and AI′ ̸= ∅ for any A ∈ CN. We set V as the set of all the concept names in diffS(I, I ′ ). We first show that V is a recovery set, that is, forget(T1 , V ) ∪ T2 is coherent by showing that I ′ is model of forget(T1 , V )∪T2 and using the fact that AI′ ̸= ∅ for any A ∈ CN. Next, we show that V is a preferred recovery set by reduction to absurdity by using the fact that if forget(T1 , V ) ∪ T2 is coherent, then there exists a model I of forget(T1 , V ) ∪ T2 such that AI ̸= ∅ for any unsatisfiable concept of T1 ∪ T2 and there exists a model I ′ of T1 such that I ∼V I ′ .

Second, we show that Mod(T1 ◦f T2) ⊆Mod(T1 ◦S T2). Suppose I |= T1 ◦f T2. Then I |= forget(T1 , V ) ∪ T2. Since I |= forget(T1 , V ), there exists I ′ |= T1 such that I ∼V I ′ . So |diff(I, I ′ )| = |V |. We show that dS (T1 , T2) = |(U ∩ S1 , ..., U ∩ Sn,W ∩ S1 , ...,W ∩ Sn)| by reduction to absurdity. Therefore, |diffS(I, I ′ )| = dS (T1 , T2). Since I |= T2 and I ′ |= T1, I is a model of T1 ◦S T2.

1 The result of forgetting may not be a DL knowledge base anymore.

For a terminological axiom φ, T1 ◦f T2 |= φ (resp. T1 ◦S T2 |= φ) if φ is satisfied by every model in Mod(T1 ◦f T2) (resp. Mod(T1 ◦S T2)). Proposition 1 tells that there exists an algorithm to decide if T1 ◦S T2 |= φ, provided that there exist algorithms for computing the function forget, because T1 ◦S T2 |= φ iff T1 ◦f T2 |= φ iff forget(T1 , V ) ∪T2 |= φ for all preferred recovery set V ∈ Pre(RT2 T1 ).

4 Logical properties

We consider postulates for revision operators in DLs given in [Qi et al., 2006], which are reformulated from Katsuno and Mendelzon's postulates (KM postulates) in [Katsuno and Mendelzon, 1992].

• (G1) Mod(T1 ◦T2) ⊆ Mod(φ) for all φ ∈ T2.
• (G2) If Mod(T1)∩Mod(T2) ̸= ∅, then Mod(T1 ◦T2) = Mod(T1)∩Mod(T2).
• (G3) If T2 is consistent, thenMod(T1 ◦T2) ̸= ∅.
• (G4) If Mod(T ) = Mod(T1) and Mod(T ′ ) = Mod(T2), then Mod(T ◦T ′ ) = Mod(T1 ◦T2).
• (G5) Mod(T1 ◦T2)∩Mod(T3)⊆Mod(T1 ◦(T2∪T3)).
• (G6) If Mod(T1 ◦T2)∩Mod(T3) is not empty, then Mod(T1 ◦(T2∪T3))⊆Mod(T1 ◦T2)∩Mod(T3).

(G1) guarantees that every axiom in the new TBox can be inferred from the result of revision. (G2) says that we do not change the original knowledge base if there is no conflict. (G3) is a condition preventing a revision from introducing unwarranted inconsistency. (G4) says the revision operator should be independent of the syntactical forms of knowledge bases. (G5) and (G6) together are used to ensure minimal change.

We are able to show that the operator ◦M satisfies all these postulates.

Proposition 2. ◦M satisfies (G1)-(G6).

Postulates (G1)-(G6) are reasonable when we only want to deal with inconsistency. However, (G2) is not a good postulate to capture a rational revision operator for terminologies because it infers that if a TBox is consistent with another one but their union is incoherent, then the result of revision is still incoherent. This is exactly the problem for the revision operator ◦M given by Definition 3. Therefore, we modify (G2) as follows:

(G2′ ) For any TBox T1 and any coherent TBox T2, T1 ∪T2 is coherent if and only if Mod(T1 ◦T2) = Mod(T1)∩Mod(T2).

Postulate (G2′ ) requires that if T1 ∪T2 is incoherent but T2 is coherent, then the result of revision should not be equivalent to their union. It is clear that ◦M does not satisfy this postulate.

We are able to show that our revision operators ◦M′ and ◦S satisfy (G2′ ) and many other postulates.

Proposition 3. For any stratified set on all concept names in Sig(T1 ∪ T2), ◦M′ satisfies (G1),(G2′ ) and (G3)-(G6). ◦S also satisfies (G1),(G2′ ) and (G3)-(G6). But they do not satisfy (G2) in general.

Proposition 3 shows that postulates (G1),(G2′ ) and (G3)- (G6) do not differentiate operator ◦S and operator ◦M′ . Therefore, we propose a new postulate which is satisfied by ◦S but falsified by ◦M′ .

Unsatisfiability Repair Given two TBoxes T1 and T2, suppose there exists a set V of satisfiable concepts in T1 ∪T2 such that all the unsatisfiable concepts in T1 ∪ T2 are satisfiable in forget(T1 , V )∪T2. Then for any model I ∈ Mod(T1 ◦T2), there exists a model I ′ ∈ Mod(T1) such that AI = AI′ for all unsatisfiable concept A in T1 ∪ T2.

This postulate says if we can resolve all unsatisfiable concepts by forgetting some satisfiable concepts, then none of the unsatisfiable concepts should be forgotten after revision. Example 1 shows that ◦M′ does not satisfy this postulate.

Proposition 4. For any stratified set on all concept names in Sig(T1 ∪ T2), ◦S satisfies the postulate "Unsatisfiability Repair".

Propositions 1-4 show that ◦S is better than other two when applied to deal with incoherence.

5 Computational Issues of Revision Operator ◦S in DL-Lite⊓

We first analyze the computational complexity of our revision operator in a special DL, called DL-Lite⊓. The language of DL-Lite⊓ extends the core language for the DL-Lite family [Calvanese et al., 2007] by allowing conjunctions of basic concepts in the left-hand side of inclusion axioms, where there exists an algorithm to compute the result of concept forgetting [Wang et al., 2008]. The DLs of the DL-Lite family are tailed to capture conceptual modeling constructs, but still have low reasoning overheads. All reasoning tasks in the DLs of this family, such as concept subsumption and answering complex queries, are computationally tractable.

We show the time complexity of subsumption checking under our revision operator.

Proposition 5. Given two TBoxes T1 and T2 in DL-Lite⊓ and a concept subsumption axiom φ in DL-Lite⊓, the problem of deciding if T1 ◦S T2 |= φ is Δp2 -complete.

Proof sketch. (Hardness)We show this by a ≤pm-reduction of the following Δp2 -complete problem [Krentel, 1988]: Given a satisfiable clause set C = {Cl, ..., Cn} on X = {x1 , ..., xn}, decide whether the lexicographically maximum truth assignment Φ(X) on (x1 , ..., xn), which we denote by Φm(X), fulfills Φm(xn) = true. For 1 ≤ j ≤ m, let L(Cj) denote the set of literals in Cj. For l a literal occurring in C, let Bl denote the concept name Ai if l is xi, or A′i if l is ¬xi.

Let T1 = {Gi ⊑ Ai, Gi ⊑ A′i , Gi+n ⊑ Ai, Gi+n ⊑ A′′ i | 1 ≤ i ≤ n} ∪ {Hj ⊑ Bl | 1 ≤ j ≤ m, l ∈ L(Cj)} and T2 = {Ai ⊓ A′i ⊑ ¬Gi,Ai ⊓ A′′ i ⊑ ¬Gi+n | 1 ≤ i ≤ n} ∪ {bigsqcapl∈L(Cj ) Bl ⊑ ¬Hj | 1 ≤ j ≤ m}. We define a stratified set for ◦S as S = ({Gi | 1 ≤ i ≤ 2n} ∪ {Hj | 1 ≤ j ≤ m}, {Ai,A′i | 1 ≤ i ≤ n}, A′′ 1 , . . . , A′′n ). For a truth assignment Φ(X), let VΦ denote {Ai | 1 ≤ i ≤ n,Φ(xi) = true} ∪ {A′i , A′′ i | 1 ≤ i ≤ n,Φ(xi) = false}. Then VΦ is a recovery set of T1 w.r.t. T2 iff Φ(X) satisfies C. Note that for a preferred recovery set V of T1 w.r.t. T2, since V does not contain any Gi or Hj, it must contain Ai or A′i ,A′′ i for all 1 ≤ i ≤ n; otherwise some Gi is unsatisfiable in forget(T1 , V ) ∪ T2. Since S prefers recovery sets that do not contain A′′ 1 (and hence contain A1) over recovery sets that contain A′′ 1 etc., it is clear that for distinct truth assignments Φ(X) and Ψ(X) satisfying C, we have VΦ ⪯lex VΨ iff Φ(X) is not lexicographically less than Ψ(X) w.r.t. (x1 , ..., xn). It follows that Pre(RT2 T1 ) = {VΦm }. Hence T1 ◦S T2 |= Gn ⊑ A′n iff T1 ◦f T2 |= Gn ⊑ A′n (by Proposition 1) iff A′n ̸∈ VΦm iff Φm(xn) = true. Since T1, T2 and S can be constructed in polynomial time, the hardness holds.

(Membership) Let the stratified set for ◦S be (S1 , ..., Sn). We use the following algorithm to check if T1 ◦ST2 |= φ.

1. U := {A ∈ ⋃ni=1 Si | A is unsatisfiable in T1 ∪ T2};
2. for i := 1, ..., n do Ti = U ∩Si; Ti+n = Si \ U;
3. for i := 1, ..., 2n do
4. for j := 0, ..., |Ti| do
5. Guess (V1, ..., Vi) where Vk ⊆ Tk for all 1 ≤ k ≤ i, and check if |Vk| = mk for 1 ≤ k ≤ i - 1, |Vi| = j and ⋃ik=1 Vk ∪ ⋃2n k=i+1 Tk is a recovery set of T1 w.r.t. T2; if so, set mi as j and continue next i;
6. Guess a stratified set (W1, ...,Wn) where Wi ⊆ Si for all 1 ≤ i ≤ n, and check if ⋃ni=1 Wi is a recovery set of T1 w.r.t. T2, forget(T1, ⋃ni=1 Wi) ∪ T2 ̸|= φ, and for all 1 ≤ i ≤ n, |Wi ∩U| =mi and |Wi \ U| =mi+n; if so, return false;

7. return true;

In the above algorithm, a preferred recovery set V is computed in lines 1-5 by a guess-and-test approach, and mi is set as |V ∩ Ti| for all 1 ≤ i ≤ 2n. Clearly (m1 , ...,m2n) is unique for all preferred recovery sets. Note that U can be computed in polynomial time. Note also that the checking process in line 5 or line 6 can be accomplished in polynomial time, so the algorithm finishes after calling an NP oracle O(1 + ∑2n i=1 (|Ti| + 1)) = O(∑ni=1 |Si|) times. That is, the algorithmworks in Δp2 time.

The above proposition shows that subsumption checking under ◦S is in general intractable. However, in a special case where every concept name constitutes a stratum in the given stratified set for ◦S, subsumption checking in DL-Lite⊓ under ◦S is tractable (see Algorithm 1).

• Algorithm 1. Checking(T1, T2, (S1 , . . . , Sn), φ) Input: Two TBoxes T1 and T2, a stratified set (S1, . . . , Sn) on all concept names in Sig(T1 ∪ T2) such that |Si| = 1 for all 1 ≤ i ≤ n, and a concept subsumption axiom φ. Output: The truth value of T1 ◦S T2 |= φ, where ◦S is defined by (S1, . . . , Sn). 1. U := {A ∈ ⋃ni=1 Si | A is unsatisfiable in T1 ∪ T2}; V := ∅; 2. for i := 1, ..., n do Ti := Si ∩U; Ti+n := Si \ U; 3. for i := 1, ..., 2n with Ti ̸= ∅ do 4. if forget(T1, V ∪ ⋃2n k=i+1 Tk) ∪ T2 is incoherent then 5. V := V ∪ Ti; 6. return forget(T1, V ) ∪ T2 |= φ;

Algorithm 1 first computes the unique preferred recovery set V in RT2 T1 (lines 1-5), then checks whether forget(T1 , V ) ∪ T2 |= φ (line 6). By Proposition 1, the result of the above checking is exactly the truth value of T1 ◦S T2 |= φ. In the algorithm, Ti consists of at most one axiom for any 1 ≤ i ≤ 2n. Since a preferred recovery set V should make |(T1 ∩ V, ..., T2n ∩ V )| minimal among that of all recovery sets, RT2 T1 has only one preferred recovery set. It is computed by considering T1 , ..., T2n in turn to keep as many axioms with higher priority as possible while guaranteeing coherence. Let V be a partial preferred recovery set before considering Ti. Then Ti is appended to V if forget(T1 , V ∪ ⋃2n k=i+1 Tk) ∪ T2 is incoherent, because otherwise coherence cannot be restored by considering Ti+1 , ..., T2n. Since the result of concept forgetting in DLLite⊓ TBoxes can be computed in polynomial time [Wang et al., 2008], as well as coherence checking and subsumption checking in DL-Lite⊓ can be accomplished in polynomial time [Calvanese et al., 2007], Algorithm 1 works in polynomial time.

6 RelatedWork

In [Flouris et al., 2005], Flouris et al. generalize the well-known AGM (Alchourr´on, G¨ardenfors and Markinson) framework in order to apply the rationales behind the AGM framework to a wider class of logics. In [Flouris et al., 2006], a framework for the distinction between incoherence and inconsistency of an ontology is proposed. A set of rational postulates for a revision operator in DLs is proposed. In [Qi et al., 2006], reformulated AGM postulates for revision are adapted to DLs. A set of postulates is given in [Ribeiro and Wassermann, 2007] by adapting Hansson's postulates for a semi-revision operator (see [Hansson, 1999]).

Some concrete operators have been proposed. In [Haase et al., 2005], an algorithm is given to determine consistent subontologies by adding an axiom to an ontology. A revision operator is given in [Halaschek-Wiener et al., 2006] based on Hansson's kernel operator. In [Qi et al., 2006], the authors propose two revision operators that satisfy their postulates. All these revision operators deal with inconsistencies. Qi et al. in [Qi et al., 2008] propose a general revision operator to deal with incoherence by adapting Hansson's kernel revision operator. However, this operator is not fine-grained in the sense that it removes a whole axiom from a TBox if it is selected by an incision function. Our revision operators are different from existing ones in that they follow another family of belief revision operators, i.e. model-based revision operators, so they are more fine-grained than existing ones.

Our work is different from existing revision approaches on prioritized knowledge bases, such as [Benferhat et al., 2002], because our work is based on a preference over concept names.

7 Conclusion and FutureWork

In this paper, we adapted the well-known Dalal revision operator for revising terminologies in description logics. We pointed out some pitfalls when we tried to adapt the notion of a difference set between two interpretations and the notion of a distance function between TBoxes. We defined three model-based revision operators successively and showed that one of them (◦S) is more rational than others using some examples. We then defined a revision operator syntactically using the notion of concept forgetting and showed that this operator is semantically equivalent to the revision operator

◦S. We considered logical properties of our revision operators with respect to postulates given in [Qi et al., 2006] and by proposing some new postulates. We showed that the revision operator ◦S is more rational than others. Finally, we showed that subsumption checking in DL-Litecore under our revision operator ◦S is P NP [O(log n)] -complete and provided a polynomial time algorithm to compute the result of revision in a special case.

We consider only revision of terminologies in DLs. As a future work, we will extend our work to consider ontologies with ABoxes. This is very challenging because it has been shown in [Wang et al., 2008] that even for DL-Lite languages, forgetting results in DL-Lite with ABoxes are not expressible in the same language. We will consider the following solutions. First, we do not require that the result of revision must be expressed in the same language as the original language for the ontologies under consideration. Second, we consider approximation of the result of revision in the original language, like the work done in [Giacomo et al., 2007].

Acknowledgments

Thanks three anonymous reviewers for their useful comments. Guilin Qi is partially supported by the EU under the IST project NeOn (IST-2006-027595). Jianfeng Du is partially supported by NSFC grants 60673103, 60721061 and 70801020.