=Paper=
{{Paper
|id=None
|storemode=property
|title=A Transformation Approach for Classifying ALCHI(D) Ontologies with a Consequence-based ALCH Reasoner
|pdfUrl=https://ceur-ws.org/Vol-1015/paper_4.pdf
|volume=Vol-1015
|dblpUrl=https://dblp.org/rec/conf/ore/SongSD13
}}
==A Transformation Approach for Classifying ALCHI(D) Ontologies with a Consequence-based ALCH Reasoner==
https://ceur-ws.org/Vol-1015/paper_4.pdf
A Transformation Approach for Classifying
ALCHI(D) Ontologies with a
Consequence-based ALCH Reasoner
Weihong Song, Bruce Spencer, and Weichang Du
Faculty of Computer Science, University of New Brunswick, Fredericton, Canada
Abstract. Consequence-based techniques have been developed to pro-
vide efficient classification for less expressive languages. Ontology trans-
formation techniques are often used to approximate axioms in a more ex-
pressive 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 axiom-
s. The transformed ontology preserves sound and complete classification
w.r.t the original ontology. The proposed approach has been implement-
ed in the prototype WSClassifier which exhibits the high performance of
consequence reasoning. The experiments show that for classifying large
and highly cyclic ALCHI(D) ontologies, WSClassifier’s performance is
significantly faster than tableau-based reasoners.
1 Introduction
Ontology classification is the foundation of many ontology reasoning tasks. Re-
cently, consequence-based techniques have been developed to provide efficient
classification for sublanguages of OWL 2 DL profile, e.g. EL++ [2,3,8], Horn-
SHIQ [7], EL⊥ (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 efficient 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 classification
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 |= A v B iff OD |= A v B;
2 Weihong Song, Bruce Spencer, and Weichang Du
− − − −
(2) transform OD into an ALCH ontology OID s.t. OID |= A v B iff OD |= A v
B. We use these approaches to implement a reasoner called WSClassifier which
transforms an ALCHI(D) ontology into an ALCH ontology and classifies it with
a fast consequence ALCH reasoner ConDOR [13]. WSClassifier is significantly
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 classified 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 rea-
soner. 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 defines 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 ∈ NDT a set of constants NLS (d); (3) NF S
is a function assigning to each d ∈ NDT a set of facets NF S (d), each f ∈ NF S (d)
has the form (pf , v); (4) ·D is a function assigning a datatype interpretation dD
D D
to each d ∈ NDT called the value space of d, a data value S v ∈ d for each
D
v ∈ NLS (d), and a facet interpretation f for each f ∈ d∈NDT NF S (d). Since
one facet may be shared by multiple datatypes, we define its interpretation as
containing subsets of all the relevant datatypes. >D , d, d[f ] or {v} are basic
forms of data ranges, which we call atomic data ranges. A data range dr is
defined recursively using u, t, and ¬. A role R is either an atomic role r or
inverse role r− . Semantics of ALCHI(D) is defined 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 ∈ NDT . ·I assigns a set AI ⊆ ∆I to each
A ∈ NC , a relation rI ⊆ ∆I × ∆I to each r ∈ NR and a relation F I ⊆ ∆I × ∆D
to each F ∈ NF . F I (x) = {v | (x, v) ∈ F I }. ·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 {v} where v ∈ NLS (d).
ALCHI(D) Ontology Classification 3
Table 1. Part of Model Theoretic Semantics of ALCHI(D)
Semantics of Data Ranges
(>D )D = ∆D {v}D = {v D } (dr1 u dr2 )D = dr1D ∩ dr2D
(d[f ])D = dD ∩ f D (¬dr)D = ∆D \ drD (dr1 t dr2 )D = dr1D ∪ dr2D
Semantics of Concepts, Roles and Axioms
F v G ⇒ F I ⊆ GI (∃F.dr)I = {x | F I (x) ∩ drD 6= ∅} (∀F.dr)I = {x | F I (x) ⊆ drD }
3 Transformation for Datatypes
In this section we introduce how we transform an ALCHI(D) ontology O into
− −
an ALCHI ontology OD such that O |= A v B iff OD |= 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 , D ) = > ϕ(d[f ]) = Ad u Af ϕ(>) = > ϕ(A) = A
ϕ(d) = Ad ϕ({v}) = Av ϕ(R) = R ϕ(F ) = RF
we use two functions normalized and getAxiomsd for each datatype d ∈ 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 classification completeness w.r.t. O, getAxiomsd must gener-
ate axioms explicitly showing the relationships implicit among data ranges before
encoding, i.e., the data-range-relationship-preserving property: for any
dn dm D
ar1 , . . . , arn , ar10 , . . . , arm
0
∈ ADRd (O), if ( i=1 ari ) u ( j=1 ¬arj0 ) = ∅, then
dn dm
( i=1 ϕ(ari ))u( j=1 ¬ϕ(arj0 )) is unsatisfiable in Od+ = getAxiomsd (ADRd (O), ϕ).
We prove this condition is sufficient 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, {true} and {f alse}, getAxiomsd
only needs to return two axioms ϕ(xsd : boolean) ≡ ϕ({true}) t ϕ({f alse})
and ϕ({true}) u ϕ({f alse}) v ⊥. For string type, currently we do not sup-
port any facets, so normalized does nothing either. Atomic data ranges are ei-
4 Weihong Song, Bruce Spencer, and Weichang Du
Algorithm 1: Datatype Transformation
Input: An ALCHI(D) ontology O
−
Output: An ALCHI ontology OD with the same classification result as O
1 foreach d ∈ NDT (O) do
2 foreach adr ∈ 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 ∈ NDT (O), d1 6= d2 do OD ← OD ∪ {ϕ(d1 ) u ϕ(d2 ) v ⊥};
− −
6 foreach d ∈ NDT (O) do OD ← OD ∪ getAxiomsd (ADRd (O), ϕ);
−
7 return OD ;
ther xsd : string or of the form {c}, where c is a constant. We need to add
ϕ({c}) v ϕ(xsd : string) for each {c} ∈ ADRR (O), as well as pairwise disjoin-
t axioms for all such ϕ({c}). 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 form-
s >a , a , e.g. R[a ] t {a}); (2) replace any constant a used
in ar with a normal form, so that any constants having the same interpreta-
tion 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 num-
bers. 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 |= A v B, then OD |= 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 |= A v B iff OID |= 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 effect 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 WSClassifier with all other avail-
able 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
ALCHI(D) Ontology Classification 5
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 {v} ∈ ADRR (O) do
3 if R[int] ∈ ADRR (O) and v D ∈ (R[int])D then add ϕ({v}) v ϕ(int) to OR+ ;
4 if R[dec] ∈ ADRR (O) and v D ∈ (R[dec])D then add ϕ({v}) v ϕ(dec) to OR+ ;
5 if R[rat] ∈ ADRR (O) and v D ∈ (R[rat])D then add ϕ({v}) v ϕ(rat) to OR+ ;
+
6 if R[int], R[dec] ∈ ADRR (O) then add ϕ(int) v ϕ(dec) to OR ;
+
7 if R[int], R[rat] ∈ ADRR (O) then add ϕ(int) v ϕ(rat) to OR ;
+
8 if R[dec], R[rat] ∈ ADRR (O) then add ϕ(dec) v ϕ(rat) to OR ;
9 Put all R[>a ] ∈ 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] ∈ ADRR (O) then
13 M ← {{ai }}n i=1 , where a1 , . . . , an are all integer constants in (a, b];
14 if M ⊆ ADRR (O) then
add ϕ(int) u ϕ(>a ) u ¬ϕ(>b ) u ( n +
d
15 i=1 ¬ϕ({ai })) v ⊥ to OR ;
16 Let N be all v such that {v} ∈ ADRR (O) and v D ∈ (a, b];
17 foreach v ∈ N do add ϕ({v}) v ϕ(>a ), ϕ({v}) u ϕ(>b ) v ⊥ to OR+ ;
18 foreach v1 , v2 ∈ N, v1 6= v2 do add ϕ({v1 }) u ϕ({v2 }) 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:float 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 configuration with simple
core blocking and individual reuse. WSClassifier is significantly 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 WSClassifier is still
faster. For the other two ontologies where WSClassifier is not the fastest, Wine
is cyclic but small, OBI is not highly cyclic. The classification time for them on
1
http://isel.cs.unb.ca/~wsong/ORE2013WSClassifierOntologies.zip
6 Weihong Song, Bruce Spencer, and Weichang Du
Algorithm 3: Transformation for inverse roles
−
Input: Normalized ontology ALCHI ontology OD
− −
Output: An ALCH ontology OID having the same classification result as OD
− −
1 Initialize OID with all ALCH axioms in OD , excluding inverse role axioms;
2 foreach r ∈ NR (O) do Invr ← ∅ ;
3 RolesToBeProcessed ← ∅;
0 − −
4 foreach r = r ∈ OD do
0
5 Invr ← Invr ∪ {r }; Invr0 ← Invr0 ∪ {r};
6 RolesToBeProcessed ← RolesToBeProcessed ∪ {r, r0 };
7 while RolesToBeProcessed 6= ∅ do
8 remove a role r from RolesToBeProcessed and pick a role r0 from Invr ;
−
9 foreach r∗ ∈ Invr where r∗ is not r0 do add r0 ≡ r∗ to OID ;
−
10 foreach r v s ∈ OD do
11 if Invs = ∅ then
12 add a fresh atomic role s0 to Invs ;
13 RolesToBeProcessed ← RolesToBeProcessed ∪ {s};
−
14 pick a role s0 from Invs and add r0 v s0 to OID ;
− 0 −
15 foreach ∃r.A v B ∈ OD do add A v ∀r .B to OID ;
− −
16 foreach A v ∀r.B ∈ OD do add ∃r0 .A v B to OID ;
−
17 return OID
all reasoners are significantly shorter comparing with the time on large highly
cyclic ontologies. Then WSClassifier took a larger percentage of time on the
overhead to transmit the ontology to and from ConDOR.
Table 3. Comparison of classification performance of ALCHI(D) ontologies
HermiT Pellet FaCT++ WSClassifier
Wine 1.160 sec 0.430 sec 0.005 sec 0.400 sec
ACGT 9.603 sec 2.955 sec * 1.945 sec
OBI 3.166 sec 45.261 sec * 8.835 sec
Galen-Heart 123.628 sec – – 2.779 sec
Full-Galen – – – 16.774 sec
FMA-C – – – 32.74 sec
Note: “–”: out of time or memory “*”: some datatypes are not supported
We have transformed some commonly used OWL 2 datatypes and facets and
inverse role axioms in an ALCHI(D) ontology to ALCH and classified it on
an ALCH reasoner with soundness and completeness of classification preserved.
WSClassifier 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 WSClassifier to distinguish positive and negative occurrences of data ranges,
in order to reduce the number of axioms to be added.
ALCHI(D) Ontology Classification 7
References
1. Armas Romero, A., Cuenca Grau, B., Horrocks, I.: MORe: Modular combination
of OWL reasoners for ontology classification. 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., Krötzsch, M., Simanc̆ı́k, F.: Concurrent classification of EL ontolo-
gies. 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: Interna-
tional Semantic Web Conference. pp. 307–322 (2008)
11. Ren, Y., Pan, J.Z., Zhao, Y.: Soundness preserving approximation for TBox rea-
soning. 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 classification 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.: Efficient upper bound computation of
query answers in expressive description logics. In: Proc. of DL (2012)