A Transformation Approach for Classifying ALCHI (D) Ontologies with a Consequence-based ALCH Reasoner

Abstract

Consequence-based techniques have been developed to provide e cient classi cation for less expressive languages. Ontology transformation techniques are often used to approximate axioms in a more expressive language by axioms in a less expressive language. In this paper, we present an approach to use a fast consequence-based ALCH reasoner to classify an ALCHI(D) ontology with a subset of OWL 2 datatypes and facets. We transform datatype and inverse role axioms into ALCH axioms. The transformed ontology preserves sound and complete classi cation w.r.t the original ontology. The proposed approach has been implemented in the prototype WSClassi er which exhibits the high performance of consequence reasoning. The experiments show that for classifying large and highly cyclic ALCHI(D) ontologies, WSClassi er's performance is signi cantly faster than tableau-based reasoners.

Introduction

Ontology classi cation is the foundation of many ontology reasoning tasks. Recently, consequence-based techniques have been developed to provide e cient classi cation for sublanguages of OWL 2 DL pro le, e.g. E L++ [ 2,3,8 ], HornSHIQ [ 7 ], E L?(D) [ 9 ], ALCH [ 13 ]. There have been some approaches to use existing consequence-based reasoners to classify more expressive ontologies, like MORe [ 1 ]. In this paper, we propose an approach to use a consequence-based ALCH reasoner to classify an ALCHI(D) ontology by transforming it into an ALCH ontology with soundness and completeness preserved. The purpose of the approach is to extend the expressiveness of the existing consequence-based reasoner without changing its complex inference rules and implementation. All proofs and further technical details can be found in our technical report [ 15 ].

Ontology transformation is often accomplished by approximating non-Horn ontologies/theories by Horn replacements [ 12,11,16 ]. These approximations can be used to optimize reasoning by exploiting more e cient inference for Horn ontologies/theories. The approximation O0 in Ren et al. [ 11 ] is a lower bound of the original ontology O, i.e. O0 entails no more subsumptions than O does. In contrast, approximation in Zhou et al. [ 16 ] provides an upper bound. Kautz et al. [ 12 ] computes both upper and lower bounds of propositional logic theories. Another approach preserves both soundness and completeness of classi cation results such as the elimination of transitive roles in Kazakov [ 7 ]. Our work of this paper is of the second kind. We classify an ALCHI(D) ontology O in two stages: (1) transform O into an ALCHI ontology OD s.t. O j= A v B i OD j= A v B; (2) transform OD into an ALCH ontology OID s.t. OID j= A v B i OD j= A v B. We use these approaches to implement a reasoner called WSClassi er which transforms an ALCHI(D) ontology into an ALCH ontology and classi es it with a fast consequence ALCH reasoner ConDOR [ 13 ]. WSClassi er is signi cantly faster than tableau-based reasoners on large and highly cyclic ontologies.

In our previous work [ 14 ] we approximated an ALCHOI ontology by an ALCH ontology which was then classi ed by a hybrid of consequence- and tableau-based reasoners. Unlike [ 14 ], in this paper we claim completeness for I's transformation. Calvanese et al. [ 4 ] introduces a general approach to eliminate inverse roles and functional restrictions from ALCF I to ALC. For eliminating I, the approach needs to add one axiom for each inverse role and each concept. So the number of axioms added can be very large. Ding et al. [ 6 ] introduces a new mapping from ALCI to ALC and further extends it to a mapping from SHI to SH in [ 5 ]. The approach allows tableau-based decision procedures to use some caching techniques and improve the reasoning performance in practice. Both approaches in [ 4,5 ] preserve the soundness and completeness of inference after elimination of I. Our approach is similar to the one in [ 6,5 ]. However, the NNF normalized form in [ 6,5 ] in which > appears in the left side of all axioms will dramatically degrade the performance of our consequence-based ALCH reasoner. Thus we eliminate the inverse role based on our own normalized form and our approach is more suitable for consequence-based reasoners. 2

Preliminary

