Rewriting ontology mediated queries (OMQs) into traditional query languages like FO-queries and Datalog is central for understanding their relative expressiveness, and plays a crucial role in the ongoing e orts to develop OMQ answering tools by reusing existing database technologies. However, the vast majority of works focus on Horn ontologies, and for OMQs where the ontologies are written in extensions of ALC, only a couple of exponential rewritings into disjunctive Datalog are known. In this paper we propose a translation of instance queries mediated by ontologies in the expressive DL ALCHI, into polynomial-sized disjunctive Datalog programs. The translation is based on a simple game-like algorithm, and can be extended to accommodate nominals. We can also rewrite OMQs with closed-predicates into Datalog programs with (limited) negation. Closed predicates are useful for combining complete and incomplete information, but make OMQs non-monotonic and thus not rewritable into positive disjunctive Datalog.
In ontology-mediated queries (OMQs), a database query is enriched with an
ontology, providing knowledge to obtain more complete answers from incomplete
data. OMQs are receiving much attention in the database and knowledge
representation research communities, particularly when the ontological knowledge is
expressed in Description Logics (DLs) or in rule-based formalisms like existential
rules and Datalog , see e.g., [
Research into OMQs that can be rewritten into rst-order (FO) queries has
produced the successful DL-Lite family [
The main contribution of this paper is a polynomial time translation of
instance queries mediated by ALCHI TBoxes into disjunctive Datalog. The
translation is based on a simple game-theoretic characterization, and implements
a so-called type-elimination procedure using a polynomially sized Datalog
program. To our knowledge, this is the rst polynomial time translation of an
expressive (non-Horn) DL into disjunctive Datalog. The translation we present
here can be extended to richer OMQs, and in particular, to nominals and closed
predicates. In fact, we report here a simpli ed version of the translation in [
The DL ALCHI We assume countably in nite, mutually disjoint sets NR of role names, NC of concept names, and NI of individual names. A role r is either a role name p, or an expression p , called the inverse of p. We let r = p if r = p . Concepts are de ned inductively: (i) >, ? and all A 2 NC are concepts; (ii) if C1; C2 are concepts, then C1 u C2, C1 t C2 and :C1 are concepts; (iii) if r is a role, and C is a concept, then 9r:C, 8r:C are concepts. A concept inclusion is an expression of form C1 v C2, where C1; C2 are concepts. A role inclusion is an expression of form r1 v r2, where r1; r2 are roles. A TBox T is a nite set of (concept and role) inclusions. An ABox A is a nite set of assertions of the forms A(a) and p(a; b), where fa; bg NI, A 2 NC, and p 2 NR. A knowledge base (KB) is a tuple K = (T ; A), where T is a TBox and A is an ABox.
An interpretation is a pair I = h I ; I i, where I is a non-empty set (called
the domain), AI I for each A 2 NC, rI I I for each r 2 NR, and
aI 2 I for each a 2 NI. The function I is extended to the remaining concepts
and roles in the standard way [
Assume a KB K = (T ; A) and an assertion . Towards deciding K 6j= polynomially sized program, we decompose the problem into two steps: using a (1) Guess a core interpretation Ic for K, whose domain is NI(A). Core interpretations x how the individuals of K participate in concepts and roles, ensuring the satisfaction of A, and the non-entailment of . (2) Check that Ic can be extended to satisfy all axioms in T .
De ning Datalog rules that do (1) is not hard, but (2) is more challenging, and will rely on a game-theoretic characterization we describe below. But rst we need to de ne core interpretations.
De nition 1. A core interpretation for a KB K = (T ; A) is any interpretation Ic such that (c1) Ic = NI(A) and aIc = a for all a 2 NI(A), (c2) Ic j= A, (c3) Ic j= A v 8r:A0 for all A v 8r:A0 2 T , (c4) Ic j= r v s for all r v s 2 T , (c5) qIc = ; for each q 62 NC(T ) [ NR(T ).
An interpretation J is called an extension of Ic, if Ic is the result of restricting J to NI(A).
A core and its extensions coincide on the assertions they entail, and deciding non-entailment of an instance query q amounts to deciding whether there is a core that does not entail q, and that can be extended into a model. But verifying whether a core can be extended into a full model is hard: it corresponds to testing consistency (of Ic viewed as an ABox) with respect to T , an ExpTime-hard problem already for fragments of ALCHI. In order to obtain a polynomial set of rules that solves this ExpTime-hard problem, we characterize it as a game, revealing a simple algorithm that admits an elegant implementation in Datalog. De nition 2. A type (over a TBox T ) is a subset of NC(T ) [ f>g such that ? 62 and > 2 . We say that satis es an inclusion = A1 u u An v An+1 t t Ak of type (N1), if fA1; : : : ; Ang implies fAn+1; : : : ; Akg \ 6= ;; otherwise violates . For an element e 2 I in an interpretation I, we let type(e; I) = fB 2 NC j e 2 BI g. A type is realized in I if there is some e 2 I s.t. type(e; I) = .
We now describe a game to decide whether a given core Ic can be extended into a model of a KB K. The game is played by Bob (the builder), who wants to extend Ic into a model, and Sam (the spoiler), who wants to spoil all Bob's attempts. Sam starts by picking an individual a, and they look at its type type(a; Ic). If it doesn't satisfy the inclusions of type (N1) Sam wins. Otherwise, in each turn Sam chooses an inclusion of the form A v 9rA0 which would need to be satis ed by (an element with) the current type, forcing Bob to pick a type for the corresponding r-successor that satis es A0. The game continues for as long as Bob can respond to the challenges of Sam.
The game on I starts by Sam choosing an individual a 2 I , and = type(a; I) is set to be the current type. Then: ( ) If does not satisfy all inclusions of type (N1) in T , then Sam is declared the winner. Otherwise, Sam chooses an inclusion A v 9r:A0 2 T with A 2 ; if there is no such inclusion, Bob is declared the winner. Otherwise, Bob chooses a new type 0 such that: (C1) A0 2 0, and (C2) for all inclusions A1 v 8s:A2 2 T : if r v s 2 T and A1 2 then A2 2 0, if r v s 2 T and A1 2 0 then A2 2 .
0 is set to be the current type, and the game continues with a new round, i.e. we go back to .
A run of the game on I is a (possibly in nite) sequence where a is the individual picked initially by Sam, and each i and i are the inclusion picked by Sam and the type picked by Bob in round i, respectively. A strategy for Bob is a partial function str that maps pairs of a type and an inclusion A v 9r:A0 with A 2 to a type 0 that satis es (C1) and (C2); intuitively, it gives a move for Bob in response to moves of Sam. A run a 1 1 2 2 : : : with type(a; I) = 0 follows a strategy str if i = str( i 1; i) for every i 1.
For a nite run w, we let tail(w) = type(a; I) if w = a, and tail(w) = ` if w = a : : : ` ` with ` 1. The strategy str is called non-losing on I if for every nite run w that follows str, tail(w) satis es all inclusions of type (N1) in T , and str(tail(w); A v 9r:A0) is de ned for every A v 9r:A0 2 T with A 2 tail(w). Theorem 1. Assume a KB K and an assertion . Then K 6j= core interpretation Ic for K such that: (1) Ic 6j= , and (2) there is a non-losing strategy for Bob on Ic. i there is a Proof. (Sketch.) We focus on showing that there is a non-losing strategy str for Bob on Ic i there exists an extension J of Ic s.t. J j= K. The claim follows from this, and the easy claim that extensions preserve non-entailment of .
For the \)" direction, from an arbitrary non-losing str for Ic, we build J as follows. We denote by frn(Ic; str) the set of all nite runs a 1 1 : : : i i, i 0 that follow str. The domain of J is:
J = frn(Ic; str) and for each a 2 NI, each A 2 NC, and each p 2 NR we let: aJ = aIc
AJ = fw j A 2 tail(w)g pJ = pIc [ f(w; w i i) j ri v p 2 T g [
f(w i i; w) j ri v p 2 T g where i = A v 9ri:A0 2 T and fw; w i ig J .
It is not hard to see that J is an extension of Ic. We show that J is a model of K. First, J j= A by de nition of Ic and the fact that J is an extension of Ic. It is left to prove that J satis es all inclusions in T . Note that for each w 2 J , type(w; J ) = tail(w). That J satis es all inclusions of type (N1) holds by de nition of non-losing str and the fact that tail(w) satis es all such inclusions. For the inclusions = A v 9r:A0 of type (N2), we see that for each w 2 J , if w 2 AJ , then A 2 tail(w) and w is a run that follows str. Hence, since str is a non-losing strategy str(tail(w); ) is de ned, that is there exists a 0 over T such that str(tail(w); ) = 0 and A0 2 0. Thus w 0 is a run that follows str, i.e. w 0 2 frn(Ic; str), so w 0 is in A0J and (w; w 0) 2 rJ if r is a role name, and (w 0; w) 2 rJ otherwise. For the inclusions A1 v 8r:A2 of type (N3), we distinguish the case of (a; a0) 2 rIc for a pair a; a0 of individuals in Ic , for which a 2 A1J implies a0 2 A2J holds by de nition of Ic, and the case of an arbitrary pair of objects (w; w0) 2 rIc where w0 is a child of w (that is, w0 is of the form w i i), or vice-versa, for which w0 2 AJ whenever w 2 A1J is ensured by the 2 condition (C2) in the de nition of the game, the fact that str is a non-losing strategy, and the construction of J . Finally, the inclusions of type (N4) are also guaranteed by the de nition of the core Ic for pairs of individual names, and by the condition (C2) in the de nition of the game for arbitrary pairs of an object and its child.
For \(", assume an arbitrary model J of K that is an extension of Ic. We can extract from it a non-losing strategy for Bob as follows. First, let T be a the set of all the types realized in J , and observe that each type in T satis es all inclusions of type (N1) and that for all a 2 NI(A), type(a; J ) 2 T . Then it su ces to set, for each 2 T and each A v 9r:A0 2 T with A 2 , str( ; A v 9r:A0) = 0 for an arbitrarily chosen 0 2 T that satis es (C1) and (C2), which exists because J is a model, hence it satis es all existential and universal inclusions in T , and all types realized in J are contained in T . This str is a non-losing strategy for Bob. tu
To decide whether Bob has a non-losing strategy on a given core we use the type elimination procedure Mark in Algorithm 1, which marks (or, eliminates ) all types from which Sam has a winning strategy. It takes as input the TBox T , and an interpretation I which intuitively is the core being checked. The algorithm starts by building the set N of all possible types over T , and then it eliminates bad choices (from which Bob would loose) by marking them. In step (MN1), the algorithm marks in N all types that violate some inclusion of type (N1) in T ; Sam wins already in the rst round on these types. Then, in the loop, (M9) exhaustively marks types that allow Sam to pick an inclusion A v 9r:A0 for
input : TBox T , interpretation I output : Set of (possibly marked) types N
f j is a type over T g (MN1) Mark each
2 N that violates some inclusion of the form (N1) in T repeat (M9) Mark each 2 N such that A v 9r:A0 2 T , A 2 , and for each 0 2 N , at least one the following holds: (C0)
0 is marked, (C10) A0 2= 0, or (C20) there exists A1 v 8s:A2 2 T with { r v s 2 T and A1 2 { r v s 2 T and A1 2 0 and A2 2=
and A2 2= 0, or until no new type is marked return N which Bob cannot reply with any 0. At the end the marked types, are those from which Bob can lose, so we get: Theorem 2. Let Ic be a core interpretation. Then Bob has a non-losing strategy on Ic i none of the types realized in Ic is marked by Mark(T ; Ic). Proof. (Sketch.) For the \)" direction, we can show (by induction in the number of iterations of Mark(T ; Ic)) that if a type is marked, then it cannot occur in a non-losing str for Bob. For the \(" direction, a non-losing str for Ic is obtained by taking all unmarked 2 N , and for each of them, and each A v 9r:A0 2 T with A 2 , setting str( ; A v 9r:A0) = 0 for an arbitrary unmarked 0 that satis es (C1) and (C2). tu 4
Assume an instance query (T ; q). We build next a polynomially sized program P such that the queries (T ; q) and (P; q) have the same certain answers for all ABoxes over the signature of T . Roughly, the program P has 3 major components: (a) rules to non-deterministically generate a core interpretation Ic for the KB (T ; A), where A is an input ABox; (b) rules that implement the type elimination algorithm presented in the previous section; (c) rules that glue (a) and (b) together, ensuring that all types that occur in Ic are not marked by the marking procedure. We remark that the construction of P is independent from any particular ABox. (I) Collecting the individuals We rst add rules to collect in the unary predicate ind all the individuals that occur in the input ABox. For each A 2 NC(T ), r 2 NR(T ), we have: ind(x)
A(x) r(x; y) ind(y) r(x; y) (II) Generating core interpretations For each A 2 NC(T ) (resp., r 2 NR(T )) we will use a fresh concept name A (resp., role name r). We add the following rules to P :
A(x) _ A(x) r(x; y) _ r(x; y) ind(x) A(x); A(x) ind(x); ind(y) r(x; y); r(x; y)
A 2 NC(T ) A 2 NC(T ) r 2 NR(T ) r 2 NR(T ) To ensure (c3) in De nition 1, for each A v 8r:A0 2 T we add the rule A0(y) A(x); r(x; y). Then, to ensure (c4), for each role inclusion r v s 2 T we add the rule s(x; y) r(x; y).
Intuitively, the stable models of the above rules generate the di erent core interpretations Ic of the KB K = (T ; A) for any given A.
We next implement the algorithm Mark from Section 3. To obtain a
polynomially sized program, we need to use non-ground rules whose number of
variables depends on the number of di erent concept names in T . Assume an
arbitrary enumeration A1; : : : ; Ak of NC(T ). Assume also a pair 0; 1 of special
individuals. Intuitively, we will use a k-ary relation Type = f0; 1gk to store the
set of all types over T . Naturally, a k-tuple (a1; : : : ; ak) 2 Type encodes the type
= fAi j ai = 1; 1 i kg [ f>g. We are most interested in computing a
k-ary relation Marked f0; 1gk that contains precisely the types marked by the
Mark algorithm. We next de ne the rules to compute Type and Marked, and
other relevant relations.
(III) A linear order over types The rst ingredient is a linear order over
all possible types. To this end, for every 1 i k, we inductively de ne i-ary
relations rsti and lasti, and a 2i-ary relation nexti, which will provide the rst,
the last and the successor elements from a linear order on f0; 1gi. In particular,
given u; v 2 f0; 1gi, the fact nexti(u; v) will be true if v follows u in the ordering
of f0; 1gi. The rules to populate nexti are quite standard (see, e.g., Theorem 4.5
in [
1 we add the following rules: nexti+1(0; x; 0; y) nexti+1(1; x; 1; y) nexti+1(0; x; 1; y) rsti+1(0; x) lasti+1(1; x) nexti(x; y) nexti(x; y) lasti(x); rsti(y)
rsti(x) lasti(x) We can now collect in the k-ary relation Type all types over T (thus computing the set N of the Mark algorithm):
Type(x) rstk(x) (IV) Implementing Step (MN1) First, we add the auxiliary facts F(0) and T(1) to P . For a k-tuple of variables x, we let B 2 x denote the atom T (xj), where j is the index of B in the enumeration of NC(T ). Similarly, we let B 62 x denote the atom F (xj), where j is the index of B in the enumeration. Then the step (MN1), which marks types violating inclusions of type (N1), is implemented using the following rule for every inclusion A1 u u An v A01 t t A0m of T : Marked(x)
Type(x); A1 2 x; : : : ; An 2 x; A01 62 x; : : : ; A0m 62 x (V) Implementing Step (M9) The following rules are added for each inclusion = A v 9r:A0 2 T . Recall that we need to mark a type if A 2 , and for each type 0 at least one of (C0), (C10) or (C20) holds. We rst use an auxiliary (2k + 1) relation MarkedOne to collect all such types 0.
Assume a fresh individual a . For collecting each 0 that satis es (C0), we add:
MarkedOne(x; a ; y)
Type(x); Marked(y)
MarkedOne(x; a ; y)
Type(x); Type(y); A0 62 y
The rules for (C20) are as follows. For all inclusions A1 v 8r:A2 2 T with r v s 2 T , we add the rule
MarkedOne(x; a ; y)
Type(x); Type(y); A1 2 x; A2 62 y For all A1 v 8r:A2 2 T with r v s 2 T , we also add
MarkedOne(x; a ; y)
Type(x); Type(y); A1 2 y; A2 62 x
We infer Marked(t) in case MarkedOne(t; a ; v) is true for all types (bit vectors) v. To this end, we need another (2k + 1)-ary relation MarkedUntil. We add:
MarkedUntil(x; a ; z) MarkedUntil(x; a ; u)
MarkedOne(x; a ; z); rstk(z) MarkedUntil(x; a ; z); nextk(z; u);
MarkedOne(x; a ; u)
Intuitively, with the above rules we traverse all types checking the conditions (C0), (C10), (C20) described in (M9). If we manage to reach the last type, we know the condition is satis ed. We add the following rule:
Marked(x)
MarkedUntil(x; a ; z); A 2 x; lastk(z) (VI) Forbidding marked types in the core We need to forbid each individual in the generated core interpretation from having a type from Marked. For all 0 i k, we take a fresh (i + 1)-ary relation symbol Proji. We rst add: Projk(x; y)
ind(x); Marked(y) We will now project away bits from the Proji relations by looking at the actual types of individuals. For all 1 i k we have the following rules: Proji 1(x; y) Proji 1(x; y)
Proji(x; y; 1); Ai(x)
Proji(x; y; 0); Ai(x) Intuitively, Proji 1(a; b1; : : : ; bi 1) says the partial type given by the bit values b1; : : : ; bi 1 can be extended to a marked type by choosing additional concepts according to the actual type of the individual a. Thus the fact Proj0(a) represent the situation where a has a marked type. Such situations are ruled out by adding the constraint:
Proj0(x)
This concludes the translation of the instance query (T ; q), where T is an ALCHI TBox, into the disjunctive Datalog program P . This construction, together with Theorems 1 and 2, yields the main result of this paper. Theorem 3. For an instance query (T ; q), we can build in polynomial time a Datalog query (P; q) such that the certain answers to (T ; q) and (P; q) coincide for any given ABox A over the signature of T .
The above encoding employs disjunctive programs. Entailment of ground
atoms in such programs is coNExpTime-complete [
Since P1 has at most two-variables in every rule, each minimal model I1 of P1 [ F is of polynomial size in the size of P1 [ F , and the set of all such models can be traversed in polynomial space. For a given I1, performing the step (S2) is feasible in (deterministic) exponential time, because P2 is disjunction-free and of polynomial size in the size of the original instance query. It follows that computing the certain answers to (P; q) for any given ABox A over the signature of T requires single exponential time.
We have presented our results for ALCHI, but they also apply to SHI, its
extension with transitivity axioms; it is well known that instance queries mediated
by SHI TBoxes can be rewritten in polynomial time to instance queries mediated
by ALCHI TBoxes (see, e.g., [
As mentioned in the introduction, both the game theoretic characterization
and the Datalog translation can be extended to ontologies in ALCHOI, the
extension of ALCHI with nominals. This is possible even in the presence of
the so-called closed predicates, which are useful for combining complete and
incomplete knowledge, by explicitly specifying predicates assumed complete, thus
given a closed-world semantics [
BScStud v 8attends::GradCourse and the ABox A:
Course(c1), Course(c2), GradCourse(c2), BScStud(a) Then (a; c1) is not a certain answer to (T ; q) with q = attends(x; y). But if c1 and c2 are known to be the only courses, then (a; c1) should be a certain answer. This can be achieved by declaring Course a closed predicate: (a; c1) is indeed a certain answer to the OMQ with closed predicates (T ; ; q), where = fCourseg.
Interestingly, OMQs with closed predicates are non-monotonic. Indeed, (a; c1)
is a certain answer to (T ; ; q) over A, but it is not a certain answer over
the extended set of facts A0 = A [ fCourse(c3)g. For this reason, these queries
cannot be rewritten into monotonic variants of Datalog, like positive Datalog
with disjunction as considered here. However, one can devise a polynomial time
translation into disjunctive Datalog with negation as failure, for OMQs of the
form (T ; ; q) where T is an ALCHOI TBox, is a set of closed predicates, and
q is an instance query. The translation uses the same ideas presented here, but
handling closed predicates (both in the game-theoretic characterization, and in the
Datalog translation) implies reasoning about the types that are already realized
in the core; in Datalog, this requires negation. Details can be found in [
This work was supported by the Austrian Science Fund (FWF): projects P25207N23, T515 and W1255-N23. 21. C. Lutz, I. Seylan, and F. Wolter. Ontology-mediated queries with closed predicates.
In Proc. of IJCAI 2015. IJCAI/AAAI, 2015. 22. B. Motik, U. Sattler, and R. Studer. Query answering for OWL-DL with rules. J.
Web Sem., 3(1):41{60, 2005. 23. M. Ortiz, S. Rudolph, and M. Simkus. Worst-case optimal reasoning for the
Horn-DL fragments of OWL 1 and 2. In Proc. of KR 2010. AAAI Press, 2010. 24. H. Perez-Urbina, B. Motik, and I. Horrocks. Tractable query answering and rewriting under description logic constraints. J. Applied Logic, 8(2):186{209, 2010. 25. D. Trivela, G. Stoilos, A. Chortaras, and G. B. Stamou. Optimising resolution-based rewriting algorithms for OWL ontologies. J. Web Sem., 33:30{49, 2015.