Introduction The problem of revising a description logic-based ontology (called DL ontology) is closely related to the problem of belief revision which has been widely discussed in the literature. Among early works on belief revision, the AGM theory (Alchourrón et al., 1985) introduced intuitive and plausible constraints (namely AGM postulates) which should be satisfied by any rational belief revision operator. However, it is not trivial to adapt belief revision operators to DLs because DLs have their own features (Flouris et al., 2005) (Qi and Yang, 2008). One main difficult for such revision is that DL ontologies often incur infinitely many models. To address this issue, we propose a finite set of finite structures, namely a set MT(O) of completion trees, for characterizing a possibly infinite set of models of an ontology O. Then, we define a distance over a set of completion trees. This distance allows one to determine how far an ontology is from another one. Another problem our approach has to address is that there may not exist a revision ontology such that (i) it is expressible in the logic used for expressing initial ontologies O; O0, and (ii) it admits exactly a set of models MT(O; O0) computed from MT(O) and MT(O0). For this reason, we borrow the notion of maximal approximation (De Giacomo et al., 2007) which allows us to build a minimal revision ontology admitting MT(O; O0). Construction of the revision ontology First, we define a novel tableau algorithm, namely TA, for a SHIQ ontology without individuals by replacing expansion v-, u-, t, ch-rules by a new rule, namely sat-rule which chooses a subset S from a set sub(O) including all sub-concepts of a SHIQ ontology O. Note that all concepts in the form of conjunctions or of disjunctions are removed from sub(O) and replaced with their conjuncts and disjuncts. This can be performed by a function Flat(C) that flattens conjunctions and disjunctions of a concept C into subsets of sub-concepts occurring in C. For example, Flat(A u (9R:B t C)) = ffA; 9R:Bg; fA; Cgg. sat-rule. If sat-rule has never been applied to a node x then we choose a subset S sub(O) such that L(x) [ S f (C v D) S where f (C v D) 2 Flat(:C t D)
CvD2T for each C v D 2 T , and set L(x) := S [ S where S = f:C j C 2 sub(O) n Sg In this paper, a completion tree for O is a tree T = (V; E; L; x) where V is a b set of nodes with the root node xb 2 V . Each node x 2 V is labeled with a function L(x) sub(O). E is a set of edges and each edge hx; yi 2 E is labeled with a function L(hx; yi) containing a set of SHIQ roles.
The sat-rule that is applied to each node of a completion tree introduces a lot of nondeterminisms. We need this “bad” behavior of the new tableau algorithm to control the generation process of completion trees in such a way that allows one to infer the ontology when knowing completion trees and its signature. We use MT(O) to denote the set of all completion trees which are generated by running the novel tableau algorithm TA for an ontology O. Note that TA does not necessarily terminate when a complete and clash-free completion tree is built. It should terminate when all non-determinisms are considered. We can extend straightforwardly MT(O) to MT(O0; sub(O)) as follows. The set MT(O0; sub(O)) is built by the tableau algorithm TA for O0 with an extra set of concepts sub(O) that is taken into account when applying the sat-rule. In this case one can import additional concepts into node labels of a completion tree for O0 while respecting the axioms of O0. Importing sub(O) to MT(O0) ensures that MT(O0; sub(O)) captures semantic constraints from O which are compatible with O0.
Next, we introduce a distance between two completion trees T and T 0 which allows one to talk about the similarity between two ontologies. This distance is defined for two completion trees which are isomorphic, i.e., there is an isomorphism that maintains the successor relationship from two nodes of a completion tree to the two corresponding nodes of the other one via . Note that we can always obtain such an isomorphism between two completion trees by adding empty nodes and edges to completion trees since node and edge labels are ignored in the definition of isomorphisms. Definition 1 (Distance). Let T = hV; L; E; xbi and T 0 = hV 0; L0; E0; xb0i two completion trees. Let (T; T 0) be the set of all isomorphisms between T and T 0. The distance between T and T 0, denoted T M T 0, is defined as follows: T M T 0 = 2 m(iTn;T 0)f mx2aVx(jL(x) M L0( (x))j)+hxm;yai2xE(jL(hx; yi) M L0(h (x); (y)i)j)g We can check that M is a distance over a set of isomorphic trees with the operator M defined over two node or edge labels ; 0 as follows: L( ) M L0( 0) = (L( ) [ L0( 0)) n (L( ) \ L0( 0)). Based on this distance, we now define a set of completion trees a revision ontology of an ontology O by another O0 should admit. Definition 2 (Revision operation). Let O and O0 be two consistent SHIQ ontologies. A set of tree models MT(O; O0) of the revision of O by O0 is defined as follows: MT(O; O0) = fT 2 MT(O0; sub(O)) j 9T0 2 MT(O; sub(O0));
8T 0 2 MT(O; sub(O0)); T 00 2 MT(O0; sub(O)) : T M T0 T 0 M T 00g Intuitively, MT(O0; sub(O)) includes completion trees from MT(O0) each node of which is consistently filled by an arbitrary set of concepts imported from sub(O) such that each axiom of O0 remains satisfied. Among these completion trees, MT(O; O0) retains only those which are closest to completion trees from MT(O; sub(O0)) thanks to the operator T M T 0 that characterizes the difference between T and T 0. We consider the following example. Let O = f> v A u 9R:(:B) u :Bg and O0 = f:A v 8R:B; :B v A u 8R:Bg. By running the algorithm TA for O, we build the set MT(O; sub(O0)) which contains a unique tree model T1 with nodes fa; bg and labels L(a) = fA; 9R:(:B); :Bg; L(b) = fA; 9R:(:B); :Bg; E = fR(a; b)g. In the same way, MT(O0; sub(O)) has 4 tree models one of which is T10 with nodes fa0; b0g and labels L(a0) = fA; 9R:(:B); Bg; L(b0) = f:B; A; 8R:Bg; fR(a0; b0)g. According to Definition 2, we have T10 M T1 = 2 that is minimal. Thus, MT(O; O0) contains a unique tree model T10.
We obtain a strong result which states that the all AGM postulates rephrased
By soundness and completeness of the tableau algorithm, we can show that Mod(O) is semantically equivalent to MT(O), i.e., MT(O) j= iff Mod(O) j= for some axiom . Moreover, it holds that Mod(O) \ Mod(O0) 6= ; iff MT(O; sub(O0)) \ MT(O0; sub(O)) 6= ;. Therefore, as (G2) our postulate (P2) captures the fact that if O [ O0 is consistent, then the revision ontology of O by O0 should admit exactly shared models of O and O0. Such models are encapsulated in MT(O; sub(O0)) \ MT(O0; sub(O)) by our setting.
Finally, our goal is to build from MT(O; O0) a revision ontology Ob that admits exactly MT(O; O0) as tree models. However, we can show that there may not exist such an ontology Ob by reconsidering the example above with MT(O; O0) = fT10g. Assume that there exists an ontology Ob with sub(Ob) = fA; :A; B; :B; 9R:(:B); 8R:Bg which admits the unique T10 as tree model. Due to the specific behavior of the sat-rule with sub(Ob), if we apply TA to Ob for building MT(Ob), we must obtain T1 and another tree model T20 with one node fxg, L(x) = fA; 8R:B; Bg, which is a contradiction.
For this reason, we use the notion of maximal approximation
Definition 3 (Revision ontology). Let O and O0 be two consistent SHIQ ontologies
with revision operation MT(O; O0) = fT1; ; Tng where Ti = hVi; Li; Ei; xbii for
1 i n. A revision ontology O = (T ; R) of O by O0 can be built from completion
trees in MT(O; O0) as follows: R includes the role hierarchy of O0 and the one of O;
T contains all axioms of O0 and the following axiom : > v G ( G ( l C)).
Theorem 1. Let O and O0 be two consistent SHIQ ontologies. The revision ontology
O of O by O0 is a maximal approximation from MT(O; O0). Additionally, the size of
O is bounded by a doubly exponential function in the size of O and O0.
Conclusion The main limitation of our approach is to omit individuals in ontologies.
However, our approach can be extended in order to deal with individuals by
extending the distance defined for completion trees to graphs. Another limitation is that the
obtained revision ontology is very large. This exponential blow-up in size arises from
doubly exponential size of completion trees. We believe that our procedure can be
improved by using a method for compressing completion trees generated from tableau
algorithms. Such a method has been proposed by Le Duc et al.