Due to space limitation, we only list the most necessary syntax and semantics of ALCHI(D) in the paper, the complete illustration can be found in our Technical Report [ 15 ]. The syntax of ALCHI(D) uses atomic concepts NC , atomic roles NR and features NF . We use A; B for atomic concepts, C; D for concepts, r; s for atomic roles, R; S for roles, F; G for features. The parameter D de nes a datatype map D = (NDT ; NLS ; NF S ; D), where: (1) NDT is a set of datatype names; (2) NLS is a function assigning to each d 2 NDT a set of constants NLS (d); (3) NF S is a function assigning to each d 2 NDT a set of facets NF S (d), each f 2 NF S (d) has the form (pf ; v); (4) D is a function assigning a datatype interpretation dD to each d 2 NDT called the value space of d, a data value vD 2 dD for each v 2 NLS (d), and a facet interpretation f D for each f 2 Sd2NDT NF S (d). Since one facet may be shared by multiple datatypes, we de ne its interpretation as containing subsets of all the relevant datatypes. >D, d, d[f ] or fvg are basic forms of data ranges, which we call atomic data ranges. A data range dr is de ned recursively using u, t, and :. A role R is either an atomic role r or inverse role r . Semantics of ALCHI(D) is de ned via an interpretation I = ( I ; D; I ; D). I and D are disjoint non-empty sets called object domain and data domain. dD D for each d 2 NDT . I assigns a set AI I to each A 2 NC , a relation rI I I to each r 2 NR and a relation F I I D to each F 2 NF . F I (x) = fv j (x; v) 2 F I g. D interprets data ranges and concepts, as shown in Table 1. We write NDT (O) and ADR(O) for all datatypes and atomic data ranges in O. And ADRd(O) denotes the subset of ADR(O) in datatype d, i.e. of the form d, d[f ] or fvg where v 2 NLS (d). In this section we introduce how we transform an ALCHI(D) ontology O into an ALCHI ontology OD such that O j= A v B i OD j= A v B. We assume all the datatypes in D are disjoint, as do Motik et al [ 10 ]. We apply our approach to some commonly used datatypes: (1) real with facets rational, decimal, integer, >a, a, <a and a; (2) strings with equal value; (3) boolean values.

Our basic idea to produce OD from O is to encode features into roles and data ranges into concepts, and then add extra axioms to preserve the subsumptions between atomic concepts in NC (O). Table 2 gives the de nition of encoding function ' over atomic elements in O, where Ad; Af ; Av are fresh concepts and RF is a fresh role. ' over complex data ranges, roles, concepts and axioms are de ned recursively using corresponding constructors. It is easy to prove that classi cation of '(O) = f'( ) j 2 Og is sound w.r.t. O (proof see [ 15 ]). In order to preserve classi cation completeness, extra axioms need to be added to '(O) to get OD. Algorithm 1 shows how OD is computed. In the procedure we use two functions normalized and getAxiomsd for each datatype d 2 NDT (O). normalized rewrites data ranges d[f ] into normalized forms to reduce the kinds of facets used. getAxiomsd produces a set of ALCHI axioms Od+ to be included into OD. Details will be explained later for the datatypes and facets supported. In order to preserve classi cation completeness w.r.t. O, getAxiomsd must generate axioms explicitly showing the relationships implicit among data ranges before encoding, i.e., the data-range-relationship-preserving property: for any ar1; : : : ; arn; ar10; : : : ; arm0 2 ADRd(O), if (din=1 ari) u (djm=1 :arj0 ) D = ;, then (din=1 '(ari))u(dm

j=1 :'(arj0 )) is unsatis able in Od+ = getAxiomsd(ADRd(O); ').

We prove this condition is su cient for completeness in [ 15 ].

For boolean type, we do not have any facets, so normalized does nothing. Since the only atomic data ranges are xsd : boolean, ftrueg and ff alseg, getAxiomsd only needs to return two axioms '(xsd : boolean) '(ftrueg) t '(ff alseg) and '(ftrueg) u '(ff alseg) v ?. For string type, currently we do not support any facets, so normalized does nothing either. Atomic data ranges are ei

Algorithm 1: Datatype Transformation

Input: An ALCHI(D) ontology O

