Tableau-based revision in SHIQ Thinh Dong, Chan Le Duc, Philippe Bonnot, Myriam Lamolle LIASD - EA4383, IUT of Montreuil, University of Paris8, France {dong, leduc, bonnot, lamolle}@iut.univ-paris8.fr 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 con- junctions and disjunctions of a concept C into subsets of sub-concepts occurring in C. For example, Flat(A u (∃R.B t C)) = {{A, ∃R.B}, {A, C}}. sat-rule. If sat-rule has neverSbeen applied to a node x then we choose a subset S ⊆ sub(O) such that L(x) ∪ f (C v D) ⊆ S where f (C v D) ∈ Flat(¬C t D) CvD∈T for each C v D ∈ T , and set L(x) := S ∪ S̄ where S̄ = {¬C | C ∈ sub(O) \ S} In this paper, a completion tree for O is a tree T = (V, E, L, x b) where V is a set of nodes with the root node x b ∈ V . Each node x ∈ V is labeled with a function L(x) ⊆ sub(O). E is a set of edges and each edge hx, yi ∈ 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 non- determinisms. 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 ontol- ogy 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 re- specting 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, x bi and T 0 = hV 0 , L0 , E 0 , x b0 i two com- pletion 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 = min 0 {max(|L(x) M L0 (π(x))|)+ max (|L(hx, yi) M L0 (hπ(x), π(y)i)|)} π∈Π(T,T ) x∈V hx,yi∈E 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 )) \ (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 ) = {T ∈ MT(O0 , sub(O)) | ∃T0 ∈ MT(O, sub(O0 )), ∀T 0 ∈ MT(O, sub(O0 )), T 00 ∈ MT(O0 , sub(O)) : T M T0 ≤ T 0 M T 00 } 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 = {> v A u ∃R.(¬B) u ¬B} and O0 = {¬A v ∀R.B, ¬B v A u ∀R.B}. By running the algorithm TA for O, we build the set MT(O, sub(O0 )) which contains a unique tree model T1 with nodes {a, b} and labels L(a) = {A, ∃R.(¬B), ¬B}, L(b) = {A, ∃R.(¬B), ¬B}, E = {R(a, b)}. In the same way, MT(O0 , sub(O)) has 4 tree models one of which is T10 with nodes {a0 , b0 } and labels L(a0 ) = {A, ∃R.(¬B), B}, L(b0 ) = {¬B, A, ∀R.B}, {R(a0 , b0 )}. 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 (Qi et al., 2006) for DL ontologies in our setting hold. This result relies on a total pre-order over a set of all completion trees that can be devised from the distance according to Definition 1. The main difference between the postulates presented by Qi et al. and those reformulated in our setting is that the set of models Mod(O) of an ontology O is replaced with MT(O). To illustrate this point, we consider a postulate by Qi et al. (G2): If Mod(O) ∩ Mod(O0 ) 6= ∅ then Mod(O, O0 ) = Mod(O) ∩ Mod(O0 ); and our corresponding postulate: (P2) If MT(O, sub(O0 )) ∩ MT(O0 , sub(O)) 6= ∅ then MT(O, O0 ) = MT(O, sub(O0 )) ∩ MT(O0 , sub(O)). A proof of (P2) can be obtained straightforwardly from the definition of MT(O, sub(O0 )) and MT(O, O0 ). By soundness and completeness of the tableau algorithm, we can show that Mod(O) is semantically equivalent to MT(O), i.e., MT(O) |= α iff Mod(O) |= α 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 O b that admits ex- actly MT(O, O0 ) as tree models. However, we can show that there may not exist such an ontology O b by reconsidering the example above with MT(O, O0 ) = {T 0 }. Assume that 1 there exists an ontology O b with sub(O)b = {A, ¬A, B, ¬B, ∃R.(¬B), ∀R.B} which admits the unique T10 as tree model. Due to the specific behavior of the sat-rule with sub(O), b if we apply TA to O b for building MT(O), b we must obtain T1 and another tree 0 model T2 with one node {x}, L(x) = {A, ∀R.B, B}, which is a contradiction. For this reason, we use the notion of maximal approximation (De Giacomo et al., 2007) to define an ontology O∗ which satisfies the following conditions: (i) O∗ is ex- pressible in SHIQ, (ii) it admits tree models in MT(O, O0 ), and (iii) it is a “smallest” ontology admitting MT(O, O0 ). Such an ontology O∗ , namely maximal approximation, can be built from the node labels of all tree models in MT(O, O0 ). Definition 3 (Revision ontology). Let O and O0 be two consistent SHIQ ontologies with revision operation MT(O, O0 ) = {T1 , · · · , Tn } where Ti = hVi , Li , Ei , xbi i 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 hierarchyG of O0 G and thelone of O; 0 T contains all axioms of O and the following axiom : > v ( ( C)). 1≤i≤n x∈Vi C∈Li (x) 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 extend- ing 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 im- proved by using a method for compressing completion trees generated from tableau algorithms. Such a method has been proposed by Le Duc et al. (Le Duc et al., 2013). Acknowledgements This work was partially supported by FUI project “Learning Café”. References [Alchourrón et al., 1985] Carlos Alchourrón, Peter Gärdenfors, and David Makinson. On the logic of theory change : Partial meet contraction and revision functions. Journal of symbolic Logic, 50:510–530, 1985. [De Giacomo et al., 2007] Giuseppe De Giacomo, Maurizio Lenzerini, Antonella Poggi, and Riccardo Rosati. On the approximation of instance level update and erasure in description logics. In Proceedings of the Twenty-Second AAAI Conference on Artificial Intelligence, July 22-26, 2007, Vancouver, British Columbia, Canada, pages 403–408, 2007. [Flouris et al., 2005] Giorgos Flouris, Dimitris Plexousakis, and Grigoris Antoniou. On applying the agm theory to dls and owl. In In 4th International Semantic Web Conference (ISWC, pages 216–231, 2005. [Le Duc et al., 2013] Chan Le Duc, Myriam Lamolle, and Olivier Curé. A decision procedure for SHOIQ with transitive closure of roles. In The Semantic Web - ISWC 2013 - 12th Interna- tional Semantic Web Conference, Sydney, NSW, Australia, October 21-25, 2013, Proceedings, Part I, pages 264–279, 2013. [Qi and Yang, 2008] Guilin Qi and Fangkai Yang. A survey of revision approaches in description logics. In Diego Calvanese and Georg Lausen, editors, Web Reasoning and Rule Systems, volume 5341 of Lecture Notes in Computer Science, pages 74–88. Springer Berlin Heidelberg, 2008. [Qi et al., 2006] Guilin Qi, Weiru Liu, and David A. Bell. Knowledge base revision in descrip- tion logics. In European Conference on Logics in Artificial Inteligence, pages 386–398, 2006.