The problem of exchanging knowledge bases from a source signature to a target signature connected through a mapping has recently attracted attention in knowledge representation. In this paper, we study this problem for knowledge bases and mappings expressed in OWL 2 QL, one of the profiles of the standard Web Ontology Language OWL 2. More specifically, we consider the membership and non-emptiness problems associated with computing universal solutions, which have been identified as one of the most desirable translations to be materialized. We study two settings: when ABoxes are in OWL 2 QL and when null values are allowed in the ABox language. For the former case, we provide a novel technique based on reachability games on graphs to show that the non-emptiness and membership problems are in PTime. For the latter case, we report a range of complexity results from NP to EXPTIME. We also consider the problem of computing universal UCQ-solutions, which provide an alternative notion of translation containing sufficient information to properly answer union of conjunctive queries, reporting a PSPACE lower bound for the membership problem.
Complex forms of information, maintained in different formats and organized according
to different structures, often need to be shared between agents. In recent years, both in
the data management and in the knowledge representation communities, several settings
have been investigated that address this problem from various perspectives: in
information integration, uniform access is provided to a collection of data sources by means of
an ontology (or global schema) to which the sources are mapped [
The work we present in this paper is inspired by the latter setting, investigated in
databases. We study it, however, under the assumption of incomplete information
typical of knowledge representation [
In this paper, we adjust the above mentioned framework to OWL 2 QL [
Then, we argue that for certain natural shapes of source KBs and mappings the universal solutions do not exist, unless null values are allowed in ABox languages. So, we consider extended ABoxes that may contain nulls, presenting a number of complexity results ranging from NP to EXPTIME for this setting.
Finally, we consider universal UCQ-solutions, an alternative notion for materialization of knowledge in the target that contains sufficient information to answer unions of conjunctive queries. We show that universal UCQ-solutions exist for certain source KBs and mappings, where universal solutions (even with extended ABoxes) do not. We also report PSPACE-hardness for the membership problem for universal UCQ-solutions.
The paper is organized as follows. We give preliminary notions on DLs and queries in Section 2, and on KB exchange in Section 3. In Section 4, we present the known results and give some intuition about the shape of universal solutions. In Sections 5 and 6, we present the results on the complexity of computing universal solutions for KBs and extended KBs, respectively. In Section 7, we consider universal UCQ-solutions and in Section 8, we present conclusions and outline some future work. 2
The DLs of the DL-Lite family [
R ::= P j P Q ::= R j :R
B ::= A j 9R C ::= B j :B Below, for a basic role R, we use R to denote P when R = P , and P when R = P .
A TBox is a finite set of concept inclusions B v C and role inclusions R v Q. We call an inclusion of the form B1 v :B2 or R1 v :R2 a disjointness assertion. An ABox is a finite set of membership assertions B(a), R(a; b), where a; b 2 Na. Here, we also consider extended ABoxes, obtained by allowing labeled nulls in membership assertions. Formally, an extended ABox is a finite set of membership assertions B(u) and R(u; v), where u; v 2 (Na [ N`). We denote by Ind(A) the set of constants occurring in A. Moreover, a(n extended) KB K is a pair hT ; Ai, where T is a TBox and A is an (extended) ABox. A signature is a finite set of concept and role names. A KB K is said to be defined over (or simply, over) if all the concept and role names occurring in K belong to (and likewise for TBoxes, ABoxes, concept inclusions, role inclusions, and membership assertions). An interpretation I of is a pair h I ; I i, where I is a non-empty domain and I is an interpretation function such that: (1) AI I , for every concept name A 2 ; (2) P I I I , for every role name P 2 ; and (3) aI 2 I , for every constant a 2 Na. Function I is extended to also interpret concept and role constructs: (1) (9R)I = fx 2 I j 9y 2 I such that (x; y) 2 RI g; (2) (:B)I = I n BI ; (3) (P )I = f(y; x) 2 I I j (x; y) 2 P I g; and (4) (:R)I = ( I I )nRI . Note that, consistently with the semantics of OWL 2 QL, we do not make the unique name assumption, i.e., distinct constants a; b 2 Na may be interpreted as the same object. Note also that labeled nulls are not interpreted by I.
Let I = h I ; I i be an interpretation over a signature . Then I is said to satisfy a concept inclusion B v C over , denoted by I j= B v C, if BI CI ; I is said to satisfy a role inclusion R v Q over , denoted by I j= R v Q, if RI QI ; and I is said to satisfy a TBox T over , denoted by I j= T , if I j= for every 2 T . Moreover, satisfaction of membership assertions over is defined as follows. A substitution over I is a function h : (Na [ N`) ! I such that h(a) = aI for every a 2 Na. Then I is said to satisfy an (extended) ABox A, denoted by I j= A, if there exists a substitution h over I such that: (1) for every B(u) 2 A, it holds that h(u) 2 BI ; and (2) for every R(u; v) 2 A, it holds that (h(u); h(v)) 2 RI . Finally, I is said to satisfy a(n extended) KB K = hT ; Ai, denoted by I j= K, if I j= T and I j= A. Such I is called a model of K, and we use MOD(K) to denote the set of all models of K. We say that K is consistent if MOD(K) 6= ;. As is customary, given an (extended) ABox A over a signature and a membership assertion over , we use notation A j= to indicate that for every interpretation I of , if I j= A, then I j= (and likewise for (extended) KBs).
We also need to introduce the notions of -types and -homomorphisms. For an interpretation I and a signature , the -types tI (x) and rI (x; y) for x; y 2 I are given by the set of concepts B and roles R over , respectively, such that x 2 BI and (x; y) 2 RI . We also use tI (x) and rI (x; y) to refer to the types over the signature of all DL-LiteR concepts and roles. A -homomorphism from an interpretation I to an interpretation J is a function h : I 7! J such that h(aI ) = aJ , for all individual names a interpreted in I, tI (x) tJ (h(x)) and rI (x; y) rJ (h(x); h(y)) for all x; y 2 I . We say that I is -homomorphically embeddable into J if there exists a -homomorphism from I to J . If is the set of all DL-LiteR concepts and roles, we call -homomorphism simply homomorphism.
DL-LiteR enjoys the canonical model property. Let K = hT ; Ai be a (nonextended) KB, and vTR the reflexive and transitive closure of the role relation on the set of all basic roles over NR induced by T (that is, the reflexive and transitive closure of f(R1; R2) j R1 v R2 2 T or R1 v R2 2 T g). Then define [R] = fS j R vTR S and S vTR Rg, [R] relationship K as follows: T [S] if R vTR S, and a generating – a K w[R], if (1) K j= 9R(a); (2) K 6j= R(a; b) for every b 2 Na; (3) [R0] = [R] for every [R0] such that [R0] T [R] and K j= 9R0(a). – w[S] K w[R], if (1) T j= 9S v 9R; (2) [S ] 6= [R]; (3) [R0] = [R] for every [R0] such that [R0] T [R] and T j= 9S v 9R0.
Denote by path(K) the set of all K-paths, where a K-path is a sequence aw[R1] : : : w[Rn] such that n 0, a 2 Na, a K w[R1] and w[Ri] K w[Ri+1] for 1 i n 1. Moreover, for every 2 path(K), denote by tail( ) the last element in . Finally, the canonical (or, universal) model of K, denoted UK, is defined as:
UK = path(K);
aUK = a; for a 2 Na;
AUK = fa 2 Ind(A) j K j= A(a)g [ f w[R] 2 UK j T j= 9R
P UK = f(a; b) 2 Ind(A) Ind(A) j K j= P (a; b)g [
f( ; w[R]) j tail( ) K w[R]; [R] T [P ]g [
f( w[R]; ) j tail( ) K w[R]; [R ] T [P ]g:
v Ag;
Theorem 1 ([
Queries and certain answers. A k-ary query q over a signature , with k 0, is a function that maps every interpretation h I ; I i of into a k-ary relation qI ( I )k. Given a (non-extended) KB K over , the set of certain answers to q over K, denoted by cert (q; K), is defined as: TI2MOD(K)f(a1; : : : ; ak) j fa1; : : : ; akg Na and (a1I ; : : : ; akI ) 2 qI g. A conjunctive query (CQ) over a signature is a formula of the form q(x) = 9y: '(x; y), where x, y are tuples of variables and '(x; y) is a conjunction of atoms of the form A(t), with A a concept name in , and P (t; t0), with P a role name in , where each of t; t0 is either a constant from Na or a variable from x or y. Given an interpretation I = h I ; I i of , the answer of q over I, denoted by qI , is the set of tuples a of elements from I for which there exist a tuple b of elements from I such that I satisfies every conjunct in '(a; b). A union of conjunctive queries (UCQ) over a signature is a formula of the form q(x) = Win=1 qi(x), where each qi (1 i n) is a CQ over , whose semantics is defined as qI = Sin=1 qiI . 3
Assume that 1, 2 are signatures with no concepts or roles in common. An inclusion
E1 v E2 is said to be from 1 to 2, if E1 is a concept or a role over 1 and E2 is
a concept or a role over 2. A mapping is a tuple M = ( 1; 2; T12), where T12 is
a TBox consisting of inclusions from 1 to 2 [
The main problem studied in the knowledge exchange area is the problem of
translating a KB according to a mapping, which is formalized through several different
notions of translation. Let M = ( 1; 2; T12) be a mapping, K1 = hT1; A1i a KB over
1 and K2 = hT2; A2i an extended KB over 2. The first such notion is the
concept of solution, which is formalized as follows: K2 is a solution for K1 under M if
MOD(K2) SATM(MOD(K1)). Thus, K2 is a solution for K1 under M if every
interpretation of K2 is a valid translation of an interpretation of K1 according to M. Then,
K2 is a universal solution for K1 under M if MOD(K2) = SATM(MOD(K1)). Thus,
K2 is designed to exactly represent the space of interpretations obtained by translating
the interpretations of K1 under M [
A second class of translations is obtained in [
Arguably, the most important problem in knowledge exchange [
In what follows, we show some known results and examples of universal solutions.
First of all, it was shown in [
Example 1. Assume that M = fA( ); B( )g; fA0( ); B0( )g, fA v A0; B v B0g , and let K1 = hT1; A1i, where T1 = fg and A1 = fA(a); B(b)g. Then the ABox A2 = fA0(a); B0(b)g is a straightforward universal solution for K1 under M.
It can be shown (c.f. Lemma 1) that in the language without disjointness assertions, an ABox A2 is a universal solution for hT1; A1i under M = ( 1; 2; T12) if and only if UA2 is 2-homomorphically equivalent to UhT1[T12;A1i. This fact is used in the following more involved example: Example 2. Assume M = fA( ); R( ; ); S( ; )g; 2; T12 where 2 = fQ( ; )g, T12 = fR v Q; S v Qg, and that K1 = hT1; A1i, where T1 = fA v 9R; 9R v 9Rg and A1 = fA(a); S(a; a)g. Let A2 = fQ(a; a)g. In the following picture, it is easy to see h is a 2-homomorphism from UhT1[T12;A1i to UA2 . The existence of a 2homomorphism in the other direction is trivial and, hence, A2 is a universal solution for K1 under M.
2-reduct of UhT1[T12;A1i
: UA2 :
Q Q a a aw[R] aw[R]w[R]
aw[R]w[R]w[R] Q
Q
Q h
The following example shows that extended ABoxes are necessary to guarantee the existence of universal solutions in certain cases.
Example 3. Assume that M = fA( ); R( ; )g; fB( )g, f9R v Bg , and let K1 = hT1; A1i, where T1 = fA v 9Rg and A1 = fA(a)g. Then the ABox A2 = fB(n)g, where n is a labeled null, is a universal solution for K1 under M if nulls are allowed. Notice that here, a universal solution with non-extended ABoxes does not exist: substituting n by any constant is too restrictive, ruining universality.
Finally, we discuss the impact of disjointness assertions on the universal solutions. Example 4. Consider Example 1 with T1 = fA v :Bg. With this seemingly harmless disjointness assertion A2 is no longer a universal solution (not even a solution) for K1 under M. The reason for that is the lack of the unique name assumption on the one hand, and the presence of the disjointness assertion in T1 that forces a and b to be interpreted differently in the source, on the other hand. Thus, for a model J of A2 such that aJ = bJ , A0J = B0J = faJ g, there is no model I of K1 such that (I; J ) j= T12 (hence, aI = aJ and bI = bJ ). In general, there is no universal solution for K1 under M, even though K1 and T12 are consistent with each other.
The problem raised by the latter example could be solved by allowing for inequalities between constants in the ABoxes. A similar problem appears with disjointness assertions in the mapping, but it requires negative facts to be present for a universal solution to exist (i.e., facts of the form :A(a); :P (a; b)), which are not part of OWL 2 QL. On the other hand, having disjointness assertion in the source or the mapping does not exclude the existence of universal UCQ-solutions, which is explained in Example 6. 5
In this section, we show that both the membership and the non-emptiness problems for universal solutions without null values are in PTIME.
Assume that 1, 2 are disjoint signatures, and that K = hT1 [ T12; A1i is a KB such that T1 is defined over 1 and T12 is a set of inclusions from 1 to 2. Moreover, let UK be the canonical model of K. Then a basic concept B over 1 is said to be safe in UK if d 62 Na and tUK2 (d) = ; for every d 2 BUK . Intuitively, safeness for B means no constant “associated” with B and no target concept that is “associated” with B via T1 and T12 will be mentioned in the target; in Example 4 neither A nor B is safe in UhT1[T12;A1i. Furthermore, a pair of basic concepts (B; C) is is said to be safe if B or C is safe. Intuitively, if a pair (B; C) is not safe and (B v :C) 2 T1, then universal solution cannot exist, as explained in Example 4. Similarly, we say a basic role R over 1 is safe if either d 62 Na and tUK2 (d) = ;, or d0 62 Na and tUK2 (d0) = ;, for every (d; d0) 2 RUK . A pair of roles (R; Q) is safe if 1) R or Q is safe, and 2) tUK2 (d0) = ; or tUK2 (d00) = ; for every d; d0; d00 2
UK such that (d; d0) 2 RUK and (d; d00) 2 QUK .
Lemma 1. A KB K2 = hT2; A2i over 2 is a universal solution for a KB K1 = hT1; A1i under a mapping M = ( 1; 2; T12) iff the following conditions hold: (tr) T2 is a trivial TBox, (hom) UA2 is 2- homomorphically equivalent to UhT1[T12;A1i, (ps1) each pair of concepts (B; C) is safe in UhT1[T12;A1i whenever (B v :C) 2 T1, (pm1) BUK = ; for each basic concept B such that (B v :B0) 2 T12, (ps2) each pair of roles (R; Q) is safe in UhT1[T12;A1i whenever (R v :Q) 2 T1, (pm2) RUK = ; for each basic role R such that (R v :R0) 2 T12.
It can be readily verified that conditions (tr), (ps1), (ps2), (pm1), (pm2) and the existence of a 2-homomorphism from UA2 to UhT1[T12;A1i required by (hom), are solvable in polynomial time. To solve the problem of existence of a 2-homomorphism in the opposite direction, we are going to employ the technique of reachability games on graphs. Below we present the required basic notions. 5.1
A game is defined by a game graph (a playground) and a winning condition. A game graph is a triple G = (S0; S1; T ), where S = S0 [S1 is a finite set of states, S0 \S1 = ; and T S S is a transition relation. The game starts in some state s0 2 S, and it is played in turns. In each turn, if the current state s is in Si (i = 0; 1), then Player i chooses some state s0 2 S such that (s; s0) 2 T . Thus, each play in the game is viewed as a path , which can be infinite ( = s0; s1; s2; : : :, where si 2 S and (si; si+1) 2 T for every i 0) or finite ( = s0; s1; s2; : : : ; sk 2 Sk+1, where (si; si+1) 2 T for every i 2 f0; : : : ; k 1g and fs j (sk; s) 2 T g = ;).
The winning condition defines what are the plays won by Player 0. We will consider a reachability acceptance condition specified as follows: given a set of accepting states F S, a play is a win for Player 0 iff some vertex from F occurs in . Finally, a reachability game is a pair G = (G; F ) where G is a game graph and F is a set of accepting states.
A strategy for Player 0 from state s is a (partial) function f0 : S S0 ! S such that it assigns to each sequence of states s0; s1; : : : ; sk with s0 = s and sk 2 S0, a successor state sk+1 such that (sk; sk+1) 2 T . A play = s0s1 is said to conform with strategy f0 if si+1 = f0(s0s1 : : : si) for every si 2 S0. Then, a strategy f0 is a winning strategy for Player 0 from s 2 S if every play that conforms with f0 and starts in s is a win for Player 0.
Proposition 1 ([
Assume given a mapping M = ( 1; 2; T12), a KB K1 = hT1; A1i over 1, and a KB K2 = h;; A2i over 2 (w.l.o.g., we can assume that the TBox of K2 is empty). Denote hT1 [ T12; A1i by K. We show how the problem of checking whether there exists a 2-homomorphism h from UK to UA2 can be reduced to the problem of existence of a winning strategy for Player 0 in a reachability game.
First, for such a homomorphism h to exist, it should be the case that tUK2 (a) tUA2 (a) and rUK2 (a; b) tUA2 (a; b) for all a; b 2 Ind(A1): (1) These conditions can be clearly checked in PTIME.
Now, to check how the elements a 2 UK with a 2 Ind(A1) can be mapped on UA2 , we construct a game Ga = (Ga; Fa). The game graph Ga = (S0; S1; T ) has the set of states of the kind (x; y; p), where x 2 UA2 , y 2 ftail(a ) j a 2 UK g, and p 2 fs; dg. The states (x; y; s) form S0 and will be called spoiling; intuitively, the moves going out of such states represent various edges of the tree UK accessible from the end of the current edge. On the other hand, the states (x; y; d) form S1 and will be called duplicating; the moves from them “show” how the “challenged” edge of the tree UK can be “mapped” on UA2 . Notice that the size of Ga is O(jT1 [ T12j jA2j). The transition relation T is defined as follows:
T = f (x; y; s); (x0; y0; d) j y
K y0 and x0 = xg [ f (x; y; d); (x0; y0; s) j y = w[R]; clT12[T12 (9R ) tUA2 (x0); clT12[T12 (R) rUA2 (x; x0); and y0 = yg; where for a TBox T and a concept B, clT (B) is the set of all concepts B0 over such that T j= B v B0, and for a role R, clT (R) is defined analogously.
The set Fa in the definition of the game is given by the duplicating states that are “dead ends”, i.e.,
Fa = f(x; y; d) j y = w[R] and for all x0 2 UA2 ; clT12[T12 (9R ) 6 tUA2 (x0) or Having constructed the game Ga = (Ga; Fa), we prove that verifying whether the elements a 2 UK can be 2-homomorphically mapped on UA2 reduces to checking whether Player 0 has a winning strategy in Ga from the state (a; a; s).
Lemma 2. There exists a 2-homomorphism from UK to UA2 iff (1) holds and for each a 2 Ind(A1), Player 0 does not have a winning strategy in Ga from (a; a; s).
The example below illustrates the presented reduction.
Example 5. Assume M = fR( ; ); S( ; ); Q( ; )g; 2; T12), where 2 = fR0( ; ), Q0( ; )g and T12 = fR v R0; S v R0; Q v Q0g , K1 = hT1; A1i, where T1 = f9S v 9R; 9R v 9Q; 9Q v 9Qg and A1 = f9R(a); 9S(a)g, and A2 = fR0(a; a); R0(a; b); Q0(b; b)g. Then Fa = f(b; wR; d); (a; wQ; d)g, and the game graph Ga is depicted in a) below (we ignore the states that are not reachable from (a; a; s); the duplicating states forming S1 are shown as ovals and the spoiling states forming S0 are shown as boxes). In b) below we show UK (the domain elements d 2 UK are shown as dots, the labels next to them represent tail(d), and the labels on the edges (d; d0) show the 2-role names P , such that (d; d0) 2 P UK ), in c) we show UA2 , and the dashed arrows from UK to UA2 show the homomorphism h. b; wS; s b; wR; d a; wS; d a; wS; s Fa a; a; s
W a; wR; d b; wR; s b; wQ; d b; wQ; s a; wR; s a; wQ; d wS wR wQ wQ
R0 Q0 Q0
a R0
R0
Q0 Q0 wR wQ wQ h
R0 a R0 b Q0 a) The game graph Ga b) 2-reduct of UhT1[T12;A1i c) UA2 Observe that in the game Ga Player 0 does not have a winning strategy from (a; a; s), because there is a way for Player 1 to play (infinitely) so that the game never goes out of the region W shown in a). It is not difficult to see that such strategy of Player 1 can be used to define the homomorphism h, and vice versa.
Finally, combining Lemma 2, Lemma 1 and Proposition 1 one obtains: Theorem 2. The membership problem for universal solutions with (non-extended) KBs is in PTIME.
We conclude this section by addressing the non-emptiness problem. It follows from Conditions (tr), (hom) that there exists a universal solution for K1 under M iff K2 = h;; A2i over 2 is a universal solution for K1 under M, where A2 satisfies (i) A2 j= B(a) iff K j= B(a) and (ii) A2 j= R(a; b) iff K j= R(a; b) for all a; b 2 Ind(A1 [ A2), 2-concept B, and 2-role R. Obviously, we can construct the required A2 in PTIME, then it remains to check if K2 above is a universal solution. It follows: Theorem 3. The non-emptiness problem for universal solutions with (non-extended) KBs is in PTIME. Moreover, there is an effective algorithm to compute a universal solution in polynomial time (if such a solution exists). 6
We start with the membership problem for extended KBs. Assume given a mapping M = ( 1, 2, T12), a KB K1 = hT1; A1i over 1, and a KB K2 = h;; A2i over 2, where A2 is an extended ABox. It can be shown that an analogue of Lemma 1 holds, provided that the definition of UA2 is adjusted in an obvious way to account for nulls, and so is the definition of homomorphism. In this setting, 2-homomorphism from UhT1[T12;A1i to UA2 can be still checked in PTIME, however, the opposite direction cannot be checked efficiently due to nulls in A2. In fact, it can be shown by reduction from the graph 3-colorability problem that the membership problem for universal solutions with null values is NP-hard. To decide in NP whether there exists a homomorphism h from UA2 to UhT1[T12;A1i, we can use the fact that the image W UhT1[T12;A1i of such a function h on UA2 is of polynomial size. Therefore, for each constant and null in A2, one needs to guess its homomorphic image, and then check whether the resulting function is a homomorphism. Thus, we obtain: Theorem 4. The membership problem for universal solutions with extended KBs is NP-complete.
Consider now the problem of checking whether there exists a universal solution
K2 = h;; A2i for K1 under M. This problem turns out to be harder than the
membership problem as now candidate solutions are not part of the input. In fact, we show by
reduction from the validity problem for quantified Boolean formulas that checking the
existence of a universal solution is PSPACE-hard. As for the upper bound, first, it can be
shown that such an A2 exists if and only if UhT1[T12;A1i is 2-homomorphically
embeddable into a finite part of itself. Then, such a finite subset of UhT1[T12;A1i projected
on 2 can be taken as a universal solution for K1 under M. As the inclusion of inverse
roles is one of the main sources of complexity, we use two-way alternating automata on
infinite trees (2ATA), which are a generalization of nondeterministic automata on infinite
trees [
K labeled with G corresponds to a tree model I of K (that is, a model forming a tree on the labeled nulls); and (3) A n is a (one-way) non-deterministic automaton that accepts a tree if it has a finite prefix where each node is marked with G, and no other node in the tree is marked with G. Then to verify whether a KB K1 = hT1; A1i has a universal solution under a mapping M = ( 1; 2; T12), we solve the non-emptiness problem for an automaton B defined as the product automaton of K (Acan ), K (AKmod ) and A n , where K = hT1 [T12; A1i, K (AcKan ) is the projection of AKcan on a vocabulary K not mentioning symbols from 1, and likewise for K (AKmod )K. If the language accepted Universal solutions ABoxes Extended ABoxes Membership PTIME NP-complete Non-emptiness PTIME PSPACE-hard, in EXPTIME by B is empty, then there is no universal solution for K1 under M, otherwise a universal solution (of exponential size) exists and it can be extracted from the tree accepted by B. Theorem 5. The non-emptiness problem for universal solutions with extended KBs is PSPACE-hard and in EXPTIME. Moreover, there is an effective algorithm to compute a universal solution in exponential time (if such a solution exists). 7
We start by arguing that universal UCQ-solutions exhibit more robust behavior in the presence of disjointness assertions than universal solutions.
Example 6. Consider M, K1, and A2 from Example 4. Recall that A2 is not a universal solution for K1 under M. However, A2 is a universal UCQ-solution for K1 under M. Moreover, A2 remains a universal UCQ-solution for K1 under M independently of whether the unique name assumption is employed.
Unfortunately, universal UCQ-solutions are also harder to compute, which can be
explained by the fact that TBoxes have bigger impact on the structure of universal
UCQsolutions rather than of universal solutions. In fact, by using a reduction from the
validity problem for quantified Boolean formulas, similar to a reduction in [
A summary of our results for universal solutions is presented in Figure 1.
In this paper, we have studied the problem of KB exchange for OWL 2 QL, improving on previously known results both w.r.t. the expressiveness of the ontology language and w.r.t. the understanding of the computational properties of the problem. Our main contribution is a novel PTIME algorithm for the membership and non-emptiness problems for universal solutions when OWL 2 QL ABoxes are considered. Our investigation leaves open several issues, which we intend to address in the future. For the computation of universal solutions when extended ABoxes are allowed, while we have pinned-down the complexity of the membership problem as NP-complete, an exact characterization for the non-emptiness problem is still missing. Moreover, it is easy to see that allowing for inequalities between terms and for negated atoms in the (target) ABox would allow one to obtain more universal solutions, but a full understanding of this case is still missing. Finally, we intend to investigate the challenging problem of computing universal UCQ-solutions, adopting also here an automata-based approach.