Output: An ALCHI ontology OD with the same classi cation result as O 1 foreach d 2 NDT (O) do 2 foreach adr 2 ADRd(O) do 3 Replace adr with normalized(adr) in O; 4 Create an encoding ' for O and initialize OD with '(O); 5 foreach d1; d2 2 NDT (O); d1 6= d2 do OD OD [ f'(d1) u '(d2) v ?g; 6 foreach d 2 NDT (O) do OD OD [ getAxiomsd(ADRd(O), '); 7 return OD; ther xsd : string or of the form fcg, where c is a constant. We need to add '(fcg) v '(xsd : string) for each fcg 2 ADRR(O), as well as pairwise disjoint axioms for all such '(fcg). Numeric datatypes are the most commonly used datatypes in ontologies. Here we discuss the implementation for owl : real, which we denote by R. owl : rational, xsd : decimal and xsd : integer are treated as facets rat, dec and int of R, respectively. Comparison facets of the forms >a, <a, a, a are supported. For normalized with input ar, we need: (1) if adr = R[f ], transform it to equivalent data ranges using only facets of the form >a, e.g. R[<a] = R u :(R[>a] t fag); (2) replace any constant a used in ar with a normal form, so that any constants having the same interpretation becomes the same after normalization, e.g. integer constants +3 and 3 are both interpreted as real number 3, so they are normalized into the same form "3"^^xsd : integer. Algorithm 2 gives the details of getAxiomsR for real numbers. For boolean and string, it is obvious that the corresponding getAxiomsd has data-range-relationship-preserving property. For getAxiomsR, we prove this property in [ 15 ]. So if O j= A v B, then OD j= A v B. 4

Transformation for Inverse Roles

In this section, we discuss how we transform an ALCHI ontology OD into an ALCH ontology OID, such that OD j= A v B i OID j= A v B(proof see [ 15 ]). Algorithm 3 shows the details of transformation for inverse roles. In the procedure Invr contains the set of atomic roles which are inverses of r. Line 1 initializes OID with ALCH axioms in OD. Lines 2 to 6 initializes Invr and put all r where Invr 6= ; into RolesToBeProcessed. Lines 7 to 16 processes each role in RolesToBeProcessed and adds axioms into OID to address the e ect of inverse role axioms. Detail explanations of Algorithm 3 are in our technical report [ 15 ]. 5

Experiment and Conclusion

In experiments we compare the runtime of our WSClassi er with all other available ALCHI(D) reasoners HermiT, Fact++ and Pellet, which all happen to be tableau-based reasoners. We use all large and highly cyclic ontologies we can Algorithm 2: getAxiomsR for R

Input: A set of atomic data ranges ADRR(O) of type R, encoding function ' +

Output: A set of axioms OR 1 OR+ ;; 2 foreach fvg 2 ADRR(O) do 3 if R[int] 2 ADRR(O) and vD 2 (R[int])D then add '(fvg) v '(int) to OR+; 4 if R[dec] 2 ADRR(O) and vD 2 (R[dec])D then add '(fvg) v '(dec) to OR+; 5 if R[rat] 2 ADRR(O) and vD 2 (R[rat])D then add '(fvg) v '(rat) to OR+; + 6 if R[int]; R[dec] 2 ADRR(O) then add '(int) v '(dec) to OR ; + 7 if R[int]; R[rat] 2 ADRR(O) then add '(int) v '(rat) to OR ; + 8 if R[dec]; R[rat] 2 ADRR(O) then add '(dec) v '(rat) to OR ; 9 Put all R[>a] 2 ADRR(O) in fArray with ascending order of a; 10 foreach pair of adjacent elements R[>a] and R[>b] (a < b) in fArray do 11 add '(>b) v '(>a) to OR+; 12 if R[int] 2 ADRR(O) then 13 M ffaiggin=1, where a1; : : : ; an are all integer constants in (a; b]; 14 if M ADRR(O) then 15 add '(int) u '(>a) u :'(>b) u (din=1 :'(faig)) v ? to OR+; 16 Let N be all v such that fvg 2 ADRR(O) and vD 2 (a; b]; 17 foreach v 2 N do add '(fvg) v '(>a), '(fvg) u '(>b) v ? to OR+; 18 foreach v1; v2 2 N; v1 6= v2 do add '(fv1g) u '(fv2g) v ? to OR+; + 19 return OR ; access to. FMA-constitutionalPartForNS(FMA-C) is the only large and highly cyclic ontology that contains ALCHI(D) constructors. We remove seven axioms using xsd : f loat. For Full-Galen which language is ALEHIF + without \D", we introduce some new data type axioms by converting some axioms using roles hasNumber and hasMagnitude into axioms with new features hasNumberDT and hasMagnitudeDT. Some concepts which should be modeled as data ranges are also converted to data ranges. Wine is a small but cyclic ontology. We also include two commonly used ontologies ACGT and OBI which are not highly cyclic. For Wine, ACGT and OBI, we change xsd:int, xsd:positiveInteger, xsd:nonNegativeInteger to xsd:integer, xsd: oat to owl:rational, and remove xsd:dateTime if applicable. For all the ontologies, we reduce their language to ALCHI(D). The ontologies are available from our website.1.The experiments were conducted on a laptop with Intel Core i7-2670QM 2.20GHz quad core CPU and 16GB RAM. We set the Java heap space to 12GB and the time limit to 24 hours.

Table 3 summarizes the result. HermiT is set to con guration with simple core blocking and individual reuse. WSClassi er is signi cantly faster than the tableau-based reasoners on the three highly cyclic large ontologies Galen-Heart, Full-Galen and FMA-C. ACGT is not highly cyclic, but WSClassi er is still faster. For the other two ontologies where WSClassi er is not the fastest, Wine is cyclic but small, OBI is not highly cyclic. The classi cation time for them on 1 http://isel.cs.unb.ca/~wsong/ORE2013WSClassifierOntologies.zip

Algorithm 3: Transformation for inverse roles

Input: Normalized ontology ALCHI ontology OD

Output: An ALCH ontology OID having the same classi cation result as OD 1 Initialize OID with all ALCH axioms in OD, excluding inverse role axioms; 2 foreach r 2 NR(O) do Invr ; ; 3 RolesToBeProcessed ;; 4 foreach r0 = r 2 OD do 5 Invr Invr [ fr0g; Invr0 Invr0 [ frg; 6 RolesToBeProcessed RolesToBeProcessed [ fr; r0g; 7 while RolesToBeProcessed 6= ; do 8 remove a role r from RolesToBeProcessed and pick a role r0 from Invr; 9 foreach r 2 Invr where r is not r0 do add r0 r to OID; 10 foreach r v s 2 OD do 11 if Invs = ; then 12 add a fresh atomic role s0 to Invs; 13 RolesToBeProcessed RolesToBeProcessed [ fsg; 14 pick a role s0 from Invs and add r0 v s0 to OID; 15 foreach 9r:A v B 2 OD do add A v 8r0:B to OID; 16 foreach A v 8r:B 2 OD do add 9r0:A v B to OID; 17 return OID all reasoners are signi cantly shorter comparing with the time on large highly cyclic ontologies. Then WSClassi er took a larger percentage of time on the overhead to transmit the ontology to and from ConDOR. We have transformed some commonly used OWL 2 datatypes and facets and inverse role axioms in an ALCHI(D) ontology to ALCH and classi ed it on an ALCH reasoner with soundness and completeness of classi cation preserved. WSClassi er greatly outperforms tableau-based reasoners when the ontologies are large and highly cyclic. Future work includes extension to other data types and facets, and further optimization, e.g. adapting the idea of Magka et al. [ 9 ] to WSClassi er to distinguish positive and negative occurrences of data ranges, in order to reduce the number of axioms to be added.

References

1. Armas Romero , A. , Cuenca Grau , B. , Horrocks , I.: MORe: Modular combination of OWL reasoners for ontology classi cation . In: Proc. of ISWC . pp. 1 { 16 ( 2012 )

2. Baader , F. , Brandt , S. , Lutz , C. : Pushing the EL envelope . In: IJCAI . pp. 364 { 369 ( 2005 )

3. Baader , F. , Lutz , C. : Pushing the EL envelope further . In: Proc. of OWLED ( 2008 )

4. Calvanese , D. , De Giacomo , G. , Rosati , R.: A note on encoding inverse roles and functional restrictions in alc knowledge bases . In: Proc. of the 5th Int. Description Logic Workshop . DL. vol. 98 , pp. 11 { 20 ( 1998 )

5. Ding , Y. : Tableau-based reasoning for description logics with inverse roles and number restrictions . http://users.encs.concordia.ca/~haarslev/students/ Yu_Ding.pdf ( 2008 )

6. Ding , Y. , Haarslev , V. , Wu , J.: A new mapping from alci to alc . In: Proc. DL-2007. CEUR Workshop Proceedings . vol. 250 . Citeseer ( 2007 )

7. Kazakov , Y. : Consequence-driven reasoning for Horn SHIQ ontologies . In: Proc. of IJCAI . pp. 2040 { 2045 ( 2009 )

8. Kazakov , Y. , Krotzsch, M. , Simanc k , F.: Concurrent classi cation of EL ontologies . In: Proc. of ISWC . pp. 305 { 320 ( 2011 )

9. Magka , D. , Kazakov , Y. , Horrocks , I. : Tractable extensions of the description logic EL with numerical datatypes . J. Automated Reasoning 47 ( 4 ), 427 { 450 ( 2011 )

10. Motik , B. , Horrocks , I. : Owl datatypes: Design and implementation . In: International Semantic Web Conference. pp. 307 { 322 ( 2008 )

11. Ren , Y. , Pan , J.Z. , Zhao , Y. : Soundness preserving approximation for TBox reasoning . In: Proc. of AAAI ( 2010 )

12. Selman , B. , Kautz , H.: Knowledge compilation and theory approximation . J. ACM 43 ( 2 ), 193 { 224 ( 1996 )

13. Simanc k , F., Kazakov , Y. , Horrocks , I. : Consequence-based reasoning beyond Horn ontologies . In: Proc. of IJCAI . pp. 1093 { 1098 ( 2011 )

14. Song , W. , Spencer , B. , Du , W.: WSReasoner: A prototype hybrid reasoner for ALCHOI ontology classi cation using a weakening and strengthening approach . In: Proc. of the 1st Int. OWL Reasoner Evaluation Workshop ( 2012 )

15. Song , W. , Spencer , B. , Du , W. : Technical report of a transformation approach for classifying ALCHI(D) ontologies with a consequence-based ALCH reasoner . Tech. rep. ( 2013 ), http://www.cs.unb.ca/tech-reports/documents/TR13-225.pdf

16. Zhou , Y. , Cuenca Grau , B. , Horrocks , I.: E cient upper bound computation of query answers in expressive description logics . In: Proc. of DL ( 2012 )