TBox reasoning in description logics is hard. For example, reasoning in SROIQ (i.e. OWL2-DL) is N2ExpTime-complete; even with R, a fragment of SROIQ supporting ALC GCIs and role chains, the complexity of reasoning is 2ExpTime-hard. Although various optimisation techniques have been applied, existing tableau-based DL reasoners are still ine cient in dealing with arbitrary GCIs especially when complex role chains present. In this paper, we present a soundness preserving approximation for TBox reasoning in R. The main idea is to convert R ontologies to EL+ with an additional complement table maintaining the complementary relations between named concepts. Since existing benchmarks do not focus on complex GCIs and RIs, we propose a new set of testing ontologies for TBox reasoning in R and our preliminary evaluation shows that a naive implementation of our complement-integrated TBox reasoning algorithm outperforms existing reasoners on most of these ontologies.
The family of the description logics (DL) provides a wide range of formalisms
with a trade-o between expressiveness and computational di culty. TBox
reasoning in description logics is hard; e.g., DL SROIQ [
There are mainly two approaches to providing e cient reasoning services.
The first approach investigates sophisticated optimisation techniques for
tableaux algorithms [
The second approach is based on transformations. Approximations can be
seen as some useful transformations. Selman and Kautz [
We notice that less expressive DLs, such as EL+ can deal with large amount
of GCIs of restricted patterns very e ciently and its inference patterns can be
partially generalised to more expressive DLs by syntactic manipulation of TBox.
In this paper, we present a soundness preserving syntactic approximation for
TBox reasoning services of the DL R. More precisely, we syntactically
approximate an R TBox to EL+ [
We implemented a prototype of our approach called REL and evaluate its performance on real world benchmarking ontology and a set of automated generated R TBox. Preliminary evaluations show that (1) REL outperforms tableaux based reasoners such as Pellet and FaCT++, and (2) its soundness preserving approximation service provides rather complete results, i.e. with high recall.
The rest of the paper is organised as follows: in Section 2 we present our approximation approach with examples; in Section 3 we present a soundnessguaranteed TBox reasoning algorithm for the approximation ontologies; in Section 4 an evaluation of our prototypical implementation is conducted to compare with existing DL reasoners; in Section 5 we summarise our findings and highlight the potential of this study. 2
In this section, we present our approximation approach by first showing approximation principles with an example, and then formalising these principles into algorithms. 2.1
R supports two types of TBox axioms: general concept inclusion (GCIs) and complex role inclusion (RIs). Because RIs are the same in R and EL+, and they are independent from GCIs, we preserve all the RIs in the approximation.
The approximation of the GCIs is mainly about the approximation of concept expressions. In R, a concept is inductively defined by constructs as follows:
C := >j?jAj:CjC u DjC t Dj9r:Cj8r:C while in EL+, a concept is inductively defined by constructs as:
C := >jAjC u Dj9r:C where A is an atomic concept, r is a role name.
Intuitively, an R construct belongs to one of the following sets: f>, ?g, fA, :Cg, fC u D, C t Dg, f9r:Cg, f8r:Cg. It’s easy to observe that the former construct in each set is EL+-compatible, and the latter is equivalent to some negation of the former, which means for an arbitrary R concept expression, either itself or its complement can be composed by legal EL+ constructs. So we can represent non-EL+ part by replacing its appearance with a concept name and preserve its semantics by adding axioms defining its complement. From these observations we generalise our principles of approximation as follows: 1. Representing non-EL+ parts with new concept names. And, particularly, using a symbol y to represent the unique approximation of ?. 2. Maintaining the semantics of non-EL+ concepts by definitions of their complements. 3. Using an additional complement table CT to maintain the complementary relations between concept names. 4. Preserving all the RIs. 5. Asserting additional subsumptions in reasoning to recover the semantics of approximated concept expressions.
Example 1. T = fKoala v 8eat:EucalyptLeave, EucalyptLeave v VegetarianFood, 8eat:VegetarianFood v Herbivoreg
Following principle 1, we represent non-EL+ concepts 8eat:EucalyptLeave and 8eat:VegetarianFood by new names eatEucalyptLeave and eatVegetarianFood, respectively. Following principle 2, we define neatEucalyptLeave 9eat:nEucalyptLeave and neatVegetarianFood 9eat:nVegetarianFood to represent the complements of eatEucalyptLeave and eatVegetarianFood respectively. Then recursively, we introduce nEucalyptLeave and nVegetarianFood to represent non-EL+ concepts :EucalyptLeave and :VegetarianFood respectively. Thus the TBox becomes:
T 0 = featVegetarianFood v Herbivore, Koala v eatEucalyptLeave, EucalyptLeave v VegetarianFood, neatEucalyptLeave 9eat:nEucalyptLeave, neatVegetarianFood 9eat:nVegetarianFoodg
Following principle 3, we build
CT = f(eatEucalyptLeave, neatEucalyptLeave), (EucalyptLeave, nEucalyptLeave), (eatVegetarianFood, neatVegetarianFood), (VegetarianFood, nVegetarianFood)g
Following principle 5, in such a knowledge base, reasoning can infer Koala v Herbivore as follows:
EucalyptLeave v VegetarianFood ! nVegetarianFood v nEucalyptLeave ! neatVegetarianFood v neatEucalyptLeave ! eatEucalyptLeave v eatVegetarianFood ! Koala v Herbivore. 2.2
Given an R TBox T , we first generate a set S(T ) of concept expressions appearing in T as follows: 1. Initialise S(T ) by an f>g. 2. If C is refereed in T, then add C into S(T ). 3. For each C 2 S(T ), add :C into S(T ). 4. For each C 2 S(T ), if C is a conjunction (disjunction), add all its conjuncts (disjuncts) into S(T ); if C is a existential (universal) restriction, add its filler into S(T ). 5. Go back to 3 and repeat until no more changes can be made.
We then assign names to these concepts by a function n which assigns each atomic concept in S(T ) (including >) to itself, and each complex concept expression a unique name that does not appear in S(T ).
We further define these names by a function d which assigns each conjunction C Ci 2 S(T ) in S(T ) an axiom n(C) n(Ci), each existential restriction C 9r:D in S(T ) an axiom n(C) 9r:n(D).
With these names and definitions, we approximate T by Algorithm A-1. Its input is an R TBox T . Its output is (AS; CT) with AS an EL+ TBox and CT a set of paired concept names.
Algorithm A-1: OntoApprox(T ) 1: AS := ; 2: CT := ; 3: for each GCI C v D 2 T do 4: AS := AS [ fn(C) v n(D)g 5: end for 6: for each concept C 2 S(T ) do 7: CT := CTf(n(C); n(:C)); (n(:C); n(C))g 8: if C is a conjunction or existential restriction then 9: AS := AS [ fd(C)g 10: end if 11: end for 12: for each RI 2 T do 13: AS := AS [ f g 14: end for 15: normalise AS
This algorithm needs some explanation:
– By step-1 and step-2, AS and CT are initialised by empty sets.
– Step-4 rewrite the GCI with the named concepts.
– Step-7 updates CT.
– Step-8 and 9 maintain the definition of some concepts.
– Step-13 preserve all the RIs.
– Step-15 normalise AS as a classical EL+ ontology [
After the execution of A-1, AS is a normalised EL+ ontology. For every concept name A 2 CNAS, there exists B such that (A; B) 2 CT or (B; A) 2 CT. The complexity of A-1 is described by the following theorem: Theorem 1. Given an R TBox, T and N ;T the number of axioms in T , Algorithm A-1 will terminate in O(N ;T ) time in worst case.
Proof. Algorithm A-1 is linearly w.r.t. N ;T + jS(T )j, where jS(T )j is also linear w.r.t. N ;T .
We call the pair of (AS; CT) an ELC+ ontology to indicate that it is an EL+ ontology plus a complement table. As Algorithm A-1 shows, CT actually contains pairs of complementary named concepts. In the following, for each A appear in (AS; CT), we use CT(A) to represent the complement of A, i.e. (A; CT(A)) 2 CT.
Following Theorem 1 and the algorithms, we immediately know that jASj = O(N ;T ) and jCTj = O(N ;T ). Also, the approximation is additive, which means OntoApprox(T1 [ T2) = OntoApprox(T1) [ OntoApprox(T2) when any concept expression C has the same n(C) in these three approximations. 3
Soundness-preserving ELC+ TBox Reasoning We define entailment in an ELC+ ontology O = (AS; CT) as: O j= i AS [ fA :Bj(A; B) 2 CTg j= . Given CNAS the set of concept names, RNAS the set of role names, TBox reasoning in O yields, for each C 2 CNAS, a subsumer set S(C) = fXjO j= C v Xg, for each r 2 RNAS, a relation set R(r) = f(X; Y)jO j= X v 9r:Yg. 3.1
TBox reasoning in AS alone can be done by EL+ classification [
R6 realises axiom A u :A v ?. R7 asserts the reverse subsumption between concepts to supplement the absence of negation. R8 builds up the relations between conjuncts of a conjunction, e.g. A u B v ? implies A v :B. R9 deals with ? in existential restrictions, e.g. A v 9r:? implies A v ?.
We show the application of some rules with the following example:
The extra completion rules can be considered as introductions of new
normalised EL+ axioms in addition to AS. For example, R7 introduces a new
axiom CT(A) v CT(B) given known subsumption B v A. In the following we
propose an abstract algorithm which performs ELC+ TBox reasoning by realising
the completion rules with incremental reasoning of EL+ [
The algorithm computes these sets by processing corresponding axioms. For each name concept or existential restriction appearing on LHS of some axiom, the algorithm maintains a Oˆ set while for each name concept A, the algorithm maintains a FIFO queue(A).
Given a ELC+ ontology O = (AS; CT), the algorithm is initialised as follows: 1. 8C 2 CNAS; S(C) = fCg [ f>g, S(y) = CNAS; 2. 8r 2 RNAS; R(r) = ;; 3. if A1 u : : : u An v B 2 AS, then add A1; : : : ; Ai 1 u Ai+1; : : : ; An ! B into Oˆ (Ai); 4. if A u 9r:B 2 AS, then add 9r:B 2 into Oˆ(A); 5. if 9r:A u B 2 AS, then add B 2 into Oˆ(9r:A); 6. 8A 2 CNAS, queue(A)=Oˆ (A)[Oˆ (>);
Then, for all A 2 CNAS such that y< S(A), Algorithm A-2 is applied to all the entries X 2queue(A) until no more changes can be made.
Algorithm A-2: Process(A; X) 1: S(A) = S(A) [ fBg 2: queue(CT(B)) =queue(CT(B)) [ f! CT(A)g 3: Oˆ (CT(B)) =Oˆ (CT(B)) [ f! CT(A)g 4: if y< S(B) and CT(B) < S(A) and CT(A) < S(B) then 5: queue(A)=queue(A)[Oˆ (B) 6: for all concept names A0 and role name r with (A0; A) 2 R(r) do 7: queue(A0)=queue(A0)[Oˆ (9r:B) 8: end for 9: else 10: AddSubsumer(A,y) 11: for all concept names A0 and role name r with (A0; A) 2 R(r) do 12: AddSubsumer(A0,y)
– Step-2 and step-3 realise R7 with incremental reasoning. The application of R7 will always introduce a new axioms CT(B) v CT(A). Therefore we generate a new entry ! CT(A) for Oˆ(CT(B)) and initialise it into queue(CT(B)) accordingly. – Step-4 checks the condition of R6. Such a condition is important because once we realise that a concept is subsumed by y, we immediately know that it’s subsumed by any concept. – Step-10 to Step-13 realise R6 and R9
Post-processing should be done so that 8A 2 CNAS and y2 S(A), S(A) := CNAS and R(r) := R(r) [ f(A; B)g for all r 2 RNAS and B 2 CNAS. Also, A 2 S(>) should be subsumer of all the concept. The complexity of the reasoning is described by the following theorem: Theorem 2. Given an ELC+ ontology O = (AS; CT) the computation of the S sets an R sets for all its named concepts and named roles will terminate in polynomial time w.r.t. jCNAS [ RNASj.
Proof. The complexity of A-3 immediately follow the polynomial complexity of
EL+ classification [
Given the original ontology O1 and its approximation O2 = OntoApprox(O1), we can provide various reasoning services: – The entailment checking of an arbitrary GCI is realised as: O1 j= C v D if
O2 j= CApprox(C) v CApprox(D).
– The unsatisfiability of an concept expression C can be realised by the
entailment checking of O1 j=? C v ?, which will be reduced to entailment
checking O2 j=? CApprox(C) vy.
– The inconsistency checking of O1 can be realised by entailment checking
O1 j=? > v ?. Therefore, the problem of ontology consistency in O1 can also
be reduced to entailment checking O2 j=? > vy in O2.
– Incremental reasoning with a temporal ontology Otemp: O1 [ Otemp can be
approximated into OntoApprox(O1 [ Otemp), which is equivalent to O2 [
OntoApprox(Otemp), whose taxonomy can be computed incrementally by
adopting the incremental reasoning algorithm in [
The quality of the approximation and the reasoning is guaranteed by the following theorem: Theorem 3. Given an R ontology O1, approximate it into O2 with Algorithm A-1. For any A; B 2 CNO1 , O1 j= A v B if B 2 S(A) can be inferred from O2 by Algorithm A-2.
Proof (sketch): It is easy to see the approximation by Algorithm A-1 is an equivalent syntactic transformation, because it is reversible. The completion rules implemented by Algorithm A-2 are obviously soundness-guaranteed. Incompleteness Our extra completion rules process each axiom in AS individually. In Algorithm A-2 we also process each queue entry individually. This helps keeping the reasoning tractable but some information that can only be derived from interaction of multiple entries will be lost: Example 3. T = fA u :B v C; A u B v C; D v 9r::C; 9r:B v E; 9r::A v Eg
Obviously, we have T j= A v C and thus D v E. However, if we approximate it into (fX1 A u nB; X2 A u B; X3 9r:nC; X4 9r:nA; : : :g; f(B; nB); : : :g) and initialise Algorithm A-1, we will have queue(A) = fnB ! X1; B ! X2g. Obviously, B and nB are not subsumers of A thus we can’t further infer C 2 S(A).
This can be solved by resolution: nB ! X1 2 queue(A) implies A v f c(nB)tX1 thus A v B t C. similarly we have A v nB t C. Together we can infer A v C.
In order to further infer D v F. A new axiom 9r:(B t :A) 9r:B t 9r::A has to be added into T and approximated for incremental reasoning.
Although we can’t guarantee completeness, we will see in next section that the recall is high, at least for our benchmark ontologies.
We implement our approximation and reasoning algorithm as a functionality of our REL reasoner for EL+, which is a component of our TrOWL Tractable Reasoning infrastructure of OWL1.
To evaluate its performance, We compare REL with FaCT++ v1.2.3 and Pellet 2.0.0 rc5. The experiments are conducted in an environment of Microsoft Windows XP SP3 with 2.66 GHz CPU and 1G memory allocated to JVM 1.6.0.07.
In order to test its e ects on di cult TBox with complex GCIs, we create our own set of 16 R ontologies 2. In these ontologies, the size of any conjunction or disjunction is at most 5, the depth of a concept expression on the lhs or rhs of a GCI is at most 4. The domain and range of any role is a disjunction of depth at most 3. These ontologies are split into two sets, i.e. S1 and S2. In S1, ontologies have increasing number of concept names and GCIs. jRNj is fixed to 10, number of simple RIs and complex RIs are about 10. In S2, ontologies have increasing jRNj. jCNj is fixed to 20, number of GCIs is fixed to 30, number of RIs is increasing with the jRNj . The performance metrics for REL include approximation time, 1 http://trowl.eu/ 2 http://www.abdn.ac.uk/~csc303/benchmark/RBenchmarkTest.zip reasoning time and completeness. All the time are measured in seconds. To evaluate the completeness, we check the subsumption between each pair of named concepts and count the number of discovered subsumptions.
Pellet timed-out or clashed in all the 16 ontologies. Results of REL and FaCT++ are illustrated in Table 2, in which recall is calculated as the ratio of subsumptions discovered by REL against those discovered by FaCT++. means FaCT++ timed-out or run out of memory.
As we can see, some ontologies are extremely di cult in contrast to their small size. By looking in depth into the ontologies, we see the di erences as: – R2 is quite easy for both REL and FaCT++ because it contains many explicit equivalence between concept names. – R3 has relatively complex domain and range with disjunctions, which are di cult to optimise for tableau algorithms. – R4 and R7 are relatively easy because they are actually shallow ontologies with only a few implicit subsumptions. – R1, R5, R6, R8 and R9 are di cult for FaCT++ because they all have many explicit or implicit A v 9r:> axioms, which will lead to large expansions for tableau algorithm. – R11, R12 and R13 are actually shallow with a few implicit subsumptions, although the number of roles is not small.
In order to evaluate the usability of our approximative reasoning approach on real world ontologies, we test REL on the wine and cyc ontology. More precisely, we first remove all the ABox axioms from these ontologies, and then use Pellet, FaCT++ and REL to classify them. The results are given in Tab.3. In order to justify the complement-integrated reasoning algorithm, we also use a EL+ reasoner to classify the approximated EL+ TBox solely without taking complement table into account.
Comparison shows that, REL can perform e ciently on real world ontologies as well and the recall is rather high (more than 90%). Also the complementintegrated reasoning algorithm can significantly improve the recall on particular ontologies. 5
In this paper we presented our approach to approximating description logic R into EL+ with an additional complement table. The approximation method we proposed is a syntax-based transformation which is very e cient and preserving the complementary relations. With additional completion rules and abstract algorithms that we proposed, the reasoning of resulted ontology is sound and tractable. Preliminary evaluation results showed that our approach can outperform existing DL reasoners on some di cult R ontologies.
The follow-up of the current work will be the investigation of the completeness and the optimisation of the implementation. Potential extension of this method aims at including more expressiveness for both source and target languages: a more comprehensive approximation from OWL2-DL to OWL2-EL is under investigation. We expect our work to push one step forward to dealing with complex GCIs and RIs in very expressive DLs, and to build a bridge between the ALC and EL families of DLs.
This work has been partially supported by the European Project Marrying Ontologies and Software Technologies (MOST ICT 2008-216691).