=Paper=
{{Paper
|id=None
|storemode=property
|title=Efficient Upper Bound Computation of Query Answers in Expressive Description Logics
|pdfUrl=https://ceur-ws.org/Vol-846/paper_43.pdf
|volume=Vol-846
|dblpUrl=https://dblp.org/rec/conf/dlog/ZhouGH12
}}
==Efficient Upper Bound Computation of Query Answers in Expressive Description Logics==
https://ceur-ws.org/Vol-846/paper_43.pdf
Efficient Upper Bound Computation of Query
Answers in Expressive Description Logics
Yujiao Zhou, Bernardo Cuenca Grau, and Ian Horrocks
Department of Computer Science, University of Oxford, UK
1 Introduction
In recent years, there has been a growing interest in the problem of conjunctive
query answering over description logic (DL) ontologies and large scale data sets.
This problem is central to many applications, which often involve managing data
sets consisting of hundreds of millions, or even billions of data assertions.
Meeting the scalability requirements of such applications is, however, a very
challenging problem. Answering conjunctive queries over ontologies in expres-
sive DLs is of high computational complexity; in fact, decidability is still an
open problem for SROIQ [14] —the DL that underpins the standard ontol-
ogy language OWL 2 [6]. Although small restriction on the ontology or query
language can ensure decidability [26], worst case complexity is still very high
(at least 2NExpTime) [15]. Several OWL/SROIQ reasoners, including Her-
miT [20], FaCT++ [28] and Racer [12], support query answering for restricted
classes of conjunctive queries, but in spite of intensive efforts at optimisation,
they can still only deal with small to medium size data sets [17, 13].
Scalability of query answering can be ensured by restricting the expressive
power of the ontology language to the level that makes reasoning tractable.
This has led to the development of three profiles of OWL 2, namely OWL 2
RL, OWL 2 EL, and OWL 2 QL [21]; these profiles are based on (families of)
“lightweight” description logics, notably the DLP [10], DL-Lite [4], and the EL
families of DLs [2], respectively. Query answering in all these lightweight DLs
can be implemented in polynomial time w.r.t. the size of data (and even in
LogSpace in the case of DL-Lite). Such appealing theoretical properties have
spurred the development of specialised reasoning techniques [24, 22, 18, 4, 16].
Although allowing for efficient query answering, these lightweight DLs impose
severe restrictions on the expressive power of the ontology language. In order to
provide scalable query answering w.r.t. ontologies that cannot be captured by
such lightweight DLs, Semantic Web researchers have developed reasoners that
can process arbitrary OWL/SROIQ ontologies, but that guarantee complete-
ness only for ontologies that fall within the fragment defined by the OWL 2
RL profile. Given the close connection between OWL 2 RL and datalog, these
reasoners typically implement (deductive) database algorithms based on data
materialisation. Examples of such systems include Jena [19] and OWLim [16].
All such materialisation-based reasoners are sound ; that is, the answers they
compute can be seen as a lower bound on the complete set of query answers.
For ontologies outside the OWL 2 RL profile, however, these reasoners are in-
complete, and hence they are not guaranteed to compute all query answers. A
possible approach to this problem is to investigate the behaviour of the reasoner
on a given query Q and ontology T in an effort to show that it behaves as
a complete reasoner w.r.t. Q, T and an arbitrary data set [7]. Providing such
guarantees is, however, not always possible.
An alternative approach, which we investigate in this paper, is to devise a
scalable procedure for computing complete but possibly unsound query answers.
Such answers provide an upper bound to the set of all answers, which can com-
plement the lower bounds efficiently computed by incomplete reasoners. The
combined use of such lower and upper bounds has many interesting implica-
tions. First, the difference between the upper and lower bounds can be used as
an optimisation for reducing the number of candidate answers; furthermore, it
also provides a measure of the degree of incompleteness of a reasoner for a given
input; finally, if both bounds match, we can efficiently compute all query answers
without relying on potentially very expensive entailment tests.
In order to be useful, upper bounds should clearly be as tight as possible,
and should also be efficiently computable. Obtaining such an upper bound is,
however, not straightforward. The technique we use is to approximate T to give
an ontology T 0 that is strictly “stronger” that T (i.e., T 0 |= T ), and that is
within a fragment for which query answers can be efficiently computed.
Knowledge approximation has been extensively studied in the literature, al-
though mostly in the direction of weakening the ontology/theory [8, 23]. There
has also been some work on strengthening approximations. For propositional
logic, Horn theories can be used to both strengthen and weaken the original
theory [27]; these Horn approximations can then be used to optimise reasoning
by exploting the more efficient inference in the Horn theories. Finally, approxi-
mation is also related to the computation of least common subsumers [1].
Our technique exploits recent work on chase termination for existential rules,
which introduces a so called Models-Summarising Acyclicity (MSA) check [5].
MSA is an approximation of existential rules (datalog± ) into datalog. As most
SROIQ TBoxes can be translated into existential rules extended with disjunc-
tion (datalog±,∨ ) using model-preserving transformations, we can adapt MSA
to produce a datalog approximation of a SROIQ TBox. Moreover, the result-
ing datalog rules can be translated back into an OWL 2 RL TBox for which
complete query answers can be computed using materialisation based reasoners.
We have implemented our approach, and conducted preliminary experiments
using LUBM [11]. Our preliminary results suggest that our bound could be tight
for many queries, and it can be computed efficiently (or at least with similar
efficiency to computing the lower bound).
2 Preliminaries
We assume basic familiarity with the DLs underpinning the ontology language
OWL 2 and its profiles. We next introduce datalog±,∨ and datalog languages,
and define the syntax and semantics of conjunctive queries. In our definitions, we
adopt standard first-order logic notions of variable, constant, term, substitution,
atom, formula, and sentence. We assume all formulas to be function-free. We
denote with ⊥ the special atom evaluated as false in all interpretations, and we
use ≈ to denote the special equality predicate in first-order logic. Finally, we
also adopt the standard notions of satisfiability, unsatisfiability, and entailment.
Datalog Languages. A datalog±,∨ rule r is a formula of the form (1), where
each Bj is an atom different from ⊥ whose free variables are contained in x, and
– m = 1 and ϕ1 (x, y 1 ) = ⊥, or
– m ≥ 1 and, for each 1 ≤ i ≤ m, formula ϕi (x, y i ) is a conjunction atoms
different from ⊥ whose free variables are contained in x ∪ y i .
m
_
∀x.[B1 ∧ ... ∧ Bn ] → ∃y i .ϕi (x, y i ) (1)
i=1
A rule is safe if each variable in x also occurs in some Bj , and we consider
only safe rules. For brevity, the quantifier ∀x is left implicit. The body of r is
Wm set body(r) = {B1 , . . . , ±,∨
the Bn }, and the head of r is the formula head(r) =
i=1 ∃y i .ϕ(x, y i ). A datalog rule r is datalog± if m = 1 [3], and it is datalog
±
if it is datalog and the head is a single atom without existential quantifiers.
A fact is a ground atom, and an instance I is a finite set of facts. We denote
with ind(I) the set of all individuals occurring in I.
For Σ a set of datalog rules and I an instance, the saturation of Σ w.r.t. I
is the instance I 0 consisting of all facts entailed by Σ ∪ I.
Most DL ontologies can be transformed into a set of datalog±,∨ rules and an
instance by means of standard transformations. The rules and facts obtained via
such transformations involve only unary and binary predicates; thus, we define
an ABox A as an instance containing only unary and binary atoms.
Queries. A conjunctive query (CQ), or simply a query, is a formula Q(x) of the
form ∃y.ϕ(x, y), where ϕ(x, y) is a conjunction of atoms. A tuple of individuals
a is a certain answer to a query Q(x) w.r.t. a set of first-order sentences F and
an instance I if F ∪ I |= Q(a). The set of answers of Q(x) w.r.t. F and I is
denoted as cert(Q, F, I), where the free variables of Q(x) are omitted for brevity.
3 Technical Approach
3.1 Overview
Given a TBox T , an ABox A and a query Q, our goal is to compute a (hopefully
tight) upper bound to the set cert(Q, T , A) of answers. We poceed as follows:
1. Transform T into a set ΣT of datalog±,∨ rules such that ΣT is a conservative
extension of T .
2. Transform ΣT into a set approx(ΣT ) of datalog rules s.t. approx(ΣT ) |= ΣT .
Student v Person Student(x) → Person(x)
RA v Student RA(x) → Student(x)
RA v ∃works.Group RA(x) → ∃y.[works(x, y) ∧ Group(y)]
Group v Org Group(x) → Org(x)
Emp(x) → Person(x)
Emp ≡ Person u ∃works.Org Emp(x) → ∃y.[works(x, y) ∧ Org(y)]
Person(x) ∧ works(x, y) ∧ Org(y) → Emp(x)
works v memberOf works(x, y) → memberOf(x, y)
Student v Grad t Undergrad Student(x) → Grad(x) ∨ Undergrad(x)
func(works) works(x, y) ∧ works(x, z) → y ≈ z
Fig. 1. Transforming Tex into datalog±,∨ rules ΣTex
3. Transform approx(ΣT ) into an OWL 2 RL TBox T 0 for which we have
cert(Q, approx(ΣT ), A) = cert(Q, T 0 , A) for every query Q and ABox A.
Our transformation depends only on T , and satisfies the following property:
cert(Q, T , A) ⊆ cert(Q, T 0 , A) for every query Q and ABox A
Given the OWL 2 RL TBox T 0 we can then use T and T 0 with a materialisation
based reasoner rl that is sound for OWL 2 and complete for OWL 2 RL (such as
OWLim) to respectively compute a lower and an upper bound to query answers
for the given Q and A. More precisely, we have:
rl(Q, T , A) ⊆ cert(Q, T , A) ⊆ rl(Q, T 0 , A) for every Q and A
3.2 Computing the Upper Bound
We next describe in detail the transformations in Steps 1-3. As a running exam-
ple, we use the TBox Tex in Figure 1.
From DL TBoxes to Datalog±,∨ Rules. The first step is to transform the
DL TBox T into a set ΣT of datalog±,∨ rules such that ΣT is a conservative
extension of T . For a wide range of DLs, this can be achieved by first using
the well-known correspondence between DL axioms and first-order logic for-
mulas and then applying standard structural transformation rules, which may
involve introducing new predicates. The transformation of our example Tex into
datalog±,∨ rules ΣTex is also shown in Figure 1; here, Tex and ΣTex are equivalent.
From Datalog±,∨ to Datalog. Next, we approximate the datalog±,∨ rules
ΣT by a datalog program approx(ΣT ) that entails ΣT . Intuitively, this transfor-
mation can be described in two steps:
– Rewrite each datalog±,∨ rule r into a set of datalog± rules by transforming
disjunctions in the head of r into conjunctions and splitting the conjunctions
into different datalog± rules. Such a way to eliminate disjunction in the head
has been used in OWL reasoning with logic program [25].
RA(x) → ∃y.[works(x, y) ∧ Group(y)] RA(x) → works(x, c1 ) ∧ Group(c1 )
Emp(x) → ∃y.[works(x, y) ∧ Org(y)] Emp(x) → works(x, c2 ) ∧ Org(c2 )
Student(x) → Grad(x) ∨ Undergrad(x) Student(x) → Grad(x) ∧ Undergrad(x)
Fig. 2. Transforming ΣTex into approx(ΣTex )
– Transform the resulting datalog± rules into datalog using fresh individuals
to skolemise existentially quantified variables.
Figure 2 illustrates this process for our example. The figure shows only the rules
in ΣTex that need changing; note that c1 and c2 are fresh individuals used to
skolemise existentially quantified variables.1
Definition 1. For each datalog±,∨ rule r of the form (1) and each variable
yij ∈ y i , let crij be a fresh individual unique for r and yij . Then, approx(r) is the
following set of rules, where for each 1 ≤ i ≤ m, θir is a substitution mapping
each variable yij ∈ y i to crij :
approx(r) = {B1 ∧ ... ∧ Bn → ϕi (x, θir (y i )) | 1 ≤ i ≤ m} (2)
For Σ a set of datalog±,∨ rules, approx(Σ) is the smallest set that contains
approx(r) for each rule r ∈ Σ.
We next show that approx(ΣT ) entails ΣT . The following proposition pro-
vides sufficient and necessary conditions for a datalog±,∨ rule to be entailed by
an arbitrary set of first-order sentences (the proof is rather straightforward and
can be found in [7]).
Proposition 1. Let F be a set of first-order sentences and r be a datalog±,∨
rule of the form (1). Then, for each substitution σ mapping the free variables of
r to distinct individuals not occurring in F or r, we have F |= r if and only if
m
_
F ∪ {σ(B1 ), . . . , σ(Bn )} |= ∃y i .ϕi (σ(x), y i )
i=1
Proposition 1 can be used to show that each datalog±,∨ rule r in ΣT is entailed
by approx(r), and hence approx(ΣT ) strengthens ΣT .
Proposition 2. For Σ a set of datalog±,∨ rules, we have approx(Σ) |= Σ.
Proof. It suffices to show that, for each rule r ∈ Σ of the form (1) and each
ri ∈ approx(r), we have ri |= r. Let σ be a substitution mapping the free variables
in r to fresh individuals; by Proposition 1, we have
m
_
ri |= r ⇔ ri ∪ {σ(B1 ), . . . , σ(Bn )} |= ∃y i .ϕi (σ(x), y i ) (3)
i=1
1
Note that, although approx(ΣTex ) is strictly speaking not datalog (we have conjunc-
tion of atoms in the head), it is trivially equivalent to a set of datalog rules.
Since ri and r have the same body atoms, the definition of ri in (2) implies
ri ∪ {σ(B1 ), . . . , σ(Bn )} |= ϕi (σ(x), θir (y i )) (4)
Since substitution θir maps variables to constants, the following conditions clearly
hold by the semantics of first-order logic:
m
_
ϕi (σ(x), θir (y i )) |= ∃y i .ϕi (σ(x), y i ) |= ∃y i .ϕi (σ(x), y i ) (5)
i=1
But then, conditions (3), (4) and (5) immediately imply ri |= r, as required. t
u
The fact that approx(Σ) entails Σ implies that query answers w.r.t. approx(Σ)
are an upper bound to those w.r.t. Σ.
Proposition 3. For each set of datalog±,∨ rules Σ, each ABox A and each
query Q, we have cert(Q, Σ, A) ⊆ cert(Q, approx(Σ), A).
From Datalog to OWL 2 RL. The last step is to transform approx(ΣT ) into
an OWL 2 RL TBox T 0 . Although arbitrary datalog rules cannot be transformed
into OWL 2 RL, the rules in approx(ΣT ) have been obtained from a DL TBox
and are therefore tree-shaped, which makes this transformation possible.
There is, however, a technical consideration related to the fresh skolem con-
stants in approx(ΣT ). In particular, the following rule in our running example
(see Figure 2) does not directly correspond to an OWL 2 RL axiom:
RA(x) → works(x, c1 ) ∧ Group(c1 ) (6)
This issue can be easily addressed by introducing fresh atomic roles. More pre-
cisely, rule (6) can be transformed into the following three OWL 2 RL axioms,
where R0 is a fresh atomic role:
RA v ∃R0 .{c1 } > v ∀R0 .Group R0 v works
3.3 Additional Considerations
Transformation of Disjunctive Rules. The proof of Proposition 2 suggests
that we can easily weaken approx(ΣT ) given in Definition 1 such that ΣT is still
entailed. In particular, when transforming a disjunctive rule in ΣT into datalog
by replacing disjunctions with conjunctions, it suffices to keep only one of the
conjuncts. For example, given the transformation
Student(x) → Grad(x) ∨ Undergrad(x) Student(x) → Grad(x) ∧ Undergrad(x)
we can replace in approx(ΣT ) the rule Student(x) → Grad(x) ∧ Undergrad(x)
with either Student(x) → Grad(x), or Student(x) → Undergrad(x). Any of these
choices will lead to a (different) upper bound. In practice, one can choose to
process any number of such different options, or simply devise suitable heuristics
to choose the most promising one.
Unsatisfiability Issues. For given TBox T and ABox A, it might be the case
that approx(ΣT ) ∪ A is unsatisfiable, whereas ΣT ∪ A is satisfiable. Then, the
upper bound we obtain is the trivial one for each query. For example, if we extend
Tex in Figure 1 with the axiom Grad u Undergrad v ⊥, we obtain a rule with ⊥
in the head in ΣT , namely Grad(x) ∧ Undergrad(x) → ⊥. For Aex = {RA(a)} we
then have that Tex ∪ Aex is satisfiable, but approx(ΣTex ) ∪ Aex is unsatisfiable;
thus, for a given Q, any tuple of individuals of the appropriate arity must be
included in the upper bound.
A way to address this issue is to remove from approx(ΣT ) all rules with ⊥ in
the head. Although it is then no longer the case that approx(ΣT ) |= ΣT , we can
still guarantee completeness provided that ΣT ∪ A is satisfiable.
Proposition 4. Let Σ be a set of datalog±,∨ rules and let Σ 0 the result of re-
moving from approx(Σ) all rules containing ⊥ in the head. Then, the following
condition holds for each ABox A and each query Q: if Σ ∪ A is satisfiable, then
cert(Q, Σ, A) ⊆ cert(Q, Σ 0 , A).
In practice, checking the satisfiability of T ∪A, which is equisatisfiable with ΣT ∪
A, is easier than (and a prerrequisite for) query answering. Even if satisfiability
of T ∪ A cannot be checked in practice using a complete reasoner for a very large
A, we can still compute an upper bound “modulo satisfiability”.
Why Translating Back into OWL 2 RL? Our last step was to transform
approx(ΣT ) into OWL 2 RL TBox T 0 . Note, however, that one could obtain the
upper bound directly from approx(ΣT ) by first computing the saturation A0 of
approx(ΣT ) w.r.t. A and then computing cert(Q, ∅, A0 ).
The saturation A0 can be computed in polynomial time [5]; indeed, the rules
in approx(ΣT ) are tree-shaped, which can be exploited to obtain a polynomial
time saturation procedure. This could lead to better performance in the compu-
tation of our upper bound —an interesting topic for future work.
Our current approach, however, does have some advantages. In particular,
one can use the same off-the-shelf RL reasoner (such as OWLim) to compute
both the lower and upper bound, which is convenient in practice. Furthermore,
as suggested by our experiments, reasoners such as OWLim are quite efficient
for large data sets.
4 Experiments
We have implemented our approach in Java and used the latest version of
OWLim-Lite as an OWL 2 RL reasoner. All experiments have been performed
on a desktop computer with 4Gb of RAM, of which 3000Mb were assigned as
maximum heap size in Java.
In our experiments, we have used LUBM extended with additional synthet-
ically generated queries. The LUBM ontology contains 93 TBox axioms, out of
which 8 contain existential quantification, and 39 are domain and range axioms.
The LUBM ontology, however, does not contain disjunction or negation; thus,
Table 1. Number of answers for the 14 LUBM queries
Query 1 2 3 4 5 6 7
Lower Bound 4 0 6 34 719 7356 67
Upper Bound 4 0 6 34 719 7356 67
Query 8 9 10 11 12 13 14
Lower Bound 7356 194 4 212 14 1 5594
Upper Bound 7356 194 4 212 14 1 5594
Table 2. Synthetic queries for which OWLim is incomplete
Query Lower Bound Upper Bound HermiT’s answers
3 540 1087 1087
51 0 547 547
67 540 1087 1087
69 0 547 547
the corresponding issues discussed in Section 3.3 do not apply to our experi-
ments. To test how tight our upper bounds are for different queries, we have
used LUBM(1,0), the smallest data set in the benchmark, since the complete
DL reasoner HermiT can answer all test queries for this data set. LUBM(1,0)
contains data for one university and 14 departments, with a total of 100, 543
ABox assertions about 17, 174 different individuals.
4.1 Results for LUBM(1,0)
Standard Queries. LUBM provides 14 queries. As shown in Table 1, the lower
and upper bounds computed using OWLim coincide, which allows us to conclude
that OWLim is complete for all these queries and the LUBM(1,0) data set.
Hence, in these cases, one wouldn’t need to use a complete DL reasoner at all.
Additional Synthetic Queries. We have used a synthetic query generation
tool [9] to compute 78 additional queries for LUBM. For all these queries, except
those in Table 2, lower and upper bounds also coincide. Furthermore, for all
queries in Table 2 the upper bound is tight.
Observe, however, that the lower bound is missing those answers which re-
quire taking into account LUBM’s axioms with existential quantifiers, for which
OWLim is not complete. For example, consider the following query
Q51 (x) = ∃y.(memberOf(x, y) ∧ Group(y))
LUBM’s ontology contains all the axioms in Tex , except for the last two axioms in
Figure 1; furthermore, LUBM(1,0) contains many instances of RA. Since LUBM’s
ontology implies that each RA works for (and hence is a member of) some group,
all these instances are answers to Q51 , which are not computed by OWLim.
Additional Query. For all previous test queries, we have obtained a tight upper
bound. To show that this is not always the case, we have manually created the
additional query given next.
Q(x1 , x2 ) = ∃y.works(x1 , y) ∧ works(x2 , y) ∧ Group(y)
Since this query is not tree-like, it cannot be answered using HermiT. To obtain
the complete answers, we have used REQUIEM2 to compute a (complete) UCQ
rewriting U of Q w.r.t. LUBM’s ontology; then, we used OWLim to compute
the answers to U w.r.t. the LUBM(1,0) data. For this query, the lower and
upper bounds contained zero and 299, 209 answers, respectively; in contrast, we
obtained 547 answers using REQUIEM and hence the upper bound is not tight.
As shown in Figure 2, our transformation implies that all RAs work for the
same group (represented by the skolem constant c1 ); since there are many in-
stances of RA in LUBM(1,0), all pairs of RA instances will be included in the
upper bound. Clearly, however, many of these RAs work for different groups.
Note, however, that even for this query we managed to reduce the number
of candidate answers from 17, 1742 ∼ 3 × 108 to 299, 209.
4.2 Scalability Tests
To test scalability of upper bound computation, we have performed additional
experiments using LUBM data sets of increasing size (from 1 to 10 universities).
For each data set and each of the 78 synthetic queries, we have computed lower
and upper bounds (using OWLim) and the complete answers (using HermiT).
The results are summarised in Figure 4.2, where the time refers to the total
query answering time for all test queries.
We can observe similar query answering times and scalability behaviour for
lower and upper bound computation. Furthermore, we can observe that Her-
miT’s performance is similar to OWLim’s for relatively small data sets. HermiT,
however, does not scale well for the largest LUBM data sets. In particular, it
takes 178s to complete the tests for 9 universities and runs out of memory for
10 universities; in contrast, OWLim computation times increase more regularly.
5 Conclusion and Future Work
In this paper, we have proposed a novel technique for efficiently computing
an upper bound to CQ answers for ontologies given in a expressive DL. Our
preliminary experiments on LUBM show that this upper bound might be tight
in many cases. Furthermore, we identified cases were lower and upper bounds
coincide and hence it is not necessary to use a fully-fledged DL reasoner such as
HermiT to compute query answers (HermiT is able to answer rollable queries).
Our work so far, however, is only very preliminary, and there are plenty of
possibilities for future work. We are planning to perform experiments with on-
tologies involving disjunction and negation, and address the issues discussed in
2
http://www.cs.ox.ac.uk/isg/tools/Requiem/
100
1400
Answers by Hermit
80 Lower Bound by OWLim 1200
Upper Bound by OWLim
The Number of Axioms (*103)
The Size of ABox
1000
60
Time (s)
800
40 600
400
20
200
0 0
0 2 4 6 8 10
The Number of Universities
Fig. 3. Running Time Comparison
Section 3.3. Furthermore, we will implement a dedicated datalog engine that can
compute the saturation in polynomial time for tree-shaped datalog rules; this
might allow us to improve performance as well as to simultaneously compute
lower and upper bounds. We will also develop techniques for identifying during
upper bound computation the fragments of the ABox and TBox that are suffi-
cient to determine, using a complete reasoner, which of the answers in the upper
bound are actual answers; we expect that these techniques will provide addi-
tional room for optimisation. As a result, we can integrate all these techniques
in HermiT to optimise query answering.
Acknowledgements. This work was supported by the Royal Society, the EU
FP7 project SEALS and the EPSRC projects ConDOR, ExODA, and LogMap.
References
1. Baader, F., Sertkaya, B., Turhan, A.: Computing the least common subsumer wrt
a background terminology. J. of Applied Logic (JAL) 5(3), 392–420 (2007)
2. Baader, F., Brandt, S., Lutz, C.: Pushing the EL envelope. In: IJCAI (2005)
3. Cali, A., Gottlob, G., Lukasiewicz, T., Marnette, B., Pieris, A.: Datalog+/-: A fam-
ily of logical knowledge representation and query languages for new applications.
In: Proc. of LICS (2010)
4. Calvanese, D., De Giacomo, G., Lembo, D., Lenzerini, M., Rosati, R.: Tractable
reasoning and efficient query answering in description logics: The DL-Lite family.
J. of Automated Reasoning (JAR) 39(3), 385–429 (2007)
5. Cuenca Grau, B., Horrocks, I., Krötzsch, M., Kupke, C., Magka, D., Motik, B.,
Wang, Z.: Acyclicity conditions and their application to query answering in de-
scription logics. In: Proc. of KR (2012)
6. Cuenca Grau, B., Horrocks, I., Motik, B., Parsia, B., Patel-Schneider, P.F., Sattler,
U.: OWL 2: The next step for OWL. J. Web Semamtics (JWS) 6(4), 309–322 (2008)
7. Cuenca Grau, B., Motik, B., Stoilos, G., Horrocks, I.: Completeness guarantees
for incomplete ontology reasoners: Theory and practice. J. of Artificial Intelligence
Research (JAIR) 43 (2012)
8. Del Val, A.: First order lub approximations: characterization and algorithms. Ar-
tificial Intelligence 162(1-2), 7–48 (2005)
9. Grau, B.C., Stoilos, G.: What to ask to an incomplete semantic web reasoner? In:
Proc. of IJCAI. pp. 419–476 (2011)
10. Grosof, B.N., Horrocks, I., Volz, R., Decker, S.: Description logic programs: com-
bining logic programs with description logic. In: Proc. of WWW (2003)
11. Guo, Y., Pan, Z., Heflin, J.: Lubm: A benchmark for OWL knowledge base systems.
J. Web Semantics (JWS) 3(2-3), 158–182 (2005)
12. Haarslev, V., Möller, R.: RACER system description. J. of Automated Reasoning
(JAR) pp. 701–705 (2001)
13. Haarslev, V., Möller, R., Wessel, M.: Querying the semantic web with
RACER+NRQL. In: Proc. of ADL (2004)
14. Horrocks, I., Kutz, O., Sattler, U.: The even more irresistible SROIQ. In: Proc.
of KR (2006)
15. Kazakov, Y.: RIQ and SROIQ are harder than SHOIQ. In: Proc. of KR (2008)
16. Kiryakov, A., Ognyanov, D., Manov, D.: OWLIM–a pragmatic semantic repository
for OWL. In: Proc. of WISE Workshops (2005)
17. Kollia, I., Glimm, B., Horrocks, I.: Query answering over sroiq knowledge bases
with SPARQL. In: Proc. of DL (2011)
18. Lutz, C., Toman, D., Wolter, F.: Conjunctive query answering in the description
logic EL using a relational database system. In: Proc. of IJCAI. vol. 9 (2009)
19. McBride, B.: Jena: Implementing the rdf model and syntax specification. In: Se-
mantic Web Workshop. vol. 40 (2001)
20. Motik, B., Shearer, R., Horrocks, I.: Hypertableau reasoning for description logics.
J. of Artificial Intelligence Research (JAIR) 36(1), 165–228 (2009)
21. Motik, B., Cuenca Grau, B., Horrocks, I., Wu, Z., Fokoue, A., Lutz, C.: OWL 2
Web Ontology Language Profiles. W3C Recommendation (2009)
22. Pérez-Urbina, H., Motik, B., Horrocks, I.: Tractable query answering and rewriting
under description logic constraints. J. of Applied Logic (JAL) 8(2), 186–209 (2010)
23. Ren, Y., Pan, J.Z., Zhao, Y.: Soundness preserving approximation for tbox rea-
soning. In: Proc. of AAAI (2010)
24. Rosati, R.: On conjunctive query answering in EL. In: Proc. of DL. vol. 46 (2007)
25. Rudolph, S., Krötzsch, M., Hitzler, P., Sintek, M., Vrandecic, D.: Efficient owl rea-
soning with logic programs–evaluations. Web Reasoning and Rule Systems (2007)
26. Rudolph, S., Glimm, B.: Nominals, inverses, counting, and conjunctive queries or:
Why infinity is your friend! J. Artif. Intell. Res. (JAIR) 39, 429–481 (2010)
27. Selman, B., Kautz, H.: Knowledge compilation and theory approximation. J. of
the ACM (JACM) 43(2), 193–224 (1996)
28. Tsarkov, D., Horrocks, I.: Fact++ description logic reasoner: System description.
J. Automated Reasoning (JAR) pp. 292–297 (2006)