Query Extensions and Incremental Query Rewriting for OWL 2 QL Ontologies

Abstract

Query rewriting over lightweight ontologies, like DL-Lite ontologies, is a prominent approach for ontology-based data access. It is often the case in realistic scenarios that users ask an initial query which they later refine, e.g., by extending it with new constraints making their initial request more precise. So far, all DL-Lite systems would need to process the new query from scratch. In this paper, we study the problem of computing the rewriting of an extended query by ‘extending’ a previously computed rewriting of the initial query and avoiding recomputation. Interestingly, our approach also implies a novel algorithm for computing the rewriting of a fixed query. More precisely, the query can be ‘decomposed’ into its atoms and then each atom can be processed incrementally. We present detailed algorithms, several optimisations for improving the performance of our query rewriting algorithm, and finally, an experimental evaluation.

1 Introduction

Efficiently managing and retrieving large amounts of data is a key problem for many modern applications. Ontologies expressed in the W3C’s Web Ontology Language OWL [15] and its revision OWL 2 [10] are often used for providing a formal and unified schema that describes the data that are stored in distributed and/or heterogeneous data sources. A key application for such systems is ontology-based data access (OBDA) [29], where answers to user queries reflect both the data as well as the ontology that describes them. However, reasoning and conjunctive query (CQ) answering in the ontology languages OWL 2 DL, OWL DL, and OWL Lite is of very high computational complexity in the worst case [20, 25]. Actually, no complete algorithm for querying OWL 2 DL ontologies is currently known.

The need for efficient query answering has motivated the development of many lightweight ontology languages which provide reasoning services of at most polynomial data complexity. One such language is DL-Lite [2, 8]. DL-Lite forms the logical underpinnings of the ontology language OWL 2 QL, a well-known profile of OWL 2 [23]. Query answering in DL-Lite is usually performed via a technique called query rewriting [2, 8, 28]. According to this technique a query $q$ and a DL-Lite ontology are transformed into another query $q^{\prime }$, called a rewriting, such that the answers of $q^{\prime }$ over the input data and discarding the ontology are precisely the answers of $q$ over the data and the ontology. Common target languages for representing rewritings in DL-Lite are non-recursive Datalog [13, 32] or union of conjunctive queries (UCQs) [8, 9, 27].

The nice properties of DL-Lite have motivated the development of many algorithms and systems for computing a rewriting, such as QuOnto [1], Requiem [27], Presto [32], Nyaya [11], Quest [30] and Rapid [9]. For a given query most of these systems will compute a rewriting by applying (usually in a brute-force manner) a certain set of equivalence-preserving transformations to the query discarding any information computed for previously rewritten queries. However, it is quite often the case that user queries have very small differences with previously executed ones. For example, in Web search scenarios, it has been shown that users usually first ask some ‘general’ query and then, according to the returned results, they refine it by adding further constraints making their request more precise [16, 17, 26]. Consequently, a query can be refined several times until the user (possibly) finds the intended information.

For example, a user might initially ask to retrieve from a student database all those students who are athletes using the following conjunctive query:

$$\begin{aligned} \{{x}\mid \mathsf{Student }(x), \mathsf{Athlete }(x) \} \end{aligned}$$

where $x$ is a variable that needs to be replaced with actual students from the database while $\mathsf{Student }$ and $\mathsf{Athlete }$ are concept atoms (unary predicates). Then, the user can refine the search by requesting only those athletes who are female by extending the previous query with the new concept atom $\mathsf{Female }(x)$ giving raise to the following query:

$$\begin{aligned} \{{x}\mid \mathsf{Student }(x), \mathsf{Athlete }(x), \mathsf{Female }(x) \}. \end{aligned}$$

Finally, the new query can be further extended requesting only those female athlete students who take a specific course. This can be done by adding the role atom (binary predicate) $\mathsf{takesCourse }(x,y)$. In all these cases all aforementioned DL-Lite systems would compute a rewriting for the extended queries by running their algorithm each time from scratch discarding any information computed during previous runs. However, due to the overlap between the queries much of the previously computed information would need to be re-computed by each system.

In the current paper, we study the problem of computing a rewriting for queries that have been extended with new atoms. More precisely, given a DL-Lite ontology, a query, a rewriting computed (possibly previously) for this query and a new atom that would extend the original one, we study how to compute a rewriting for the new query by “extending” the input rewriting and avoid computing one from scratch. We study the problem theoretically and design a detailed practical algorithm. Roughly speaking, the algorithm computes a rewriting for a query that is relevant only to the newly added atom and then combines this with the input rewriting using proper operations. This way the algorithm performs only the additional work that is required to compute a rewriting for the extended query.

Interestingly, our techniques for rewriting extended queries imply a novel approach for computing a rewriting for fixed queries. More precisely, given a (fixed) query one can pick one of its atoms compute a rewriting for it and then iteratively add the rest of the atoms by extending the previously computed rewriting. When all the atoms of the input query have been processed a rewriting for the given query would have been computed. Based on this idea, we present a detailed query rewriting algorithm for conjunctive queries over DL-Lite ontologies. Subsequently, in order to improve its efficiency we also present several novel optimisations.

Finally, we have implemented all the proposed algorithms and we have conducted an extensive experimental evaluation comparing our algorithms against several available state-of-the-art rewriting systems. The evaluation shows that computing a rewriting incrementally is in the vast majority of cases faster than the currently fastest DL-Lite system. Especially, the comparison with the original DL-Lite algorithm [8] with which our algorithm shares many common features showed that the new algorithm is several orders of magnitude faster. This can be justified by the more guided rewriting strategy that processes each atom at a time in contrast to the brute-force approach followed by most existing systems. In summary, our paper makes the following major contributions:

• It studies the problem of computing a rewriting for queries that have been extended with new atoms given a rewriting for them.

• It shows how the reduction step of the original algorithm for DL-Lite [8] can be optimised in order to avoid an exponential blow-up of redundant queries.

• It presents a novel query rewriting algorithm that incrementally processes the atoms of the query.

• It presents several optimisations by which the performance of the incremental query rewriting algorithm can be significantly improved.

• It provides an extensive experimental evaluation of the proposed algorithms, also contrasting them with existing state-of-the-art query rewriting systems.

Besides the immediate practical benefits, our study has several theoretical consequences and gives many interesting opportunities for future research. First, it shows that rewriting in DL-Lite can largely be performed in parallel. That is, one can complete all “rewriting” work for each atom independently and then combine the results without referring to the rewriting module again. To the best of our knowledge, this is the first complete and practical algorithm for query rewriting that is based on this approach. Second, the experimental evaluation shows that with relatively few optimisations incremental rewriting behaves very well in practice. Hence, it would be interesting to apply such a strategy over other ontology languages such as Linear-Datalog$^\pm$ [11] or OWL 2 EL [23].

2 Preliminaries

In this section, we first briefly recall some notions from graph theory. Then, we present the Description Logic $\text{ DL-Lite}_{R}$ [8], a lightweight knowledge representation formalism which consists of the logical underpinnings of the ontology language OWL 2 QL. Subsequently, we define the syntax and semantics of conjunctive queries and unions of conjunctive queries and finally, we provide a brief overview of the so-called $\mathsf{PerfectRef }$ query rewriting algorithm for $\text{ DL-Lite}_{R}$ ontologies [8].

2.1 Directed Graphs

A (directed) graph is a tuple $G=\langle V , E \rangle$, where $V$ is a set of vertices and $E\subseteq V\times V$ is a binary relation over $V$. We often abuse notation and use $G$ to refer to the set of edges of the graph; in that case it is understood that $V$ is exactly the set of endpoints of elements of $E$. Hence, adding a pair $\langle a , b \rangle$ to $G$ creates a new graph $G=\langle V\cup \{a,b\} , E\cup \{\langle a , b \rangle \} \rangle$.

For $a,b\in V$, we say that $b$ is reachable from $a$ in $G$, written $a\rightsquigarrow _G b$, if ${c_0, \ldots , c_n}$ with $n \ge 0$ exist where ${c_0 = a}$, ${c_n = b}$ and ${\langle c_i , c_{i+1} \rangle \in E}$ for each ${0 \le i < n}$. Note that, according to this definition, each $c \in V$ is reachable from itself. Finally, an element $c\in V$ is called top in $G$ if for each $c^{\prime }\in V$ we have $c \rightsquigarrow _G c^{\prime }$.

2.2 The $\text{ DL-Lite}_R$ language

A $\text{ DL-Lite}_R$ signature is the disjoint union of a countably infinite set $\mathbf C$ of atomic concepts (unary predicates), $\mathbf R$ of atomic roles (binary predicates) and $\mathbf I$ of individuals (constants). A $\text{ DL-Lite}_R$-role is either an atomic role $P\in \mathbf R$ or its inverse $P^-$. Let $A\in \mathbf C$ be an atomic concept and $R$ a $\text{ DL-Lite}_R$-role; then, a $\text{ DL-Lite}_R$ -concept is either an atomic concept $A$ or a concept of the form $\exists R$.

Let $B_i$ be $\text{ DL-Lite}_R$-concepts and $R_i$ be $\text{ DL-Lite}_R$-roles. A $\text{ DL-Lite}_R$-TBox, denoted by $\mathcal T$, is a finite set of axioms of one the following forms:

$$\begin{aligned} B_{1}\sqsubseteq B_{2} \qquad R_{1}\sqsubseteq R_{2} \end{aligned}$$

An ABox is a finite set of assertions of the form $A(c)$ or $P(c,d)$ for $A\in \mathbf C$, $P\in \mathbf R$ and $c,d\in \mathbf I$. A $\text{ DL-Lite}_R$-ontology $\mathcal O =\mathcal T \cup \mathcal A$ is the union of a TBox and an ABox.¹ In the following, since we are concerned with a particular DL language, we simply speak of roles, concepts, TBoxes, and ABoxes referring only to those expressible in $\text{ DL-Lite}_R$.

$\text{ DL-Lite}_R$ can be seen as a fragment of First-Order Logic (FOL); thus, it can be given formal semantics via a translation to FOL, where concepts are translated into formulae with one free variable, roles into formulae with two free variables, axioms into FO-sentences, and TBoxes, ABoxes and ontologies into FO-sentences. The transformation $\pi (\cdot )$ for axioms and ontologies is given in Table 1, while the translation of concepts is defined as given in Table 2.

Table 1 The translation of $\text{ DL-Lite}_R$-axioms and ontologies into FOL sentences. Note that, $B$ is a concept, $R$ is a role, and $a,b$ are individuals.

Table 2 The translation into FOL formulas

An ontology $\mathcal O$ is consistent if $\pi (\mathcal O )$ has a model, while entailment ($\models$) is defined as usual in FOL.

2.3 Conjunctive Queries

We use standard notions of (function-free) term, variable and substitution from First-Order Logic. For $\alpha$ an atom and $\sigma$ a substitution, the result of applying $\sigma$ to $\alpha$ is denoted as $\alpha _\sigma$. Moreover, we use the notation $\mathsf{dom }(\sigma )$ to denote the domain of a substitution $\sigma$. Furthermore, every substitution $\sigma$ induces a directed graph $G=\langle V,E\rangle$, where $t\in V$ iff $t$ is a term in $\sigma$ and $\langle x,t\rangle \in E$ iff $x\mapsto t\in \sigma$.

A concept atom is of the form $A(t)$ with $A$ an atomic concept and $t$ a term. A role atom is of the form $R(t,t^{\prime })$ for $R$ an atomic role, and $t,t^{\prime }$ terms. A conjunctive query (CQ) $q$ is an expression of the form:

$$\begin{aligned} \{\varvec{x}\mid \, {\alpha _1, \ldots , \alpha _m}\} \end{aligned}$$

where $\varvec{x}=(x_1,\ldots ,x_n)$ is a tuple of variables called distinguished (or answer) and each $\alpha _i$ is a concept or role atom called body atom. Each distinguished variable appears in at least some atom $\alpha _i$; all other variables of the query are called undistinguished. A variable that is either distinguished or appears in at least two different atoms $\alpha _i,\alpha _j$ with $i\ne j$ in $q$ is called bound, otherwise it is called unbound. For an atom $\alpha$, we use $\mathsf{var }(\alpha )$ to denote the set of its variables; $\mathsf{var }$ can be extended to queries in the obvious way. Moreover, by $\mathsf{avar }(q)$ we denote all the distinguished variables of $q$. Finally, a union of conjunctive queries (UCQ) is a set of CQs.

For a query $q$, we will often abuse notation and use $q$ to refer to the set $\{\alpha _1,\ldots ,\alpha _m\}$ of its body atoms. Hence, for $\beta$ an atom by $q$ $\cup$ $\{\beta \}$ we denote the new $CQ$ of the form $\{\mathsf{avar }(q) \mid {\alpha _1,\ldots ,\alpha _m,\beta }\}$.

Given CQs $q_1,q_2$ with distinguished variables $\varvec{x}$ and $\varvec{y}$, respectively, we say that $q_2$ subsumes $q_1$ (or that $q_2$ is a subsumer of $q_1$), if there exists a substitution $\sigma$ from $\mathsf{var }(q_2)$ to $\mathsf{var }(q_1)$ such that $[\{Q(\varvec{y})\}\cup q_2]_\sigma$ is a subset of $\{Q(\varvec{x})\}\cup q_1$, where $Q$ is a predicate of the same arity as $\varvec{x}$ $(\varvec{y})$ that does not appear in $q_1$ and $q_2$. For a UCQ $u$ and CQ $q$, we say that $q$ is redundant in $u$ if another query $q^{\prime }$ in $u$ exists that subsumes $q$; otherwise it is called non-redundant in $u$.

A certain answer to a CQ $q$ with respect to an ontology $\mathcal O$ is a tuple $\varvec{c} = (c_1, \ldots , c_n)$ of individuals such that $\mathcal O$ entails the FOL formula obtained by building the conjunction of all atoms $\alpha _i$ in $q$, replacing each distinguished variable $x_j$ with $c_j$ and existentially quantifying over undistinguished variables. We denote with $\mathsf{cert }(q,\mathcal{O })$ the set of all certain answers to $q$ w.r.t. $\mathcal O$.

W.l.o.g. we assume that CQs are connected. More precisely, let $q$ be a CQ. We say that $q$ is connected if, for all terms $t, t^{\prime }$, there exists a sequence $t_1 , \ldots , t_n$ such that $t_1 = t$, $t_n = t^{\prime }$ and, for all $1 \le i < n$, there exists a role $R$ such that $R(t_i, t_{i+1}) \in q$.

2.4 Query Answering and Rewriting for $\text{ DL-Lite}_R$

Query answering over DL-Lite-ontologies is performed with a technique known as query rewriting [8, 28]. Given a TBox $\mathcal T$ and query $q$, the technique computes another query $q^{\prime }$, called a rewriting for $q,\mathcal T$, with the following property: for each ABox $\mathcal A$ such that $\mathcal O =\mathcal T \cup \mathcal A$ is consistent we have:

$$\begin{aligned} \mathsf{cert }(q,\mathcal{O })=\mathsf{cert }(q^{\prime }, \mathcal{A }) \end{aligned}$$

(1)

Query rewriting has been extensively used for query answering over “lightweight” ontologies [8, 9, 32]. A rewriting can be computed by applying certain transformations over the input TBox $\mathcal T$ and query $q$. Several techniques and algorithms have been proposed so far in the literature [8, 9, 11, 19, 28, 32] and many of them differ quite substantially from each other. For example, several techniques have proposed the use of non-recursive Datalog for representing the rewriting $q^{\prime }$ [13, 32], while others return $q^{\prime }$ in its equivalent disjunctive normal form—that is, as a union of conjunctive queries $u$ which we next call a UCQ rewriting for $q,\mathcal T$. Non-recursive Datalog provides a more compact (polynomial size) structure for computing rewritings in contrast to the worst case exponential size of UCQs [18]. However, it has been advocated [31] that UCQs provide a more suitable form when it comes to actually evaluating the computed rewriting over the stored data. In addition, recent optimisation techniques show how the structure of the data (structure of the ABox) can be used to significantly reduce the size of the UCQ [30, 31].

Next, we briefly present the $\mathsf{PerfectRef }$ algorithm proposed by Calvanese et al. [8] as our algorithm uses several of its techniques. Given a CQ $q$ and a TBox $\mathcal T$, $\mathsf{PerfectRef }$ computes a UCQ rewriting for $q,\mathcal T$, by applying exhaustively a reformulation and reduction step. Each one of them takes as input a CQ and possibly some axiom from $\mathcal T$ and generates a new CQ. This process terminates when no new query is generated.

In the reformulation step the algorithm picks a CQ $q$, an atom $\alpha$ in the CQ and an axiom $I$ in $\mathcal T$ and checks whether $I$ can be used to replace $\alpha$ in $q$ with a new atom, hence creating a new CQ. For example, for the CQ $q_1=\{{x}\mid {S(x,y),S(y,z)}\}$ and the axiom $I_1=B\sqsubseteq \exists S$ reformulation would replace $S(y,z)$ producing a new query $q_2=\{{x}\mid {S(x,y),B(y)}\}$. Next, if an axiom of the form $I_2=\exists S^-\sqsubseteq B$ exists in $\mathcal T$ then this can also be used to replace $B(y)$ in $q_2$ producing the query $q_3=\{{x}\mid {S(x,y),S(w,y)}\}$, where $w$ is a new variable not appearing in $q_2$. More formally, for an atom $\alpha$ of a query and an axiom $I\in \mathcal T$, the function $\mathsf{gr }(\alpha ,I)$ returns a new atom as defined in Table 3. If for some axiom $I$ and some atom $\alpha$ one of the conditions in Table 3 holds, then we say that $I$ is applicable to $\alpha$, and applying $I$ to some $\alpha$ in some CQ $q$ creates a new CQ of the form $q[\alpha /\mathsf{gr }(\alpha ,I)]$—that is, a new query that contains the atom $\mathsf{gr } (\alpha ,I)$ instead of the atom $\alpha$.

Table 3 Function $\mathsf{gr }$ defined for an atom $\alpha$ and an axiom $I$

In the reduction step a new CQ is generated by applying to some CQ $q$ the most general unifier (mgu) of two of its atoms. For example, applying reduction on query $q_3$ from above generates the new query $q_4=\{{x}\mid {S(x,y)}\}$, since $S(w,y)$ unifies with $S(x,y)$.

3 Rewriting Under Atom Extensions

In this section, we study the problem of computing a UCQ rewriting for queries that have been extended with new atoms, by extending a previously computed UCQ rewriting for them. First, we provide an overview of the algorithm emphasising several of its technical points, after which we present the algorithm in detail.

3.1 An Overview

Consider the following TBox about an academic domain and the CQ which retrieves all individuals that teach someone:

$$\begin{aligned} \mathcal T&= \{\mathsf{Professor } \sqsubseteq \exists \mathsf{teaches },\;\exists \mathsf{teaches }^-\sqsubseteq \mathsf{Student }\}\\ q&= \{{x}\mid {\mathsf{teaches }(x,y)}\} \end{aligned}$$

The following set is a UCQ rewriting for $q,\mathcal T$ computed using the $\mathsf{PerfectRef }$ algorithm:

$$\begin{aligned} u=\{q, q_1\},&\; \text{ where} \;&q_1 = \{{x}\mid {\mathsf{Professor }(x)}\}. \end{aligned}$$

More precisely, $q_1$ is produced by applying the first TBox axiom on atom $\mathsf{teaches }(x,y)$ of $q$, replacing it with $\mathsf{Professor }(x)$.

Suppose now, that the initial query is extended in order to retrieve only individuals that teach students—that is, $q$ is extended with atom $\alpha = \mathsf{Student }(y)$ and the new query is the following:

$$\begin{aligned} q^{\prime }=\{{x}\mid {\mathsf{teaches }(x,y),\mathsf{Student }(y)}\}. \end{aligned}$$

Again, using the $\mathsf{PerfectRef }$ algorithm, we can compute the following UCQ rewriting for $q^{\prime },\mathcal T$:

$$\begin{aligned} u^{\prime }=\{q^{\prime },q^{\prime }_1,q,q_1\} \end{aligned}$$

where $q^{\prime },q$, and $q_1$ are as defined previously, and $q^{\prime }_1 =\{{x}\mid \mathsf{teaches }(x,y),\mathsf{teaches(z,y) }\}$. More precisely, $q^{\prime }_1$ is obtained from $q^{\prime }$ by applying the second TBox axiom on atom $\mathsf{Student }(y)$, replacing it with $\mathsf{teaches }(z,y)$ for $z$ a fresh variable, while $q$ is obtained from $q^{\prime }_1$ by applying reduction on its two atoms. Note that variable $y$ in query $q^{\prime }_1$ is bound since it appears in both atoms $\mathsf{teaches }(x,y)$ and $\mathsf{teaches }(z,y)$, while after reduction it becomes unbound. Hence, finally, the algorithm can produce query $q_1$ from $q$ as shown earlier.

From the above example, we can observe that when run for $q^{\prime },\mathcal T$, the $\mathsf{PerfectRef }$ algorithm has to recompute queries $q$ and $q_1$, although these have been computed previously for $q,\mathcal T$. To avoid repeating this work it would be beneficial to perform any rewriting work only for the newly added atom and then appropriately ‘combine’ the result with the previously computed rewriting (which in the following we informally call reference rewriting).

Consider the query $q_\alpha =\{{y}\mid {\mathsf{Student }(y)}\}$. The set $u_\alpha =\{q_\alpha ,q^{\prime }_\alpha \}$, where $q^{\prime }_\alpha =\{{y}\mid {\mathsf{teaches }(z,y)}\}$ for $z$ a fresh variable, is a UCQ rewriting for $q_\alpha ,\mathcal T$ computed using the $\mathsf{PerfectRef }$ algorithm. It can be easily seen that query $q^{\prime }$ of $u^{\prime }$ can be constructed by adding the atoms of $q_\alpha$ to $q$ (which has been computed previously in $u$), while query $q^{\prime }_1$ can also be constructed by adding the atoms of $q^{\prime }_\alpha$ to $q$. However, note that adding the atoms of $q_\alpha$ to $q_1\in u$ creates the CQ $\{{x}\mid {\mathsf{Professor }(x),\mathsf{Student }(y)}\}$ which is not part of $u^{\prime }$.

The above considerations suggest that given a rewriting $u$ for $q,\mathcal T$ and an atom $\alpha$, a rewriting for $q\cup \{\alpha \},\mathcal T$ can be computed by computing a rewriting $u_\alpha$ for a ‘special’ query $q_\alpha$ and then properly extending the CQs in $u$ with the body atoms of queries from $u_\alpha$. More precisely, for $\alpha ,u,q$ and $\mathcal T$ the algorithm will compute a UCQ rewriting $u_\alpha$ for the query $q_\alpha =\{{\mathsf{var }(\alpha )\cap \mathsf{var }(q)}\}{\alpha }$ and then add the atoms of a query $q^{\prime }_\alpha \in u_\alpha$ to the atoms of a query $q^{\prime }\in u$ if $\mathsf{avar }(q^{\prime }_\alpha )\subseteq \mathsf{var }(q^{\prime })$.

Intuitively, the above approach is possible because the $\mathsf{PerfectRef }$ algorithm is to a large extent ‘local’ with respect to the atoms of a query. For example, the application of the reformulation step on some query atom is independent from the rest of the query atoms. Unfortunately, the second operation of the $\mathsf{PerfectRef }$ algorithm, that of reduction, involves more than one atoms in the query and hence refutes our independence argument. A straightforward approach would be to also use reduction between queries from the two rewritings. In our running example, atom $\mathsf{teaches }(x,y)$ in query $q$ unifies with atom $\mathsf{teaches }(z,y)$ in query $q^{\prime }_\alpha$. The result of unifying these two queries indeed produces the CQ $q$ of $u^{\prime }$. However, this approach has two issues. First, it is well-known that, in terms of performance, reduction is an inefficient step that can create a large number of (possibly redundant) queries [12, 28, 32]. Second, even with this operation we still cannot produce query $q_1\in u^{\prime }$.

The reduction step was initially introduced because an axiom $I$ might only be applicable to a reduction of some CQ. In our running example, $q_1$ is produced from $q$ because variable $y$ that was bound in $q^{\prime }_1$ became unbound in $q$ after reduction. An advantage in our case is that we already know from the reference rewriting that $q_1$ can be produced from $q$. Hence, our algorithm only needs to check whether some CQ in $u_\alpha$ can be ‘unified’ into $q$ in such a way that all queries that are produced due to $q$ in the reference rewriting can still be produced without producing all possible unifications. If such a query exists, then $q$ and all queries ‘produced by’ $q$ (in our case $q_1$) should be part of the result. The algorithm presented in the next section identifies such cases using the function $\mathsf{mergeCQs }$ defined next.

Definition1

Let $q, q^{\prime }$ be two queries. Then, function $\mathsf{mergeCQs } ({q^{\prime }},{q})$ returns the smallest set $\Sigma$ of substitutions such that:

• If there exists atom $\alpha \in q^{\prime }\cap q$, then $\Sigma$ contains $\{x\mapsto x\mid x\in \mathsf{var }(\alpha )\}$;

• If there exist $R(z,y)\in q^{\prime },R(x,y)\in q$ or $R(y,z)\in q^{\prime },R(y,x)\in q$ and $x,y,z$ are all distinct, then $\Sigma$ contains $\{z\mapsto x\}$.

 

Note that, our restricted reduction approach is similar to the factorisation step proposed by Gottlob et al. [11]. However, since DL-Lite only allows for predicates with at most two variables (cf. FO translation in Table 2) the checks we need to perform (i.e., the ones of Definition 1) are much more tailor made and lightweight. Whereas, to implement the factorisation step one has to check applicability of certain TBox axioms over an atom, that is, try to actually apply a rewriting step.

As the next example shows, the substitutions returned by function $\mathsf{mergeCQs }$ indicate how a query can be merged into another one and this is key to our algorithm.

Example 1

Consider the following TBox and CQ:

$$\begin{aligned} \mathcal T = \{A \sqsubseteq _{} \exists R\} \quad q = \{{x}\mid {R(x,y)}\} \end{aligned}$$

with the UCQ rewriting:

$$\begin{aligned} u=\{q, q_1 \}, \quad \text{ where} \quad q_1 =\{{x}\mid {A(x)}\}. \end{aligned}$$

Consider now that we extend $q$ with atom $\alpha _1=R(z,y)$ and that we want to compute a UCQ rewriting for $q^{\prime } =q\cup \{R(z,y)\}$ and $\mathcal T$ using the approach described earlier. First, we construct $q_{\alpha _1}=\{{y}\mid {R(z,y)}\}$ since $y$ is the only variable in $\mathsf{var }(a)\cap \mathsf{var }(q)$ and then the UCQ rewriting $u_{\alpha _1}=\{q_{\alpha _1}\}$ for $q_{\alpha _1},\mathcal T$. Finally, a UCQ $u^{\prime }$ is computed as follows: The atoms of $q_{\alpha _1}$ are added to $q$ creating the CQ $q^{\prime }=q\cup \{R(z,y)\}$, while query $q_{\alpha _1}$ merges into $q$ since $\mathsf{mergeCQs } ({q_{\alpha _1}},{q})$ contains $\{z\mapsto x\}$; hence, $q$ and $q_1$ are added to $u^{\prime }$. It can be verified that $u^{\prime }=\{q^{\prime },q,q_1\}$ is a UCQ rewriting for $q^{\prime },\mathcal T$.

Suppose now that we want to further extend $q^{\prime }$ with the atom $\alpha _2=B(z)$ and that we want to compute a UCQ rewriting for $q^{\prime \prime } = q^{\prime }\cup \{B(z)\}$ and $\mathcal T$. One such rewriting computed using $\mathsf{PerfectRef }$ is the following:

$$\begin{aligned} \begin{array}{lll} u^{\prime \prime }= \{q^{\prime \prime }, q^{\prime }_1, q^{\prime }_2\},&\text{ where}&q^{\prime }_1=\{{x}\mid {R(x,y),B(x)}\}\\&\text{ and}&q^{\prime }_2=\{{x}\mid {A(x),B(x)}\}. \end{array} \end{aligned}$$

Suppose now that we want to compute $u^{\prime \prime }$ using our approach. Hence, we create the CQ $q_{\alpha _2}=\{{z}\mid {B(z)}\}$, compute the UCQ rewriting $u_{\alpha _2}=\{q_{\alpha _2}\}$ for $q_{\alpha _2},\mathcal T$ and then combine queries from $u^{\prime }$ and $u_{\alpha _2}$. Adding the atoms of $q_{\alpha _2}$ to $q^{\prime }$ creates query $q^{\prime \prime }$, however, for all other queries $q_i\in u^{\prime }$ we have $\mathsf{avar }(q_{\alpha _2})\nsubseteq \mathsf{var }(q_i)$ and hence no other query of $u^{\prime \prime }$ can be constructed.

The problem in the previous example is that after we merged $q_{\alpha _1}$ into $q$ our reference to variable $z$ was lost as this was mapped to $x$. This information is critical when we later further extend the input query and we want to decide whether it is possible to extend queries from $u^{\prime }$ with queries from $u_{\alpha _2}$. To correctly handle these cases, instead of the subset condition between variables, our algorithm uses the more involved method $\mathsf{canBeJoined }$ defined next.

Definition 2

Let $q$ be a query, let $\sigma$ be a substitution, and let $\mathsf{vars }$ be a set of variables. Then, function $\mathsf{canBeJoined } ({q},{\sigma },{\mathsf{vars }})$ returns $\mathsf{true }$ if for each $z\in \mathsf{vars }$ there exists $x\in \mathsf{var }(q)$ such that $z\rightsquigarrow _G x$ for $G$ the graph induced by $\sigma$.

Example 2

Consider query $q^{\prime \prime }$, UCQs $u_{\alpha _2}$ and $u^{\prime }$, and substitution $\sigma$ from Example 1. For queries $q_{\alpha _2}\in u_{\alpha _2}$ and $q\in u^{\prime }$ we have that $\mathsf{canBeJoined } ({q},{\sigma },{\mathsf{avar }(q_{\alpha _2})}) =\mathsf{true }$. Hence, the atoms of $q_{\alpha _2}$ (i.e., $B(z)$) can be added to those of $q$. Note, however, that due to $\sigma$ the new query that should be created is the query $q\cup \{B(z)_{\sigma }\}$, which is precisely $q^{\prime }_1$ from Example 1. Similarly, for the CQ $q_1\in u^{\prime }$ we have $\mathsf{canBeJoined } ({q_1},{\sigma },{\mathsf{avar }(q_{\alpha _2})}) =\mathsf{true }$, hence the query $q_1\cup \{B(z)_{\sigma }\}$ (i.e., $q^{\prime }_2$) is also created. Consequently, $u^{\prime \prime }$ of Example 1 can be constructed.

Summarising the above, when there exist queries $q_i\in u_\alpha$ and $q_j\in u$ such that $\mathsf{mergeCQs } ({q_i},{q_j}) \ne \emptyset$ (i.e., $q_i$ can be ‘merged’ into $q_j$) first, we need to know which queries have been generated in $u$ due to $q_j$, in order to ‘copy’ them to the result, and second, which variable mappings are used in the merge. To capture this information, in contrast to previous approaches, our algorithm operates over graphs $\mathcal G$ and $\mathcal G _\alpha$ of queries which store the dependencies between queries and the used mappings rather than on UCQs $u$ and $u_\alpha$.

Definition 3

Let $q$ be a CQ and let $\mathcal T$ be a TBox. A rewriting graph for $q,\mathcal T$ is a directed labelled graph $\mathcal G =\langle u , \mathcal H , m \rangle$, where $u$ is a UCQ rewriting for $q,\mathcal T$, $\mathcal H$ is a binary relation over $u$, and $m$ maps each $q_i\in u$ to a set of variable mappings. Moreover, $\mathcal G$ satisfies the following properties:

• If $\langle q_1 , q_2 \rangle \in \mathcal H$, then $q_2$ is produced from $q_1$ by the application of a reformulation or reduction step.

• For each $\langle q_1 , q_2 \rangle \in \mathcal H$ if $q_2$ is produced by a reformulation step, then $m(q_2) =m(q_1)$, while if it is produced by a reduction step with $\sigma$ the mgu, then $m(q_2) =m(q_1) \cup \sigma$.  

Concluding our algorithm overview, an important question is whether we can compute a UCQ rewriting for an extended query given any reference UCQ rewriting. As the following example shows this is not always possible.

Example 3

Consider the following TBox and CQ:

$$\begin{aligned} \mathcal T = \{A \sqsubseteq _{} \exists R\} \quad q = \{{x}\mid { A(x),R(x,y)}\}. \end{aligned}$$

Then, $\mathcal G _1=\langle u_1 , \mathcal H , \emptyset \rangle$ where $u_1=\{q, q_1\}, q_1= \{{x}\mid { A(x)}\}$ and $\mathcal H =\{\langle q , q_1 \rangle \}$ is a rewriting graph for $q,\mathcal T$. However, $q$ is redundant in $u_1$. Thus, $\mathcal G _2=\langle \{q_1\} , \emptyset , \emptyset \rangle$ is also a rewriting graph for $q,\mathcal T$.

Now suppose that we want to extend $q$ with the atom $\alpha =B(y)$ creating the query $q^{\prime }= q\cup \{B(y)\}$. A UCQ rewriting for $q^{\prime },\mathcal T$ computed using $\mathsf{PerfectRef }$ consists of the UCQ $u^{\prime }=\{q^{\prime }\}$.

Consider now the query $q_\alpha \!\!=\!\!\{{y}\!\!\!\!\mid \!\!\!\!{B(y)}\}$. Using $\mathsf{PerfectRef }$, we compute the UCQ rewriting $u_\alpha =\{q_\alpha \}$. Clearly, it is not possible to compute $u^{\prime }$ from $\mathcal G _2$. However, $u^{\prime }$ can be constructed from $\mathcal G _1$. More precisely, adding the atoms of $q_\alpha$ to $q$ creates $q^{\prime }$.

The problem in the previous example is that although $q$ is redundant in $u_1$ due to $q_1$, neither $q_1$ nor any other query related or produced by $q_1$ by the extension is part of the final UCQ rewriting. Hence, $q$ and all queries that are produced by $q$ are ‘relevant’ for computing a UCQ for $q\cup \{\alpha \}$ and are not redundant. Next, we formalise a property that is sufficient for computing a rewriting graph for an extended query.

Definition 4

Let $q$ be a query, let $\mathcal T$ be a TBox, let $\mathcal G =\langle u , \mathcal H , m \rangle$ be a rewriting graph for $q,\mathcal T$. We say that $\mathcal G$ is reformulation-closed for $q,\mathcal T$ if the following properties are satisfied:

• 1. $q$ is a top element in $\mathcal G$.

• 2. For each top element $q_i$ in $\mathcal G$ we have $m(q_i) =\emptyset$.

• 3. If a query $q_2$ can be produced using a single reformulation step on some query $q_1\in u$, then $\langle q_1 , q_2 \rangle \in \mathcal H$.

• 4. If $q_1\in u$ and atoms $R(z,y)$ and $R(x,y)$ or atoms $R(y,z)$ and $R(y,x)$ appear in $q_1$, then $\langle q_1 , q_2 \rangle \in \mathcal H$, where $q_2 =q_1{_{\{z\mapsto x\}}}$.

 

It is easy to see that the rewriting graph $\mathcal G _2$ from Example 3 is not reformulation-closed for $q,\mathcal T$ since $q$ does not appear as a top element, while $\mathcal G _1$ is.

3.2 The Rewriting Extension Algorithm

Our algorithm for computing a rewriting graph for a query $q$ extended with an atom $\alpha$ is shown in Algorithm 1. The algorithm accepts a TBox $\mathcal T$, a rewriting graph $\mathcal G$ for $q,\mathcal T$, and an atom $\alpha$ and it returns a rewriting graph for $q\cup \{\alpha \},\mathcal T$. First, it computes a rewriting graph $\mathcal G _\alpha$ for the query $\{ \mathsf{var }(\alpha )\cap \mathsf{var }(q) \mid {\alpha }\}$, which explicates from $\mathcal T$ the knowledge that regards atom $\alpha$. This is accomplished using the sub-routine $\mathsf{ex\text{-}PerfectRef }$, which consists of a straightforward extension of the standard $\mathsf{PerfectRef }$ algorithm [8]. More precisely, apart from applying the standard reformulation and reduction steps this algorithm also stores the dependencies between the queries using a relation as well as the mappings that are created due to the reduction steps. Subsequently, Algorithm 1 ‘combines’ $\mathcal G$ and $\mathcal G _\alpha$ using algorithm $\mathsf{joinGraphs }$ and computes a rewriting graph for the extended query.

Algorithm $\mathsf{joinGraphs }$ is shown in Algorithm 2. Intuitively, it computes the Cartesian product of the two input rewriting graphs. The intuition is that if $\langle q , q^{\prime } \rangle \in \mathcal G$ (i.e., $q^{\prime }$ is produced by $q$) and $q_\alpha$ is a vertex in $\mathcal G _\alpha$, then the same step would also be applicable to query $q\cup q_\alpha$—that is, $q\cup q_\alpha$ will produce the CQ $q^{\prime }\cup q_\alpha$. Similarly, for $q$ a vertex in $\mathcal G$ and $\langle q_\alpha , q^{\prime }_\alpha \rangle \in \mathcal G _\alpha$.

More precisely, the algorithm uses queues $Q$ and $Q_\alpha$ in order to traverse $\mathcal G$ and $\mathcal G _\alpha$, respectively. In line 5 it picks an element $q_h$ from $\mathcal G$ and checks if the query can be extended with atoms of queries in $\mathcal G _\alpha$ (line 6). If it does, then a CQ $q_\alpha$ is also picked from $\mathcal G _\alpha$ (line 9) and a new query $q_c$ from $q_h$ and $q_\alpha$ is created (line 11) that has as distinguished variables the variables in $nv$. Moreover, $m(q_h)$ is set as the mapping for $q_c$ (line 12). Subsequently, the algorithm checks if $q_\alpha$ can be merged into $q_h$. If it does, then it adds $\langle q_c , (q_h)_\sigma \rangle$ ($(q_h)_\sigma$ being the query produced after applying $\sigma$ to $q_h$) to the new graph (line 15) and then also ‘copies’ to the result the part of $\mathcal G$ that has been produced due to $q_h$ (lines 16–25) applying also a proper substitution $\mu$. This substitution is constructed using function $\mathsf{buildSubst }$.

Definition 5

Let $\sigma$ and $\kappa$ be two sets of mappings. Then, function $\mathsf{buildSubst } ({\sigma },{\kappa })$ returns a new set of mappings $\mu$ constructed in the following steps:

• 1. Set $\mu :=\kappa \cup \sigma$

• 2. For each $z\mapsto y\in \sigma$ if $z\mapsto y^{\prime }$ in $\kappa$ exists then replace $z\mapsto y^{\prime }$ in $\mu$ with $y\mapsto y^{\prime }$.

Note that, this function is important when for $q^{\prime }$ a ‘copied’ query we have $m(q^{\prime }) \ne \emptyset$.

After checking if a query can be merged, the algorithm iterates through the queries that are produced by $q_h$ (lines 27–30) as well as over those that are produced by $q_\alpha$ (lines 31–34) and constructs proper successors of $q_c$. This is done using the sub-routine $\mathsf{buildChildren }$, depicted in Algorithm 3, which follows a similar approach as before. That is, it computes the join between $q_h$ (a child of $q_h$) and some child of $q_\alpha$ (and $q_\alpha$) and then also checks if the two queries can be merged, in which case it copies the relevant sub-graph to the result. Finally, the children of $q_h$ ($q_\alpha$) are added to $Q$ ($Q_\alpha$).

Note that $\mathcal G$ and $\mathcal G _\alpha$ can be cyclic. Hence, the algorithm needs to keep track which nodes it has visited (copied) and avoid revisiting (recopying) them. This can be done using standard graph traversal techniques.

Example 4

Consider the following rewriting graphs:

$$\begin{aligned} \mathcal G =\langle \{q_1,q_2,q_3\} , \mathcal H , m \rangle&\; \text{ and} \;&\mathcal G _\alpha =\langle \{q^1_\alpha ,q^2_\alpha \} , \mathcal H _\alpha , m _\alpha \rangle \end{aligned}$$

where $\mathcal H$ and $\mathcal H _\alpha$ are as shown in Fig. 1a and b, respectively. Assume also that $m(q_i) =\emptyset$ for each $1\le i\le 3$ and that all queries $q_i$ can be extended. Figure 1c depicts the rewriting graph that is computed by Algorithm 1 for $\mathcal G$ and $\mathcal G _\alpha$, assuming that for each $q^j_\alpha \in u_\alpha$ and for each $q_i\in u$, we have $\mathsf{mergeCQs } ({q^j_\alpha },{q_i}) =\emptyset$—that is, no merges occur. More precisely, we have the following steps:

• At the first iteration we have $Q=\{q_1\}$ and $Q_\alpha =\{q^1_\alpha \}$, hence $q_h=q_1$ and $q_\alpha =q^1_\alpha$. In line 11, CQ $q_1\cup q^1_\alpha$ is created (recall that $m(q_1) =\emptyset$). Then, in the for-loop in lines 27–30, queries $q_2\cup q^1_\alpha$ and $q_3\cup q^1_\alpha$ are created, they are set as children of $q_1\cup q^1_\alpha$ and $q_2,q_3$ are added to $Q$. Subsequently, in the for-loop in lines 31–34 CQ $q_1\cup q^2_\alpha$ is created, it is set as child of $q_1\cup q^1_\alpha$ and $q^2_\alpha$ is added to $Q_\alpha$.

• In the next iteration $Q_\alpha =\{q^2_\alpha \}$, hence $q^2_\alpha$ is picked and now $q_h=q_1$ and $q_\alpha =q^2_\alpha$. Then, in line 11, CQ $q_1\cup q^2_\alpha$ is created, and then, in a similar way as described before, CQs $q_2\cup q^2_\alpha$ and $q_3\cup q^2_\alpha$ are created and pairs $\langle q_1\cup q^2_\alpha , q_2\cup q^2_\alpha \rangle$ and $\langle q_1\cup q^2_\alpha , q_3\cup q^2_\alpha \rangle$ are added to the result.

• In the next iteration, the algorithm picks $q_2$ from $Q$ and $Q_\alpha$ is again initialised to $\{q^1_\alpha \}$. Then, again query $q_2\cup q^1_\alpha$ will be constructed and ‘connected’ with query $q_2\cup q^2_\alpha$ that was constructed previously.

• Finally, the algorithm picks $q_3$ from $Q$ and again constructs $q_3\cup q^1_\alpha$ and ‘connects’ it with $q_3\cup q^2_\alpha$. Then, the algorithm terminates.

Fig. 1

Rewriting graphs of Example

Concluding this section we show the correctness of Algorithm 1.

By the definition of the function $\mathsf{mergeCQs }$ it is clear that our algorithm does not apply the standard reduction of the $\mathsf{PerfectRef }$ algorithm. For example, for the query $\{{x}\mid {R(x,y),R(y,z)}\}$ the standard reduction will produce the query $\{{x}\mid {R(x,x)}\}$; however, for $q_1=\{{x}\mid {R(x,y)}\}$ and $q_2=\{{x}\mid {R(y,z)}\}$, we have $\mathsf{mergeCQs } ({q_2},{q_1}) =\emptyset$ and hence $q_2$ is not merged into $q_1$. Correctness of our merge approach follows by the following lemma which proof is given in the Appendix.

Lemma 1

Let $q_1,q_2$ be two CQs such that $q_2$ subsumes $q_1$ and let $q^{\prime }_1$ be the result of applying an axiom $I$ to $q_1$. If $q_2$ does not subsume $q^{\prime }_1$, then either $I$ is applicable to $q_2$ and the result subsumes $q^{\prime }_1$ or for $1\le i\le n$, atoms of the form $P(u,v),P(z_i,v)$ or $P(v,u),P(v,z_i)$ exist in $q_2$ such that for $1\le i, j\le n$, $i\ne j$ we have $z_i\ne z_j$ and for $\lambda =\{z_i\mapsto u\mid 1\le i\le n\}$, $I$ is applicable to $(q_2)_{\lambda }$ and the result subsumes $q^{\prime }_1$.

As explained in Sect. 3.1, the reduction step was introduced because an axiom $I$ might only be applicable to a reduction $q^{\prime }$ of some CQ $q$. However, it is well-known that if $q^{\prime }$ is the reduction of $q$, then $q$ subsumes $q^{\prime }$. Hence, if some $I$ is applicable to $q^{\prime }$ but not to $q$, Lemma 1 dictates that only a restricted form of reductions over atoms in $q$ are necessary to obtain a CQ over which $I$ is applicable. Such reductions are precisely those used to decide whether a query from $u_\alpha$ can be merged into a query in the reference rewriting.

Consider a CQ $q$, a TBox $\mathcal T$, an atom $\alpha$, a rewriting graph $\mathcal G$ for $q,\mathcal T$ and a rewriting graph $\mathcal G _\alpha$ computed by Algorithm 1 in line 1. Assume also that $u$ is the UCQ rewriting computed using the standard $\mathsf{PerfectRef }$ algorithm over $q\cup \{\alpha \},\mathcal T$. To show correctness, we will use induction over the number of steps that the $\mathsf{PerfectRef }$ algorithm has been applied over $q\cup \{\alpha \},\mathcal T$. For example, assume that $u_i\subseteq u$ is the UCQ computed at step $i$ and that for every $q_i\in u_i$ some $q_h$ in $\mathcal G$ and some $q_\alpha$ in $\mathcal G _\alpha$ exist such that $\{{nv}\mid {q_h\cup (q_{\alpha })_\kappa }\}$, where $\kappa =m(q_h)$ and $nv= \mathsf{avar }(q_h)\cup (\mathsf{var }((q_{\alpha })_\kappa )\cap \mathsf{avar }(q))$ subsumes $q_i$. Then, assume that at step $i+1$ some axiom $I$ is applied to $q_i$ producing $q_{i+1}$. By Lemma 1 either $I$ is applicable to $\{{nv}\mid {q_h\cup (q_{\alpha })_\kappa }\}$ and the result subsumes $q_{i+1}$ or several restricted reductions are applicable. In the former case $I$ is either applicable to some atom in $q_h$ producing some query $q^{\prime }_h$ for which we will have $\langle q_h , q^{\prime }_h \rangle \in \mathcal G$ or $I$ is applicable to $(q_\alpha )_\kappa$. Hence, in the former case we will have some $q^{\prime }_h$ in $\mathcal G$ such that $\{{nv}\mid {q^{\prime }_h\cup (q_{\alpha })_\kappa }\}$ subsumes $q_{i+1}$. In the latter case the existence of some $q^{\prime }_\alpha$ in $\mathcal G _\alpha$ such that $\langle q_\alpha , q^{\prime }_\alpha \rangle \in \mathcal G _\alpha$ and $\{{nv}\mid {q_h\cup (q^{\prime }_{\alpha })_\kappa }\}$ subsumes $q_{i+1}$ follows by the following lemma which we show in the Appendix.

Lemma 2

Let $q$ be a CQ that contains exactly one body atom and let $\kappa$ be a substitution such that some axiom $I$ is applicable to $q_\kappa$ producing $q^{\prime }$. Then $I$ is also applicable to $q$ and for $q^{\prime \prime }$ the result we have $q^{\prime \prime }_\kappa =q^{\prime }$ (modulo renaming of fresh variables).

Finally, the following theorem establishes the correctness of the algorithm. The proof is given in the Appendix and consists of a systematic analysis of all of the aforementioned cases.

Theorem 1

Let $q$ be a CQ, let $\mathcal T$ be a TBox, let $\alpha$ be an atom such that $\mathsf{var }(\alpha )\cap \mathsf{var }(q)\ne \emptyset$ and let $\mathcal G$ be a reformulation-closed rewriting graph for $q,\mathcal T$. Let $\mathcal G ^{\prime }$ be the graph returned by Algorithm 1 when applied to $\mathcal G , \alpha$ and $\mathcal T$; then $\mathcal G ^{\prime }$ is a reformulation-closed rewriting graph for $q\cup \{\alpha \},\mathcal T$.

4 An Incremental Query Rewriting Algorithm

Algorithm 2 can form the basis for developing a UCQ rewriting algorithm for fixed queries over TBoxes. More precisely, for a fixed CQ $q$ one can pick some atom $\alpha \in q$, compute a rewriting graph for the query $q_{1} = \{ \mathsf{var } (\alpha ) \cap \mathsf{avar } (q) \mid {\alpha } \}$ over $\mathcal T$ using $\mathsf{ex\text{-}PerfectRef }$ and then extend this rewriting graph by iteratively adding the rest of the body atoms of $q$ using Algorithm 2.

The above idea is illustrated in Algorithm 4. The algorithm first selects some atom $\alpha$ such that some of its variables appear as distinguished variables in $q$ (line 2) and computes a rewriting graph $\mathcal G$ for the query $\{ \mathsf{var }(\alpha )\cap \mathsf{avar }(q) \mid {\alpha }\}$ (line 3). At this point a rewriting graph for a query that contains only atom $\alpha$ of $q$, variables $cv=\mathsf{var }(\alpha )$ of $q$ and distinguished variables $\mathsf{var }(\alpha )\cap \mathsf{avar }(q)$ of $q$ have been computed. Then, the algorithm selects one-by-one the remaing atoms and extends the previously computed rewriting graph (lines 5–11). More precisely, at the $i$-th iteration the algorithm has computed a rewriting graph $\mathcal G$ for a query $q_{i}$ that contains $i+1$ atoms of $q$, has as distinguished variables the variables in $\mathsf{var }(q_i)\cap \mathsf{avar } (q)$, while $cv$ contains the variables of $q$ that appear in $q_{i}$. Hence, the algorithm picks an atom $\alpha ^{\prime }$ such that some of its variables also appear in $cv$ (line 6), it computes a rewriting graph $\mathcal G _{\alpha ^{\prime }}$ for the query $\{ \mathsf{var }(\alpha ^{\prime })\cap cv \mid {\alpha ^{\prime }}\}$ (line 8) and then, it joins $\mathcal G$ with $\mathcal G _{\alpha ^{\prime }}$ using Algorithm 2 (line 9). Finally, the algorithm uses the well-known redundancy elimination algorithm proposed in [27] to remove the redundant (subsumed) queries (line 12) and return a UCQ. Note that the latter is possible since we assume that the query is fixed.

Theorem 2

Let $q$ be a CQ and let $\mathcal T$ be a TBox. When applied to $q$ and $\mathcal T$ Algorithm 4 terminates. Let $u$ be the UCQ produced by the algorithm; then, $u$ is a UCQ rewriting for $q,\mathcal T$.

The theorem follows by Theorem 1 and induction over the atoms of $q$ that have been added by Algorithm 4.

We now comment on the maximum number of CQs generated by our rewriting algorithm. Since our algorithm computes a UCQ rewriting it is thus of the same worst case complexity as other systems, like QuOnto, Nyaya, and Requiem, i.e., exponential w.r.t. the size of the input CQ [18].

Lemma 3

Let $\mathcal T$ be a DL-Lite TBox, let $q$ be a CQ, and let $\mathcal G =\langle u , \mathcal H , m \rangle$ be the output of Algorithm 4. Then, the maximal size of $\vert u\vert$ is $\mathcal O ((\vert \mathcal T \vert \cdot \vert q\vert )^{\vert q\vert })$.

Proof

Let $m$ be the number of concepts and roles appearing in $\mathcal T$ and $n$ the number of atoms in $q$. Let also $u_i$ be the UCQ computed at the $i$-$1$-th iteration of the while-loop of Algorithm 4. In the next iteration, $u_{i+1}$ is computed by first computing a rewriting graph $\mathcal G _{\alpha _i}=\langle u_{\alpha _i} , \mathcal H _{\alpha _i}, m _{\alpha _i} \rangle$ for an atom ${\alpha _i}$ of $q$ and then using the queries in $u_{\alpha _i}$ and $u_i$ to build new queries by either extending or merging. Since the query for which $u_{\alpha _i}$ is computed contains exactly one atom, then there can be at most $m\cdot (2+1)^2$ different queries in $u_\alpha$ (the factor ‘$2+1$’ is because the atom can be a role so there are two variables plus 1 for possibly freshly introduced variables). Next, the algorithm extends the queries in $u_i$ with atoms from the queries in $u_{\alpha _i}$. Hence, there can be $\vert u_i\vert \cdot m\cdot 3^2$ CQs generated by extension. Moreover, the algorithm checks if queries from $u_\alpha$ can be merged to CQs by computing all possible merges. For each merge, all CQs in $u_i$ ‘below’ the merged query are copied. Since the queries in $u_i$ have at most $i$ atoms ($i$ atoms have been processed thus far), there can be at most $i\cdot \vert u_i\vert \cdot m\cdot 3^2$ CQs computed due to merging. Summarising, $\vert u_{i+1}\vert$ contains at most $(i+1)\cdot \vert u_i\vert \cdot m\cdot 3^2$ CQs. By recursively analysing $\vert u_i\vert$ and since $\vert u_0\vert =u_{\alpha _0}$ we can conclude that $\vert u_n\vert$ contains at most $n\cdot (n-1)\cdot \ldots \cdot 2\cdot m^n\cdot 3^{2\cdot n}$ CQs. Since $m$ is bounded by $\vert \mathcal T \vert$ and $n$ by $\vert q\vert$ we have that $\vert u\vert =\vert u_n\vert =\mathcal O (\vert \mathcal T \vert ^{\vert q\vert }\cdot \vert q\vert ! \cdot 3^{2\cdot {\vert q\vert }})=\mathcal O (\vert \mathcal T \vert ^{\vert q\vert }\cdot \vert q\vert !)=\mathcal O ((\vert \mathcal T \vert \cdot \vert q\vert )^{\vert q\vert })$.$\square$

Clearly, in absence of any optimisations or refinements Algorithm 4 is not likely to behave well in practice. In the following sections we present several optimisations which aim at improving its performance. Note that these optimisations intend to improve the computation time of the algorithm rather than reduce the size of the UCQ. Recall, however, that recent techniques show how we can also significantly reduce the size of the UCQ using the input data when we finally want to evaluate the rewriting [30, 31].

4.1 Optimising the Last Iteration

As explained in Section 3, Algorithm 2 computes the Cartesian product between the input rewriting graphs. The structure of the computed graph is important for subsequent additions of atoms, however, it is not important after processing the last atom of a fixed query using Algorithm 4. Consequently, when the last atom $\alpha ^{\prime }$ is selected in line 6, Algorithm 4 can proceed as follows: First, in line 8 it can compute a UCQ rewriting $u_{\alpha ^{\prime }}$ for the query $\{{jv}\mid {\alpha ^{\prime }}\}$ using the standard $\mathsf{PerfectRef }$ algorithm, instead of a rewriting graph $\mathcal G _{\alpha ^{\prime }}$. Then, when joining $\mathcal G$ and $u_{\alpha ^{\prime }}$ it can call a simplified version of Algorithm 2 that constructs a UCQ rather than a rewriting graph. Algorithm 5 depicts the simplified algorithm. Roughly speaking, it is obtained from Algorithm 2 by removing the for-loops in lines 27–34 and adding the computed queries to a UCQ $u^{\prime }$ rather than a graph.

Another way to further improve the performance of Algorithm 5 is to identify cases where queries from $\mathcal G$ do not need to be further processed and extended with atoms of queries from $u_\alpha$. The next proposition demonstrates a case where ‘copying’ a query from the reference rewriting to $u^{\prime }$ due to a merge is sufficient to discard certain queries from $\mathcal G$.

Proposition 1

Let $\mathcal G =\langle u , \mathcal H , m \rangle$ be a rewriting graph, let $u_\alpha$ be a UCQ, let $nv$ be a set of variables and let $q_h\in u$. If there exists a query $q_\alpha$ in $u_\alpha$ and substitution $\lambda$ such that for all $\{z\mapsto x\}\in \mathsf{mergeCQs } ({(q_{\alpha })_\lambda },{q_h})$ we have $z\not \in \mathsf{var }(q_h)$, then for each $q^{\prime }$ such that $q_h\rightsquigarrow _\mathcal G q^{\prime }$, each $q^{\prime }_\alpha$ in $u_\alpha$ and each substitution $\kappa$, the CQ $\{{nv}\mid {q^{\prime }}\}_{\mu ^{\prime }}$ where $\mu ^{\prime }=\mathsf{buildSubst } ({\{z\mapsto x\}},{m(q^{\prime })})$ subsumes $\{{nv}\mid {q^{\prime }\cup (q^{\prime }_\alpha )_\kappa }\}$.

Consider Algorithm 5 and assume that for some query $q_h$ in line 4, some query $q_\alpha$ in line 6 and some $\{z\mapsto x\}\in \mathsf{mergeCQs } ({(q_{\alpha })_\lambda },{q_h})$ in line 9 the algorithm adds to $u^{\prime }$ all CQs $\{{nv}\mid {q^{\prime }}\}_{\mu ^{\prime }}$ such that $q_h\rightsquigarrow _\mathcal G q^{\prime }$ (line 14). If $z\not \in \mathsf{var }(q_h)$, then by the properties of reformulation and reduction for all such $q^{\prime }$ we have $z\not \in \mathsf{var }(q^{\prime })$ and hence also no mapping of the form $z\mapsto y$ appears in $m(q^{\prime })$. Moreover, we clearly have that $q^{\prime }_{m(q^{\prime })}=q^{\prime }$. Hence, for any such query $q^{\prime }$ and for $\mu ^{\prime }=\mathsf{buildSubst } ({\{z\mapsto x\}},{m(q^{\prime })})$ we have $q^{\prime }_{\mu ^{\prime }}=q^{\prime }$ and thus $\{{nv}\mid {q^{\prime }}\}_{\mu ^{\prime }}$ trivially subsumes $\{{nv}\mid {q^{\prime }\cup (q^{\prime }_\alpha )_\kappa }\}$ for any $\kappa$ and $q^{\prime }_\alpha$. Consequently, Algorithm 5 adds the successors of a selected query $q_h$ to the queue in line 19 only if $\Sigma =\emptyset$ or there exists $\{z\mapsto x\}\in \Sigma$ with $z\in \mathsf{var }(q_h)$ since otherwise the extensions of such queries is known to lead to redundant queries.

4.2 Optimising Redundancy Elimination

As described in the previous section, in line 12 Algorithm 4 applies the well-known redundancy elimination algorithm [27]. It has been shown by several experimental evaluations [9, 27] that this method usually does not perform well in practice because it consists of two nested for-loops over the (potentially large) computed UCQ $u^{\prime }$. More precisely, the algorithm needs to check whether each CQ $q_1\in u^{\prime }$ is subsumed by some other CQ $q_2\in u^{\prime }$. In order to improve the performance of this method our algorithm uses three approaches which attempt to reduce the size of the sets over which the algorithm would execute these for-loops.

First, it tries to identify on the fly, during the execution of Algorithm 5, queries that if produced and added to $u^{\prime }$ are going to be redundant. The more redundant queries are identified the smaller the size of $u^{\prime }$ over which algorithm $\mathsf{removeRedundant }$ would be executed. However, $u^{\prime }$ can still be very large. Hence, second, it tries to identify queries that are going to be non-redundant in the computed set $u^{\prime }$. Such queries can then be excluded from the final check reducing the size of the first for-loop of method $\mathsf{removeRedundant }$. More precisely, if $u^{\prime }_{nr}$ is the set of non-redundant queries then only the CQs in $u^{\prime }\setminus u^{\prime }_{nr}$ need to be checked against the CQs in $u^{\prime }$. Third, it tries to identify queries that are non-subsumers. This can be used to reduce the size of the second for-loop of the method. More precisely, if $u^{\prime }_{ns}$ contains all such queries then each CQs in $u^{\prime }\setminus u^{\prime }_{nr}$ needs to be checked only against the CQs in $u^{\prime }\setminus u^{\prime }_{ns}$.

4.2.1 Pruning Redundant Queries

The following proposition presents two properties by which we can identify that a query possibly generated by Algorithm 5 will be redundant in the final UCQ.

Proposition 2

Let $\mathcal G =\langle u , \mathcal H , m \rangle$ be a rewriting graph, let $u_\alpha$ be a UCQ, let $jv,av$ be sets of variables, and let $u^{\prime }$ be the output of Algorithm 5 when applied to $\mathcal G ,u_\alpha ,jv$, and $av$. Let a CQ $q\in u$ with $\mathsf{canBeJoined } ({q},{m(q)},{jv}) =\mathsf{true }$, let $nv$ be the set of variables constructed for $q$ in line 7, and assume that $q$ is subsumed by some other CQ $q^{\prime }\in u$; then the following properties hold:

• (R1) If $\{{nv}\mid {q^{\prime }}\}\in u^{\prime }$, then $\{{nv}\mid {q}\}$ is redundant in $u^{\prime }$.

• (R2) If $\mathsf{canBeJoined } ({q^{\prime }},{m(q^{\prime })},{jv}) =\mathsf{true }$, $q^{\prime }\subseteq q$, and $m(q^{\prime }) =m(q)$, then for each $q_\alpha \in u_\alpha$ the CQ $\{{nv}\mid {q\cup (q_\alpha )_{m(q)}}\}$ is redundant in $u^{\prime }$.

Proof

Property $(R1)$ holds straightforwardly, hence we only show Property $(R2)$.

First, we show that for all $q_\alpha \in u_\alpha$ the CQ $\{{nv}\mid {q\cup (q_\alpha )_{m(q)}}\}$ is subsumed by the CQ $\{{nv^{\prime }}\mid {q^{\prime }\cup (q_\alpha )_{m(q^{\prime })}}\}$ where $nv^{\prime }$ is the set of variables constructed for $q^{\prime }$ in line 7. More precisely, since $q^{\prime }\subseteq q$ and $m(q^{\prime }) =m(q)$ the for all $q_\alpha \in u_\alpha$ we have $q^{\prime }\cup (q_\alpha )_{m(q^{\prime })}\subseteq q\cup (q_\alpha )_{m(q)}$. Moreover, for the same reasons $nv$ is equal to $nv^{\prime }$; hence $\{{nv^{\prime }}\mid {q^{\prime }\cup (q_\alpha )_{m(q^{\prime })}}\}$ subsumes $\{{nv}\mid {q\cup (q_\alpha )_{m(q)}}\}$ for each $q_\alpha \in u_\alpha$.

Now, since $\mathsf{canBeJoined } ({q^{\prime }},{m(q^{\prime })},{jv}) =\mathsf{true }$, upon termination of Algorithm 5 we have that for each $q_\alpha \in u_\alpha$ either the CQ $\{{nv^{\prime }}\mid {q^{\prime }\cup (q_\alpha )_{m(q^{\prime })}}\}$ has been added to $u^{\prime }$ (line 8) or another query that subsumes it. In either case $\{{nv}\mid {q\cup (q_\alpha )_{m(q)}}\}$ is redundant in $u^{\prime }$. $\square$

Proposition 5 can be used to avoid adding redundant queries to the result $u^{\prime }$ when Algorithm 4 calls Algorithm 5 in the last iteration. However, to check for Properties $(R1)$ and $(R2)$ we need to know the subsumption relations between the CQs in $\mathcal G$. To identify these relations, before calling Algorithm 5, Algorithm 4 executes the standard subsumption checking algorithm over $\mathcal G$ and stores all such relations. Note that, no queries are removed at this point as $\mathcal G$ needs to be reformulation-closed for Algorithm 5 to produce a UCQ rewriting. Furthermore, note that the size of $\mathcal G$ at this point of iteration is expected to be significantly smaller than that of the final UCQ, hence the subsumption algorithm is expected to behave well in practice. Then, Algorithm 5 uses Properties $(R1)$ and $(R2)$ as follows:

• In line 14, it does not add the query $\{{nv}\mid {q^{\prime }}\}_{\mu ^{\prime }}$ to $u^{\prime }$ if $q^{\prime }$ is subsumed by some $q^{\prime \prime }$ in $\mathcal G$ and $\{{nv}\mid {q^{\prime \prime }}\}$ has already been added to $u^{\prime }$.

• Let $q_h$ be a query selected in line 4. If $q_h$ is subsumed by some $q^{\prime }$ in $\mathcal G$ and either $\{{nv^{\prime }}\mid {q^{\prime }}\}$ has already been added to $u^{\prime }$, or $q^{\prime }\subseteq q_h$, $m(q^{\prime }) =m(q_h)$, and $\mathsf{canBeJoined } ({q^{\prime }},{m(q^{\prime })},{jv}) =\mathsf{true }$, then the algorithm ‘skips’ $q_h$—that is, it adds each $q^{\prime \prime }$ such that $\langle q_h,q^{\prime \prime }\rangle \in \mathcal G$ to $Q$ and it continues with the next iteration.

Note that, although the conditions of Property $(R2)$ seem rather strict, it is actually very often the case in practice that a query $q^{\prime }$ subsumes a query $q$ under the identity substitution and that $m(q^{\prime }) =m(q) =\emptyset$. Moreover, regarding Property $(R1)$, note that in the vast majority of cases the set of variables $nv$ constructed for each CQ in line 7 is the same for all queries, while in line 10 for $\sigma =\{z\mapsto x\}$ we usually have $z\not \in \mathsf{var }(q^{\prime })$; hence, in line 14 we will have that $\{{nv}\mid {q^{\prime }}\}_{\mu ^{\prime }}=\{{nv}\mid {q^{\prime }}\}$. Consequently, both conditions of Proposition 2 can be very effective in practice as also supported by our experimental evaluation.

Example 5

Assume that for some CQ and TBox, Algorithm 4 has at some point computed the graph $\mathcal G =\langle u , \mathcal H , m \rangle$, where $u$ contains $q_1=\{{x}\mid {A(x), R(x,y)}\}$ and $q_2 = \{{x}\mid {A(x)}\}$ and also $m(q_1) =m(q_2) =\emptyset$. Clearly, $q_1$ is subsumed by $q_2$, however, the algorithm cannot remove this query from $\mathcal G$ at this point. In the final step, assume that Algorithm 5 is called for $\mathcal G$ and $u_\alpha =\{q_\alpha \}$, where $q_\alpha = \{{x}\mid {B(x)}\}$. When the algorithm processes $q_1$ and $q_\alpha$ it is easy to see that the conditions of Property $(R2)$ are satisfied. More precisely, $q_1$ is subsumed by $q_2$, $q_2\subseteq q_1$ and $m(q_1) =m(q_2)$. Hence, Algorithm 5 can avoid creating query $q=\{{x}\mid {A(x), R(x,y), B(x)}\}$ from $q_1$ and $q_\alpha$. Indeed the algorithm will at some point pick $q_2$ and $q_\alpha$ and it will produce the query $q^{\prime }=\{{x}\mid {A(x),B(x)}\}$ which subsumes $q$; hence, $q$ is indeed going to be redundant if added to the result $u^{\prime }$.

4.2.2 Tracking Non-Redundant Queries

It is quite often the case that extending a query that is non-redundant in step $i$ produces a query that is also non-redundant in step $i$+1. Since usually the largest number of CQs in the final UCQ are non-redundant, it would be beneficial for the algorithm if these could be identified during the course of Algorithm 5. Such queries can then be excluded from the final reduction elimination check (line 12 of Algorithm 4), hence reducing significantly the size of the for-loops that this method needs to execute.

The following proposition provides means to identify non-redundant queries during the execution of Algorithm 5 assuming we have identified the subsumption relations in the input rewriting graph.

Proposition 3

Let $\mathcal G =\langle u , \mathcal H , m \rangle$ be a rewriting graph, let $u_\alpha$ be a UCQ, let $jv,av$ be sets of variables, and let $u^{\prime }$ be the output of Algorithm 5 when applied to $\mathcal G ,u_\alpha ,jv$, and $av$. Let a CQ $q\in u$ with $\mathsf{canBeJoined } ({q},{m(q)},{jv}) =\mathsf{true }$, let $nv$ be the set of variables constructed for $q$ in line 7, and assume that $q$ is non-redundant in $u$; then the following properties hold:

• (N1) $\{{nv}\mid {q}\}$ is also non-redundant in $u^{\prime }$.

• (N2) Let $\kappa =m(q)$ and consider a CQ $q_\alpha \in u_\alpha$. If none of the predicates of the body atoms of $q_\alpha$ appear in any CQ $q^{\prime }\in u$ different from $q$ and for each $q^{\prime }_\alpha \in u_\alpha$ we have $\mathsf{mergeCQs } ({(q^{\prime }_\alpha )_\kappa },{q}) =\emptyset$, then the query $\{{nv}\mid {q\cup (q_\alpha )_\kappa }\}$ is also non-redundant in $u^{\prime }$.

Proof

(Property $(N1)$) Let $q^{\prime }$ be an arbitrary CQ in $u$ different from $q$. Upon termination, either a CQ of the form $\{{nv^{\prime }}\mid {q^{\prime }}\}_{\mu ^{\prime }}$ for some $\mu ^{\prime }$ or a CQ of the form $\{{nv^{\prime }}\mid {q^{\prime }\cup (q_\alpha )_\kappa }\}$ for some $q_\alpha \in u_\alpha$ is added to $u^{\prime }$ by Algorithm 5. Assume that $\{{nv^{\prime }}\mid {q^{\prime }}\}_{\mu ^{\prime }}$ subsumes $\{{nv}\mid {q}\}$. Then a $\theta$ exists such that $q^{\prime }_{\mu ^{\prime }\circ \theta } \subseteq q$ and so, $q^{\prime }_{\theta ^{\prime }} \subseteq q$ for $\theta ^{\prime } = \mu ^{\prime }\circ \theta$, contrary to our assumption; similarly if we assume that $\{{nv^{\prime }}\mid {q^{\prime }\cup (q_\alpha )_\kappa }\}$ subsumes $q$. Hence, we can conclude that none of the aforementioned queries can subsume $\{{nv}\mid {q}\}$. Since $q^{\prime }$ was an arbitrary CQ it follows that no query in $u^{\prime }$ subsumes $\{{nv}\mid {q}\}$ and hence this is non-redundant in $u^{\prime }$.

(Property $(N2)$) Since $q$ is non-redundant in $u$ then for all $q^{\prime }\in u$ different from $q$ and for all substitutions $\theta$, we have $[\{Q(\mathsf{avar }(q^{\prime }))\}\cup q^{\prime }]_{\theta }\not \subseteq [\{Q(\mathsf{avar }(q))\}\cup q]$. Let $q^{\prime }$ be one such arbitrary CQ and let $\theta$ be an arbitrary substitution. If $Q(\mathsf{avar }(q^{\prime }))_\theta \ne Q(\mathsf{avar }(q))$, then the property trivially holds as $q_\alpha$ is irrelevant. Hence, assume that $Q(\mathsf{avar }(q^{\prime }))_\theta =Q(\mathsf{avar }(q))$. This implies that there must be some atom $At$ in the body of $q^{\prime }$ such that $At_\theta \in q^{\prime }_\theta$ and $At_\theta \not \in q$. Consider now an arbitrary query $q_\alpha \in u_\alpha$ such that none of the predicates of its body atoms appear in any body atom of $q^{\prime }$. This implies that $At_\theta \not \in q_\alpha$ and $At_\theta \not \in (q_{\alpha })_\kappa$ for any substitution $\kappa$ and hence also $At_\theta \not \in q\cup (q_\alpha )_{m(q)}$. Consequently, neither $\{{nv^{\prime }}\mid {q^{\prime }}\}_{\mu ^{\prime }}$ for any substitution ${\mu ^{\prime }}$ nor $\{{nv^{\prime }}\mid {q^{\prime }\cup (q^{\prime }_\alpha )_{m(q^{\prime })}}\}$ for any $q^{\prime }_\alpha \in u_\alpha$ subsume $\{{nv}\mid {q\cup (q_\alpha )_{m(q)}}\}$. Furthermore, for each query $q^{\prime }_\alpha \in u_\alpha$ we have $\mathsf{mergeCQs } ({q^{\prime }_\alpha },{q}) =\emptyset$ and again because no predicate name of $q^{\prime }_\alpha$ appears in any other CQ, no query of the form $\{{nv}\mid {q}\}_{\mu ^{\prime }}$ for $\mu ^{\prime }$ a substitution is ever added to $u^{\prime }$ by Algorithm 5. Summarising, $\{{nv}\mid {q\cup (q_\alpha )_{m(q)}}\}$ is non-redundant in $u^{\prime }$. $\square$

Let $\mathcal G =\langle u , \mathcal H , m \rangle$ be the graph and $u_\alpha$ the UCQ with which Algorithm 5 is called. Then, in order to use Properties $(N1)$ and $(N2)$ the algorithm is modified as follows:

• At the beginning it initialises an empty set $N\!R$ of non-redundant queries.

• In line 14, if $\{{nv^{\prime }}\mid {q^{\prime }}\}_{\mu ^{\prime }}=\{{nv}\mid {q^{\prime }}\}$ and $q^{\prime }$ is non-redundant in $u$, then it adds $\{{nv}\mid {q^{\prime }}\}_{\mu ^{\prime }}$ to $NR$.

• In line 8, it adds $\{{nv}\mid {q_h\cup (q_\alpha )_{m(q)}}\}$ to $NR$ if $q_h$ is non-redundant in $u$, none of the predicates in $q_\alpha$ appear in any query in $u$ and if for each $q^{\prime }_\alpha \in u_\alpha$ we have $\mathsf{mergeCQs } ({q^{\prime }_\alpha },{q}) =\emptyset$.

• Finally, it returns both the UCQ $u^{\prime }$ and the set $N\!R$.

Subsequently, the returned set $N\!R$ is used by method $\mathsf{removeRedundant }$ (line 12 of Algorithm 4) to exclude all these queries from redundancy checking.

Again, note that checking whether for each $q_\alpha$ no predicate appears in a body atom of a query in $u$ requires iterating for each $q_\alpha \in u_\alpha$ through all queries in $u$. However, this can be performed only once at the beginning of Algorithm 5 and moreover, as mentioned before, at this point of the algorithm the set $u$ is expected to be moderate in size. Furthermore, as we will show in the evaluation section, in several cases this technique helps us to significantly decrease the cost of checking redundancy of the set $u^{\prime }$ and in many cases even avoid it completely if $u^{\prime }=N\!R$. This significantly outperforms its implementation overhead.

Example 6

Consider again $\mathcal G ,u$, and $u_\alpha$ from Example 5. If $u$ contains no other queries, then it is easy to see that for $q_2\in u$ and $q_\alpha \in u_\alpha$ the conditions of Property $(N2)$ are satisfied. More precisely, $q_2$ is non-redundant in $u$, none of the predicates of $q_\alpha$ appear in any other CQ in $u$ and $\mathsf{mergeCQs } ({q_\alpha },{q_2}) =\emptyset$. Hence, the CQ produced by $q_2$ and $q_\alpha$—that is, $q^{\prime }$ from Example 5, is non-redundant in the result. However, assume that besides $q_1$ and $q_2$ the UCQ $u$ also contained the CQ $q_3=\{{x}\mid {S(x,z)}\}$ and $u_\alpha$ also contained the CQ $q^{\prime }_\alpha =\{{x}\mid {S(x,z)}\}$. Now, Property $(N2)$ is not satisfied for $q_2$ and $q^{\prime }_\alpha$, since the predicate of $q^{\prime }_\alpha$ appears in $q_3$. Hence, we cannot guarantee that $q_2$ and $q^{\prime }_\alpha$ will produce a non-redundant query. Actually, the query that they produce (i.e., $\{{x}\mid {A(x),S(x,z)}\}$) is going to be subsumed by the query produced from $q_3$ and $q^{\prime }_\alpha$ (i.e., $\{{x}\mid {S(x,z)}\}$). However, the query $q^{\prime }$ produced by $q_2$ and $q_\alpha$ is still non-redundant.

4.2.3 Tracking Non-Subsumers

Finally, the following proposition presents a property by which we can identify that a query generated during the execution of Algorithm 5 will not subsume any other CQ generated by the same algorithm.

Proposition 4

Let $\mathcal G =\langle u , \mathcal H , m \rangle$ be a rewriting graph, let $u_\alpha$ be a UCQ, let $jv,av$ be sets of variables, and let $u^{\prime }$ be the output of Algorithm 5 when applied to $\mathcal G ,u_\alpha ,jv$, and $av$. Let a CQ $q\in u$ with $\mathsf{canBeJoined } ({q},{m(q)},{jv}) =\mathsf{true }$, let $nv$ be the set of variables constructed for $q$ in line 7, and assume that $q$ does not subsume any CQ in $u$; then the following property holds:

• (S) Let a CQ $q_\alpha \in u_\alpha$. If none of the predicates of the body atoms of $q_\alpha$ appear in any CQ in $u$ (including $q$), then the query $\{{nv}\mid {q\cup (q_\alpha )_{m(q)}}\}$ does not subsume any CQ in $u^{\prime }$.

Proof

Since $q$ does not subsume any CQ in $u$, we have $q_\theta \not \subseteq q^{\prime }$ for all $q^{\prime } \in u$ different from $q$ and substitutions $\theta$. Hence, for each $\theta$ there exists an atom $At$ in the body of $q$ such that $At_\theta \in q_\theta$ and $At_\theta \not \in q^{\prime }$. To show that $\{{nv}\mid {q\cup (q_\alpha )_{m(q)}}\}$, called $q_n$ in the following, is not a subsumer of any CQ in $u^{\prime }$ consider an arbitrary CQ $q^{\prime }\in u$. Upon termination, Algorithm 5 can add to $u^{\prime }$ either the CQ $\{{nv^{\prime }}\mid {q^{\prime }}\}_{\mu ^{\prime }}$ for some $\mu ^{\prime }$ or the CQ $\{{nv^{\prime }}\mid {q^{\prime }\cup (q^{\prime }_\alpha )_\kappa }\}$ for some (possibly different) $q^{\prime }_\alpha \in u_\alpha$. We will show that $q_n$ does not subsume any such CQ.

By assumption none of the predicates of the atoms in $q_\alpha$ appear in $q^{\prime }$. Hence, there clearly exists some $At^{\prime }\in q_n$ (actually some that appears in $q_\alpha$) such that for any $\theta$ we have $At^{\prime }_\theta \not \in \{{nv^{\prime }}\mid {q^{\prime }}_{\mu ^{\prime }}\}$; hence, $q_n$ does not subsume $\{{nv^{\prime }}\mid {q^{\prime }}\}_{\mu ^{\prime }}$. Moreover, by these arguments it also follows that $q_n$ does not subsume $\{{nv^{\prime }}\mid {q^{\prime }\cup (q^{\prime }_\alpha )_\kappa }\}$ for any $\kappa$ and any $q^{\prime }_\alpha \in u_\alpha$ different from $q_\alpha$.

Finally, consider the CQ $\{{nv^{\prime }}\mid {q^{\prime }\cup (q_\alpha )_\kappa }\}$. Recall that for every $\theta$ there exists $At_\theta \in q_\theta$ such that $At_\theta \not \in q^{\prime }$. Hence, again by assumption since none of the atoms in $q_\alpha$ appear in $q$ we have $At_\theta \not \in q_\alpha$ and hence also $At_\theta \not \in \{{nv^{\prime }}\mid {q^{\prime }\cup (q_\alpha )_\kappa }\}$.

Since $q^{\prime }$ was an arbitrary query, it follows that $q_n$ cannot subsume any CQ produced by Algorithm 5. $\square$

Similarly as before, Algorithm 5 uses additional sets to store such queries which are then excluded from the for-loops of algorithm $\mathsf{removeRedundant }$.

Example 7

Consider again Examples 5 and 6, and the UCQ $u=\{q_1,q_2,q_3\}$. Then, it is easy to see that for $q_1\in u$ and $q_\alpha \in u_\alpha$ the conditions of Property $(S)$ are satisfied. More precisely, $q_1$ does not subsume any CQ in $u$ and none of the predicates of the body of atoms of $q_\alpha$ appear in any CQ in $u$. Hence, the CQ produced by $q_1$ and $q_\alpha$—that is $q^{\prime } = \{{x}\mid {A(x), R(x,y), B(x))}\}$ is not going to subsume any CQ in the result. However, assume that $u_\alpha$ also contained the CQ $q^{\prime }_\alpha =\{{x}\mid {R(x,z)}\}$. Now, Property $(S)$ is not satisfied for $q_1$ and $q_\alpha ^{\prime }$, since the predicate of $q^{\prime }_\alpha$ appears in $q_1$. Hence, we cannot guarantee that $q_1$ and $q^{\prime }_\alpha$ will produce a query that is not going to subsume any other CQ in the result. Actually the query that they produce (i.e., $\{{x}\mid {A(x), R(x,y), R(x,z))}\}$) subsumes the query produced by $q_2$ and $q^{\prime }_\alpha$ (i.e., $\{{x}\mid {A(x), R(x,z)}\}$).

5 Implementation and Evaluation

We have implemented Algorithms 1–5 in a prototype tool called IQAROS.² We have also implemented an extended $\mathsf{PerfectRef }$ algorithm, called $\mathsf{PerfectRef } ^+$, that uses a restricted reduction step based on Lemma 1.

We have conducted three experimental evaluations. The first one compares $\mathsf{PerfectRef }$ with $\mathsf{PerfectRef } ^+$ to assess how much the restricted reduction step improves the performance of the original $\mathsf{PerfectRef }$ algorithm. In the second one we compared several versions of the IQAROS system using each time a different set of the optimisations presented in Section 4. In addition, we compared against $\mathsf{PerfectRef } ^+$ to assess how much the incremental step-by-step algorithm improves the original strategy. Finally, in the third experiment we compared IQAROS against several state-of-the-art query rewriting systems. More precisely, we were able to compare with Rapid [9], Nyaya [11] and Presto [32], while we did not compare against Requiem [27] because Rapid significantly outperforms it [9].

For the evaluation we used the framework proposed in [27]. It consists of nine ontologies, namely V that captures information about European history, P1 and P5 that are two hand-crafted artificial ontologies, S that models information about European Union financial institutions, U that is a DL-Lite$_R$ version of the well-known LUBM³ ontology and A that is an ontology capturing information about abilities and disabilities. Moreover, we also used the ontologies P5X, UX and AX that consist of normalised versions⁴ of the ontologies P5, U and A. For each ontology, a set of five hand-crafted queries is proposed. All experiments were conducted on a MacBook Pro with a 2.66GHz processor and 4GB of RAM, with a time-out of 600 s.

5.1 Comparing $\mathsf{PerfectRef }$ and $\mathsf{PerfectRef } ^+$

Table 4 presents the results of running $\mathsf{PerfectRef }$ (denoted as $\mathsf{PR }$ in the table) and $\mathsf{PerfectRef } ^+$ (denoted as $\mathsf{PR }^+$ in the table) over the test queries and ontologies. The table presents the size of the computed UCQs before applying the final redundancy elimination algorithm, then the corresponding computation times (in milliseconds), and finally the time to execute the redundancy elimination algorithm in the computed UCQ. Furthermore, the column marked as $\sharp NR$ presents the size of the non-redundant UCQ that systems should have computed. Note that this is the size of the UCQ computed by both system after the final redundancy elimination. Also, note that we do not present results for ontology P1 as it is trivial for the tested systems.

Table 4 Comparison between $\mathsf{PerfectRef }$, $\mathsf{PerfectRef } ^+$ and various versions of IQAROS

From the table we can observe that in many cases, most notably in ontologies P5, P5X, and S the size of the UCQ computed by $\mathsf{PerfectRef } ^+$ is much smaller than the one computed by $\mathsf{PerfectRef }$. Especially, in P5 and P5X this is because the test queries consist of a role chain of the form $\{{x}\mid {R(x_1,x_2),\ldots ,R(x_{i-1},x_i)}\}$, hence the (standard) reduction of $\mathsf{PerfectRef }$ produces many redundant queries like those presented before Lemma 1. However, in all other cases the differences between the systems are marginal.

Regarding performance, we note that $\mathsf{PerfectRef } ^+$ demonstrates better performance than $\mathsf{PerfectRef }$ in all tests where the former managed to compute fewer redundant queries than the latter. However, in all other cases both systems behave the same and sometimes $\mathsf{PerfectRef } ^+$ is actually slower than $\mathsf{PerfectRef }$. This is due to the overhead of implementing the checks for the restricted reduction step. No significant differences were observed in the execution of the final redundancy elimination algorithm, not even in the ontologies where the UCQ computed by $\mathsf{PerfectRef } ^+$ is notably smaller that that computed by $\mathsf{PerfectRef }$.

5.2 Comparing IQAROS and $\mathsf{PerfectRef } ^+$

Table 4 also shows the results of running three different versions of IQAROS; the first one (called $\mathsf{Inc }_1$) implements Algorithms 4 and 2 without any optimisations, the second one (called $\mathsf{Inc }_2$) uses Algorithm 5 instead of Algorithm 2 when it adds the last atom of the query, while the third one (called $\mathsf{Inc }_3$) refines $\mathsf{Inc }_2$ by also implementing the various optimisations detailed in the previous section for improving the efficiency of the redundancy elimination algorithm.

First, we can observe that the sizes of the UCQs computed by $\mathsf{Inc }_1$ and $\mathsf{PerfectRef } ^+$ are almost identical (with some minor differences in some queries and ontologies). This is because both systems are based on the restricted reduction step and because in its core $\mathsf{Inc }_1$ is based on the same reformulation algorithm for explicating knowledge from $\mathcal T$. However, despite their similarities in the computed UCQs we can observe that $\mathsf{Inc }_1$ is significantly more efficient than $\mathsf{PerfectRef } ^+$. For example, in ontologies P5, P5X, S, U, and UX, $\mathsf{Inc }_1$ is several times faster than $\mathsf{PerfectRef } ^+$, while in query 5 in ontologies A and AX, it manages to be up to two orders of a magnitude faster than $\mathsf{PerfectRef } ^+$. Since in their core both systems are based on the same approach for materialising knowledge from $\mathcal T$ and since the restricted reduction step implemented in $\mathsf{PerfectRef } ^+$ did not improve much the performance of the original $\mathsf{PerfectRef }$ system, we concluded that this improvement is mainly due to the incremental rewriting strategy. More precisely, the incremental approach provides a much more guided and localised strategy (it processes a single atom at a time), compared to the blind brute-force application of the inference rules of $\mathsf{PerfectRef } (^+)$. Finally, since both systems compute UCQs of comparable size the time for eliminating the redundant queries using algorithm $\mathsf{removeRedundant }$ are quite similar. Note, however, that this algorithm heavily depends on the form of input (e.g., the order that it processes the queries) and hence small variations may occur.

Comparing the different versions of IQAROS we can observe that the size of the computed UCQs decreases as we move from $\mathsf{Inc }_1$ to $\mathsf{Inc }_2$ and finally to $\mathsf{Inc }_3$. For example, in several cases $\mathsf{Inc }_2$ computes even up to 30 times smaller UCQs than $\mathsf{Inc }_1$ (see ontologies P5X, S, U, and UX). This decrease can be justified by the fact that $\mathsf{Inc }_2$ uses (the simpler) Algorithm 5 instead of Algorithm 2, when it adds the last atom of the query. Moreover, we can see that the use of a lightweight algorithm for the last iteration of Algorithm 4 is also reflected in the computation times of $\mathsf{Inc }_2$ compared to $\mathsf{Inc }_1$. More precisely, in nearly all ontologies $\mathsf{Inc }_2$ is several times faster than $\mathsf{Inc }_1$. The effects of computing much smaller UCQs for ontologies P5X and AX are also reflected in the final redundancy elimination algorithm. However, note that neither system can compute a non-redundant UCQ for query 5 in ontology AX.

Finally, $\mathsf{Inc }_3$ produces the smallest UCQ rewriting compared to all previous systems. This is due to the additional implemented techniques for identifying redundant queries that have been described in Proposition 2. We can also observe that due to these optimisations, in most cases the UCQ computed by $\mathsf{Inc }_3$ is actually also non-redundant or it contains very few redundant queries. Regarding computation time, $\mathsf{Inc }_3$ is generally as fast as $\mathsf{Inc }_2$, however, we can observe that in several cases it is slightly slower. This is due to the overhead of implementing the various optimisations. However, when considering the time for the redundancy elimination algorithm the benefits of tracking (non-)redundant queries become most apparent. $\mathsf{Inc }_3$ is faster than all other systems and much faster in all queries of ontology AX. Especially, $\mathsf{Inc }_3$ is the only system that can compute a non-redundant UCQ for query 5 in ontologies A and AX. More precisely, from the 32,960 queries that the algorithm has computed after processing the last atom of query 5 it has identified 31,593 non-redundant queries. These queries are then skipped from the redundancy elimination step and hence the algorithm finishes in less than 2.4 s.

5.3 Comparing IQAROS, Nyaya, Presto and Rapid

Table 5 presents a comparison between $\mathsf{Inc }_3$ and the systems Rapid, Nyaya and Presto (again we do not present the results for P1). Moreover, in the columns marked as ‘UCQ Computation Time’ we also present two additional times. The first one, marked as $\mathsf{Inc }_1^n$, is the time required by $\mathsf{Inc }_1$ to process the last atom $\alpha$ of the input query $q$ using Algorithm 4, while $\mathsf{Inc }_3^n$ is the same time but for the configuration $\mathsf{Inc }_3$ using Algorithm 5. Hence, these times reflect only the time that is required to extend the rewriting graph $\mathcal G ^-$ computed so far for $q^-,\mathcal T$, where $q^-=q\setminus \{\alpha \}$, into a rewriting for $q,\mathcal T$—that is, if we were given $\mathcal G ^-$ for $q^-,\mathcal T$ these times would reflect only the time to extend the input rewriting into a new UCQ rewriting for $q^-$ extended with $\alpha$. Note here that the output of $\mathsf{Inc }^n_1$ is a rewriting graph which can then be further extended, while the output of $\mathsf{Inc }^n_3$ is a UCQ.

Table 5 Comparison between $\mathsf{Rapid }$, $\mathsf{Nyaya }$, $\mathsf{Presto }$ and IQAROS

As before, after the final redundancy elimination all systems return UCQ rewritings of the same size (those reported in Table 4 column $\sharp NR$), except for Presto in queries 2–5 in ontology P5 and queries 2 and 4 in ontology AX. After manually inspecting the ontologies and computed UCQs and contrasted with the ones computed by all other systems we concluded that $\mathsf{Presto }$ is incomplete in these cases. More precisely, it fails to compute queries which are not subsumed by other queries that it computes. Hence, there exist an ABox for which equation (1) fails; similarly, in ontology AX.

Compared to $\mathsf{Nyaya }, \mathsf{Inc }_3$ (as well as all other versions of IQAROS from Table 4) is in general much faster, in some cases even for several orders of magnitude. Furthermore, $\mathsf{Inc }_3$ also computes much smaller UCQs. Since Nyaya is also mainly based on the same reformulation algorithm as $\mathsf{PerfectRef }$ for materialising knowledge from $\mathcal T$ the reasons for this difference are again similar to the ones mentioned before.

Compared to $\mathsf{Presto }, \mathsf{Inc }_3$ computes smaller UCQs with most distinct cases queries 2–5 in P5X, queries 1 and 2 in A and finally all the queries in AX. The effects of computing much smaller UCQs are also reflected in the UCQ computation time where $\mathsf{Inc }_3$ performs in general much faster, even for several orders of magnitude in some cases (query 1 in V, queries 4 and 5 in P5X, query 1 in A, and all queries in AX) with most notable one query 5 in AX where $\mathsf{Presto }$ fails to terminate in the provided timeout. However there exist cases that $\mathsf{Presto }$ is ‘notably faster’⁵ such as query 5 in UX and query 5 in A. In addition we can see that the redundancy elimination algorithm of $\mathsf{Inc }_3$ is much more efficient than that of $\mathsf{Presto }$ due to the several optimisations techniques that are used to identify (non-)redundant and non-subsumer queries.

Compared to $\mathsf{Rapid }$, $\mathsf{Inc }_3$ computes similarly small UCQs with some small exceptions (either against or in favour) in queries 3–5 in ontology P5X, in query 1 in ontologies A and AX and in queries 2, 4 and 5 in ontology AX. Moreover, $\mathsf{Rapid }$ is notably faster only in queries 4 and 5 in P5 and 5 in S and A. However, even in these cases the difference between the systems is rather marginal as it never exceeds 253 ms. In all the other scenarios $\mathsf{Inc }_3$ is faster with most notable cases queries 4 and 5 in P5X and 2–5 in AX. Moreover, we can also see that the redundancy elimination algorithm of $\mathsf{Inc }_3$ is much more efficient than that of $\mathsf{Rapid }$ with again notable case query 5 in ontology AX. Once more, this is justified by the optimisation techniques that are used in $\mathsf{Inc }_3$ in order to identify (non-)redundant and non-subsumer queries.

However, we can see that the most efficient approach is $\mathsf{Inc }_3^n$. Hence, indeed computing a UCQ rewriting by extending a previously computed rewriting graph is the fastest way to compute a UCQ rewriting for an extended query. However, as noted before, the output of this algorithm is not a rewriting graph and hence cannot be used for further extensions of the query. However, by observing the computation time of $\mathsf{Inc }_1^n$ we can see that a rewriting graph can also be computed relatively efficiently. Hence, we argue that when a query $q$ is extended with a new atom $\alpha$ Algorithm 5 can be used to efficiently compute a new UCQ rewriting for $q^{\prime }=q\cup \{\alpha \}$, while at the same time, as a background process, Algorithm 4 (discarding redundancy elimination) can be used to compute a new rewriting graph for $q^{\prime }$, which can then be used in a similar way to compute a UCQ rewriting and a rewriting graph for extensions of $q^{\prime }$.

Summarising, Fig. 2 presents (using a logarithmic scale) the average computation time (both rewriting and final redundancy elimination) for each ontology, query and system presented in Table 5. The results depicted in the figure verify our previous analysis—that is, in the three non-trivial ontologies (i.e., V, P5X, and AX5) we can observe that $\mathsf{Inc }_3^n$ is the most efficient system followed by $\mathsf{Inc }_3$, $\mathsf{Rapid }$ and then $\mathsf{Presto }$. However, in most of the other ontologies all systems behave quite close to each other and no significant differences can be noted.

Fig. 2

Average rewriting time for all queries for each ontology

Finally, we have conducted a brief analysis of the memory required by each system in order to compute the final UCQ. The maximum amount of memory required by Rapid is 140MB, followed by Nyaya with 150MB, then Presto with 180MB, and finally $\mathsf{Inc }_3$ with 200MB. These maximum numbers were observed in ontology AX query 5.

6 Related Work

To the best of our knowledge there is no previous work in computing a rewriting of an extended query $q$ based on a previously computed rewriting for $q$ in the presence of logical constraints in either the ontology or database literature. The only relevant problem studied in the database literature is view adaptation [14, 22], where the problem is to compute the materialisation of a re-defined materialised view. However, in both works the focus is on updating the data (the materialisation of the view) and additionally there are no database constraints (ontological axioms) involved.

However, much work has been spent the last couple of years towards studying the problem of query rewriting over lightweight ontology languages both from a complexity point of view [7, 13, 18] as well as from the point of view of developing practical query rewriting systems [8, 9, 11, 24, 27, 32]. Next, we briefly overview the works that are most relevant to ours; a more extensive and detailed literature survey on query rewriting can also be found at [12].

The first algorithm for query rewriting over DL-Lite ontologies was introduced by Calvanese et al. [8] and was later implemented in the QuOnto system [1]. The algorithm rewrites an input query and TBox into a union of conjunctive queries using the reformulation and reduction steps. Then, Pérez-Urbina et al. [28] presented a resolution-based query rewriting algorithm for DL-Lite. The algorithm was implemented in the system Requiem [27] and the experimental evaluation showed that it outperforms QuOnto. Requiem was the first system to use query subsumption in order to reduce the number of computed redundant queries. Subsequently, Rosati and Almatelli [32] presented Presto that computes a rewriting in the form of a non-recursive Datalog program instead of a UCQ. Hence, the computed rewriting is much smaller compared to the output of Requiem and QuOnto. Also Presto was the first system to provide a technique that avoids the exponential blow-up of the reduction step of $\mathsf{PerfectRef }$. Recently, Chortaras et al. [9] presented a highly optimised resolution-based algorithm for DL-Lite that was implemented in the system Rapid. It was shown that Rapid outperforms both QuOnto and Requiem. Finally, a new system called Quest [30] uses similar rewriting techniques to $\mathsf{PerfectRef }$ but with many additional optimisations that use the structure of the input data to reduce the size of the computed rewriting and speed up the process.

Moreover, query rewriting has also attracted the attention in the field of query answering over database constraints. Calì et al. [3, 5] have studied and presented several lightweight classes of tuple-generating dependencies as well as of the Entity-Relationship model [4, 6]. Moreover, in subsequent works Gottlob et al. [11] also presented a practical query rewriting algorithm for Linear-Datalog $^\pm$ which is the one implemented in the Nyaya system. This algorithm is also based on the original DL-Lite algorithm but improves it with many optimisations, like atom factorization which is intended to reduce the number of redundant queries produced in the reduction step. Subsequently, a new algorithm that computes a non-recursive Datalog program for Linear-Datalog $^\pm$ was also presented [24].

Finally, a slightly different approach than the previous ones, called combined rewriting, has been proposed by Lutz et al. [21] for the DL language $\mathcal EL$ and by Kontchakov et al. [19] for the DL language DL-Lite$^\mathcal{N }_{horn}$. This approach computes small rewritings, however, it also requires pre-processing of the database.

7 Conclusions

In the current paper, we studied the problem of computing a UCQ rewriting for queries that have been extended with new atoms, by extending a previously computed UCQ rewriting for them and avoiding the computation of a UCQ rewriting from scratch. We studied the problem theoretically and presented detailed algorithms. Our study also gave rise to a novel query rewriting algorithm that is based on the incremental processing of query atoms. More precisely, given a fixed input query one can process one atom at a time and extend a previously computed rewriting until a UCQ for the input query has been computed. To improve its efficiency we have proposed several novel optimisations which greatly improve the computation time and reduce the number of computed redundant queries. Finally, we have implemented all algorithms and have conducted a detailed experimental evaluation. Our results show that the algorithm is highly efficient and generally outperforms all state-of-the-art systems that are currently available.

Apart from providing a novel efficient query rewriting system, our results have several important theoretical consequences and give many opportunities for future work. First, they show that rewriting over DL-Lite ontologies can largely be performed in parallel giving a complete efficient algorithm which, to the best of our knowledge, was previously unknown. This direction has not been explored in this paper and can be part of future work. Other directions of future work can be the investigation and design of such incremental algorithms for other lightweight languages, like Linear-Datalog$^\pm$, or for more expressive languages, like $\mathcal ELHI$. Furthermore, in the current paper, we have not studied other types of refinements for input queries, like the removal of atoms and the addition/removal of distinguished variables. Last but not least, another interesting problem that largely remains open in the area of query rewriting is how to efficiently evaluate the computed UCQ rewriting over a database. We feel that the incremental algorithm can provide some new opportunities in addressing this problem.

A Omitted Proofs

Lemma 1

Let $q_1,q_2$ be two CQs such that $q_2$ subsumes $q_1$ and let $q^{\prime }_1$ be the result of applying an axiom $I$ to $q_1$. If $q_2$ does not subsume $q^{\prime }_1$, then either $I$ is applicable to $q_2$ and the result subsumes $q^{\prime }_1$ or for $1\le i\le n$, atoms of the form $P(u,v),P(z_i,v)$ or $P(v,u),P(v,z_i)$ exist in $q_2$ such that for $1\le i, j\le n$, $i\ne j$ we have $z_i\ne z_j$ and for $\lambda =\{z_i\mapsto u\mid 1\le i\le n\}$, $I$ is applicable to $q_2{_\lambda }$ and the result subsumes $q^{\prime }_1$.

Proof

Since $q_2$ subsumes $q_1$, there exists a substitution $\theta$ s.t. $[\{Q(\mathsf{avar }(q_2))\}\cup q_2]_\theta \subseteq \{Q(\mathsf{avar }(q_1))\}\cup q_1$; however, $Q$ does not appear in either $q_1$ or $q_2$, hence $q_2{_\theta }\subseteq q_1$. Moreover, since $q_2$ does not subsume $q^{\prime }_1$ we have $q_2{_\theta }\nsubseteq q^{\prime }_1$. Hence, since $q^{\prime }_1$ is the result of applying $I$ to $q_1$ we have that $I$ is applied to an atom $\alpha \in q_1$ that is also in $q_2{_\theta }$ replacing it with a new atom $\beta$ that is not in $q_2{_\theta }$. Next, $\alpha \in q_2{_\theta }$ implies that $q_2$ contains an atom $\alpha _0$ such that $\alpha =\alpha _0{_\theta }$, i.e., an atom with the same predicate name as $\alpha$, but possibly containing different variables. By case analysis on the different types of applications between axioms and query atoms we show that either $I$ is also applicable to $\alpha _0$ and for $q^{\prime }_2$ the result of applying $I$ to $q_2$, $\theta$ can be extended to a new substitution $\sigma$ s.t. $q^{\prime }_2{_\sigma }\subseteq q^{\prime }_1$, or for $i\ge 1$ atoms of the form $P(u,v),P(z_i,v)$ or $P(v,u),P(v,z_i)$ exist in $q_2$ such that for $\lambda =\{z_i\mapsto u\mid i\ge 1\}$, $I$ is applicable to $q_2{_\lambda }$ and the result subsumes $q^{\prime }_1$.

Recall first that $\alpha \in q_1$, $\alpha \in q_2{_\theta }, \alpha _0\in q_2$, and $\beta \in q^{\prime }_1$. We have the following cases:

• 1. If $\alpha =A(x)$, then $I$ is of the form $C\sqsubseteq A$, with $C$ a concept, $\beta$ is of the form $C(x)$, while $\alpha _0$ is of the form $A(u)$, with $u\mapsto x\in \theta$. Then, clearly, $I$ is also applicable to $q_2$ creating a new query $q^{\prime }_2$ that contains $C(u)$. Then, we have the following cases:

  • If $I$ is of the form $B\sqsubseteq A$, then $\beta =B(x)$. In this case, $B(u)\in q^{\prime }_2$, and for $\sigma =\theta$ we have $B(x)\in q^{\prime }_2{_\sigma }$ which implies that $q^{\prime }_2{_\sigma }\subseteq q^{\prime }_1$.

  • If $I$ is of the form $\exists P\sqsubseteq A$, then $\beta =P(x,y)$ for $y$ a new variable in $q_1$. In this case, $P(u,z)\in q^{\prime }_2$ for $z$ a new variable in $q_2$. Since $z$ is new in $q_2$, $\theta$ can be extended to $\sigma =\theta \cup \{z\mapsto y\}$. Then, $P(x,y)\in q^{\prime }_2{_\sigma }$ which implies that $q^{\prime }_2{_\sigma } \subseteq q^{\prime }_1$.

  • The case where $I$ is of the form $\exists P^-\sqsubseteq A$ is symmetric with the previous one.

• 2. If $\alpha =P(x,y)$ and $I$ is of the form $S\sqsubseteq P$ (or equivalently $S^-\sqsubseteq P^-$), then $\beta =S(x,y)$, while $\alpha _0$ is of the form $P(u,v)$ with $\{u\mapsto x,v\mapsto y\}\subseteq \theta$. Then, clearly $I$ is also applicable to $q_2$ and its application creates $q^{\prime }_2$ with $S(u,v)\in q^{\prime }_2$, while for $\sigma =\theta$ we have $S(x,y)\in q^{\prime }_2{_\sigma }$ which implies that $q^{\prime }_2{_\sigma }\subseteq q^{\prime }_1$. The cases where $I$ is of the form $S\sqsubseteq P^-$ or $S^-\sqsubseteq P$ can be shown similarly.

• 3. If $\alpha =P(x,y)$, $y$ is unbound in $q_1$, and $I$ is of the form $C\sqsubseteq \exists P$ with $C$ a concept, then $\beta =C(x)$ and $\alpha _0=P(u,v)$ with $\{u\mapsto x,v\mapsto y\}\subseteq \theta$. If $v$ is also unbound in $q_2$, then $I$ is applicable to $q_2$ and for $q^{\prime }_2$ the result we will have $A(u)\in q^{\prime }_2$; hence, for $\sigma =\theta$ we will have $A(x)\in q^{\prime }_2{_\sigma }$ and also $q^{\prime }_2{_\sigma }\subseteq q^{\prime }_1$. If $v$ is not unbound in $q_2$ this implies that there is another atom $\alpha _2$ in $q_2$ that mentions $v$. $\alpha _2$ cannot be a concept atom of the form $A(v)$ because due to $q_2{_\theta } \subseteq q_1$ we would have $A(v)_\theta =A(y)\in q_1$ and hence $y$ would not be unbound in $q_1$ as well (it would appear in $A(y)$ and $P(x,y)$) leading to a contradiction; hence, $\alpha _2$ must be a role atom. However, $\alpha _2$ cannot be of the form $P(v,z)$, for $z$ an arbitrary variable since then, again $q_2{_\theta } \subseteq q_1$ implies that $P(v,z)_\theta =P(y,z_\theta )\in q_1$ and thus $y$ would not be unbound in $q_1$. The only possible case is that $\alpha _2$ is of the form $P(z,v)$ with $z\mapsto x\in \theta$ (again if $z$ is mapped to a different variable than $x$, this would imply that $q_1$ has two role atoms both having $y$ as a second argument and $y$ would not be unbound in $q_1$). Consequently, we have $\alpha _0{_\theta }=P(u,v)_\theta =P(z,v)_\theta =a_2{_\theta }$, which implies that the two atoms unify. Now, let the substitution $\sigma _1=\{z\mapsto u\}$. As mentioned before, $\theta$ maps both $z$ and $u$ to $x$; hence, for the defined $\sigma _1$ we have $q_2{_{\sigma _1\circ \theta }}=q_2{_\theta }$ and hence $q_2{_{\sigma _1}}$ also subsumes $q_1$. Consequently, all previous conditions apply to $q_2{_{\sigma _1}}$—that is, either $q_2{_{\sigma _1}}$ subsumes $q^{\prime }_1$, or $I$ is applicable to $q_2{_{\sigma _1}}$ and the result subsumes $q^{\prime }_1$. If neither of these is the case then again an atom $P(z^{\prime },v)$ with $z^{\prime }\ne z$ must exist in $q_2{_{\sigma _1}}$, such that it unifies with $P(u,v)$ and a $\sigma _2$ can be constructed such that $q_2{_{\sigma _1\circ \sigma _2}}$ subsumes $q_1$. Since, there is only a finite number of atoms in a query, at some point some $\lambda =\{z_i\mapsto u\mid i\ge 1\}$ exists such that $I$ is applicable to $q_2{_\lambda }$ and the result subsumes $q^{\prime }_1$. Note also that each $\sigma _i$ is independent from the other and hence they can be applied in an arbitrary order over $q_2$.

• 4. If $\alpha =P(y,x)$, $y$ is unbound in $q_1$, and $I$ is of the form $C\sqsubseteq \exists P^-$, then $\beta =C(x)$ and $\alpha _0=P(v,u)$ with $\{v\mapsto y, u\mapsto x\}\subseteq \theta$. Following a similar reasoning as in the previous case we can deduce that, either $v$ is also unbound in $q_2$ so $I$ is applicable to $q_2$ and the result subsumes $q^{\prime }_1$, or it is not and in this case a list of atoms $P(v,z_i)$ exists such that for $\lambda =\{z_i\mapsto u\}$, $I$ is applicable to $q_2{_\lambda }$ and the result subsumes $q^{\prime }_1$.$\square$

 

Lemma 2

Let $q$ be a CQ that contains only one body atom and let $\kappa$ be a substitution such that some axiom $I$ is applicable to $q_\kappa$ producing $q^{\prime }$. Then $I$ is also applicable to $q$ and for $q^{\prime \prime }$ the result we have $q^{\prime \prime }_\kappa =q^{\prime }$ (modulo renaming of fresh variables).

Proof

If $\kappa$ does not change any variables of $q$ then the property follows trivially. If it does, then we show the property by performing a case analysis on the form of $q$.

• 1. $q$ is of the form $\{{x}\mid {A(x)}\}$. Then, $\kappa$ can be of the form $\{x\mapsto y\}$ and $I$ is of the form $C\sqsubseteq A$, with $C$ a concept. In this case, $q^{\prime }=\{{y}\mid {C(y)}\}$, while $I$ is also applicable to $q$ and the result is $q^{\prime \prime }=\{{x}\mid {C(x)}\}$. If $C$ is an atomic concept then clearly $q^{\prime \prime }_\kappa =q^{\prime }$. If $C$ is of the form $\exists R$ for $R$ a role, then $q^{\prime }=\{{y}\mid {R(y,z_1)}\}$ and $q^{\prime \prime }=\{{x}\mid {R(x,z_2)}\}$, for $z_1,z_2$ fresh variables and again (modulo renaming of fresh variables) $q^{\prime \prime }_\kappa =q^{\prime }$.

• 2. $q$ is of the form $\{{x}\mid {R(x,y)}\}$. Then we have two cases depending on $I$.

  • (a) If $I$ is of the form $C\sqsubseteq \exists R$, then $\kappa$ cannot map $y$ to $x$ (and vice versa), as this would make $x$ ($y$) bound in $q_\kappa$. Hence, $\kappa$ (possibly) maps $x$ and/or $y$ to different variables. In any case $q^{\prime }=\{x_\kappa \mid C(x_\kappa )\}$. Clearly, $I$ is applicable to $q$ and again as in case 1. we can deduce that $q^{\prime \prime }_\kappa =q^{\prime }$.

  • (b) If $I$ is of the form $P\sqsubseteq R$ and $\kappa$ is as in the previous case, then the claim follows by a similar argument. However, $\kappa$ can be of the form $\{y\mapsto x\}$ (or $\{x\mapsto y\}$). Then, $q^{\prime }=\{x\mid P(x,x)\}$ (or $q^{\prime }=\{y\mid P(y,y)\}$). Clearly, $I$ is also applicable to $q$ and the result is $q^{\prime \prime }=\{x\mid P(x,y)\}$ for which $q^{\prime \prime }_\kappa =\{x\mid P(x,x)\}$ (or $q^{\prime \prime }_\kappa =\{y\mid P(y,y)\}$). In either case $q^{\prime \prime }_\kappa =q^{\prime }$.

• 3. $q$ is of the form $\{ x,y \mid R(x,y) \}$ and $I$ is of the form $P\sqsubseteq R$. This case is similar to case 2(b).

 

Theorem 1

Let $q$ be a CQ, let $\mathcal T$ be a TBox, let $\alpha$ be an atom such that $\mathsf{var }(\alpha )\cap \mathsf{var }(q)\ne \emptyset$ and let $\mathcal G$ be a reformulation-closed rewriting graph for $q,\mathcal T$. Let $\mathcal G ^{\prime }$ be the graph returned by Algorithm 1 when applied to $\mathcal G , \alpha$ and $\mathcal T$; then $\mathcal G ^{\prime }$ is a reformulation-closed rewriting graph for $q\cup \{\alpha \},\mathcal T$.

Proof

First, note that $\mathsf{ex\text{-}PerfectRef }$ extends $\mathsf{PerfectRef }$, hence for a given query $q$ and TBox $\mathcal T$ it computes a rewriting graph for $q,\mathcal T$. Moreover, since $\mathsf{PerfectRef }$ applies exhaustively reformulation and reduction and does not prune computed queries, the output of the extended algorithm is reformulation-closed.

Let $\mathcal G =\langle u , \mathcal H , m \rangle$ be the input of Algorithm 1 and let $\mathcal G ^{\prime }=\langle u^{\prime } , \mathcal H ^{\prime }, m^{\prime } \rangle$ be its output. Moreover, for the following of the proof, let $jv = \mathsf{var }(\alpha )\cap \mathsf{avar }(q)$, let $\mathcal G _\alpha = \langle u_\alpha , \mathcal H _\alpha , m _\alpha \rangle$ be the rewriting graph computed by Algorithm 1 in line 1, and let $u_i$ be a UCQ rewriting computed after $i$ steps of the $\mathsf{PerfectRef }$ algorithm when applied to $q\cup \{\alpha \},\mathcal T$—that is, after generating $i$ queries by an application of the reformulation or the reduction step.

Correctness of the claim is strongly based of the following property:

($\star$): For all $i\ge 0$ and for all $q_j$ in $u_i$ a vertex $q_{h}$ in $\mathcal G$ and a vertex $q_\alpha$ in $\mathcal G _\alpha$ exist such that, for $\kappa =m(q_{h})$ and $nv=\mathsf{avar } (q_h)\cup (\mathsf{avar } (q)\cap \mathsf{var }((q_\alpha )_\kappa ))$ we have $\mathsf{canBeJoined } ({q_h},{\kappa },{jv}) =\mathsf{true }$, and one of the following conditions hold:

• 1. $\{{nv}\mid {q_{h}\cup (q_{\alpha })_\kappa }\}$ subsumes $q_j$, or

• 2. for some $\sigma \in \mathsf{mergeCQs } ({(q_\alpha )_\kappa },{q_{h}})$ some CQ $q^{\prime }$ exists such that $q_{h}\rightsquigarrow _\mathcal G q^{\prime }$ and $\{{nv}\mid {q^{\prime }}\}_{\mu ^{\prime }}$, where $\mu ^{\prime }=\mathsf{buildSubst } ({\sigma },{m(q^{\prime })})$ subsumes $q_j$.

Assume for now that Property $(\star )$ holds. We will show that $\mathcal G ^{\prime }=\langle u^{\prime } , \mathcal H ^{\prime }, m^{\prime } \rangle$ is a reformulation-closed rewriting graph for $q\cup \{\alpha \},\mathcal T$.

First, we show that $u^{\prime }$ is a UCQ rewriting for $q\cup \{\alpha \},\mathcal T$. Assume that when applied to $q\cup \{\alpha \}$ and $\mathcal T$ the $\mathsf{PerfectRef }$ algorithm terminates after $n$ steps and that $u_n$ is the computed UCQ rewriting. But then, by Property $(\star )$, we know that upon termination of Algorithm 1, for each CQ $q_n\in u_n$ either a CQ of the form $\{{nv}\mid {q_h\cup (q_\alpha )_\kappa }\}$ or a CQ of the form $\{{nv}\mid {q^{\prime }}\}_{\mu ^{\prime }}$ that subsumes $q_n$ has been added to $u^{\prime }$. Moreover, functions $\mathsf{canBeJoined }$, $\mathsf{buildSubst }$, and the condition $\mathsf{dom }(\sigma )\subseteq \mathsf{var }(q^{\prime })\cup \mathsf{dom }(m(q^{\prime }))$ of the respective algorithms ensure that every CQ produced by our algorithm can also be produced by the $\mathsf{PerfectRef }$ algorithm. Consequently, $u^{\prime }$ is both sound and complete, thus it is indeed a UCQ rewriting for $q\cup \{\alpha \},\mathcal T$.

Now we show that $\mathcal G ^{\prime }$ is reformulation-closed. First, by definition of the mappings $m^{\prime }(q^{\prime }_n)$ for each CQ added to $\mathcal G ^{\prime }$ it follows that $m^{\prime }$ satisfies the conditions in Definition 3. Furthermore, upon termination of the algorithm also the relation $\mathcal H ^{\prime }$ satisfies the property of Definition 3. Moreover, again it can be easily seen that the algorithm will create and set as a top element of $\mathcal G ^{\prime }$ the CQ $q\cup \{\alpha \}$ with $m^{\prime }(q\cup \{\alpha \})=\emptyset$, while for all top elements $q_i$ in $\mathcal G ^{\prime }$ we will also have $m(q_i) =\emptyset$ as they inherit the mapping of $q$ (we elaborate more on this in the proof of Property $(\star )$ later on). In addition, $\mathcal H ^{\prime }$ is closed under restricted reduction; if for some $q_h\in u, \kappa =m(q_h)$ and $q_\alpha \in u_\alpha$ we have some $\sigma \in \mathsf{mergeCQs } ({(q_\alpha )_\kappa },{q_h})$, then the algorithm first adds $q^+=\{{nv}\mid {q_h\cup (q_\alpha )_\kappa }\}$ to $\mathcal G ^{\prime }$ (line 13) and then adds $\langle q^+ , \{{nv}\mid {(q_h)}\}_\sigma \rangle$ to $\mathcal G ^{\prime }$ (line 15). Then, it copies the sub-graph of $\mathcal H$ below $q_h$, but $\mathcal H$ is also reformulation-closed. The only interesting case is if for some $q^{\prime }$ such that $q_h\rightsquigarrow _\mathcal G q^{\prime }$ we have $z\mapsto x\in \sigma$ and $z\mapsto x^{\prime }\in m(q^{\prime })$. The latter implies that there exists $q^{\prime \prime }$ such that $\langle q^{\prime \prime } , q^{\prime } \rangle \in \mathcal H$ and $R(x^{\prime },y),R(z,y)$ are atoms in $q^{\prime \prime }$ while $q^{\prime }=q^{\prime \prime }_{z\mapsto x^{\prime }}$, i.e., every occurence of $z$ in $q^{\prime \prime }$ has been mapped to $x^{\prime }$. In the new graph $\mathcal H ^{\prime }$, the algorithm will rather contain the query $q^{\prime \prime }_\sigma$, i.e., $q^{\prime \prime }_\sigma$ will now contain atoms $R(x^{\prime },y),R(x,y)$ instead of $R(x,y),R(z,y)$, i.e., occurences of $z$ have been mapped to $x$. Subsequently, a child of $q^{\prime \prime }_\sigma$ needs to be created. For $\mathcal H ^{\prime }$ to be reformulation-closed the child needs to be a query where now $x$, rather than $z$, is mapped to $x^{\prime }$. This is accomplished by function $\mathsf{buildSubst }$. More precisely, since $z\mapsto x\in \sigma$ and $z\mapsto x^{\prime }\in m(q^{\prime })$, the function returns a mapping $\mu$ that contains $z\mapsto x$ and $x\mapsto x^{\prime }$ which is applied to $q^{\prime }$ creating the appropriate query. Consequently, $\mathcal G ^{\prime }$ is reformulation-closed for $q\cup \{\alpha \},\mathcal T$.

Now, we give the omitted proof of Property ($\star$).

To show this property we use induction over the number of steps $i$ that algorithm $\mathsf{ex\text{-}PerfectRef }$ has completed when applied to $q\cup \{\alpha \},\mathcal T$. For a CQ $q$ we will use the notation $m _q$ to denote the substitution $m(q)$.

Base Case ($i=0$): On the one hand, when algorithm $\mathsf{ex\text{-}PerfectRef }$ is applied to $q\cup \{\alpha \},\mathcal T$, at step $0$ it initialises a UCQ $u_0$ to contain the vertex $q\cup \{\alpha \}$. On the other hand, in line 1 Algorithm 1 computes $\mathcal G _\alpha$ for $q_\alpha =\{ \mathsf{var }(\alpha )\cap \mathsf{var }(q) \mid {\alpha }\}$ and $\mathcal T$ which uses $\mathsf{ex\text{-}PerfectRef }$ and hence at least contains $q_\alpha$ as a vertex. Moreover, since $\mathcal G$ is reformulation-closed for $q,\mathcal T$, then $q$ appears as a top element in $\mathcal G$ with $m _q=\emptyset$. Hence, by construction of $q_\alpha$ and $jv$ we have $\mathsf{canBeJoined } ({q},{m _{q}},{jv}) =\mathsf{true }$ and also $\{{nv}\mid {q\cup (q_{\alpha })_{m _q}}\}$ is exactly $q\cup \{\alpha \}$. Consequently, condition 1 is satisfied and hence also Property ($\star$) is satisfied at step $i=0$.

Induction Step: Assume that Property ($\star$) holds at step $i$ for each $q_j\in u_i$. Subsequently, suppose that at step $i+1$ the algorithm produces the UCQ $u_{i+1}$ by applying a reformulation or a reduction step on some query $q_j$ in $u_i$ producing a query $q_{i+1}$. Moreover, by induction hypothesis, vertices $q_h$ in $\mathcal G$ and $q_\alpha$ in $\mathcal G _\alpha$ exist such that Property ($\star$) is satisfied—that is, for $\kappa =m _{q_h}$, we have $\mathsf{canBeJoined } ({q_h},{\kappa },{jv}) =\mathsf{true }$ and either the query $\{{nv}\mid {q_h\cup (q_{\alpha })_{\kappa }}\}$ (called $q^{+}$ in the following) subsumes $q_j$, or for some $\sigma \in \mathsf{mergeCQs } ({(q_\alpha )_\kappa },{q_h})$ and some $q^{\prime }$ such that $q_h\rightsquigarrow _\mathcal G q^{\prime }$, we have that $\{{nv}\mid {q^{\prime }}\}_{\mu ^{\prime }}$ (called $q^m$ in the following) subsumes $q_j$. We now distinguish between two cases according to whether $q_{i+1}$ was produced by a reformulation or a reduction step.

If a reduction step was applied to $q_j$ to produce $q_{i+1}$, then it is well-known by the properties of reduction that $q_j$ subsumes $q_{i+1}$. Hence, by the transitivity of the subsumes relation and the induction hypothesis $q_{i+1}$ is also subsumed by either $q^+$ or $q^m$. Consequently, Property ($\star$) is still satisfied.

Otherwise, assume that a reformulation step was applied to $q_j$ to produce $q_{i+1}$. This implies that some axiom $I$ is applied to some body atom of $q_j$ producing $q_{i+1}$. By induction hypothesis, either $q^+$ or $q^m$ subsume $q_j$. If either of these queries subsumes $q_{i+1}$, then Property ($\star$) is satisfied. If neither query subsumes $q_{i+1}$, then by Lemma 1, either (i) $I$ is applicable to them and the result subsumes $q_{i+1}$ or (ii) for $n\ge 1$ atoms of the form $P(u,v),P(z_i,v)$ or $P(v,u),P(v,z_i)$ exist in $q^+$ or in $q^m$ such that for $\lambda =\{z_i\mapsto u\mid 1\le i\le n\}$, $q^+_\lambda$ or $q^m_\lambda$ subsumes $q_j$, $I$ is applicable to $q^+_\lambda$ or $q^m_{\lambda }$ and the result subsumes $q_{i+1}$. We now examine separately the cases that $q^+$ or $q^m$ subsume $q_j$.

• 1. Assume that $q^+$ subsumes $q_j$ and also that we have case (i) from above—that is, $I$ is applicable to $q^+=\{{nv}\mid {q_h\cup (q_\alpha )_{\kappa }}\}$. Since reformulation applies an axiom to a single body atom of a query at each time, this implies that $I$ is either applicable to some body atom of $q_h$ and the application creates a CQ of the form $\{{nv}\mid {q^{\prime }_h\cup (q_{\alpha })_\kappa }\}$, or it is applicable to some body atom of $(q_{\alpha })_\kappa$ and the application creates a CQ of the form $\{{nv}\mid {q_h\cup q^{\prime }_{\alpha }}\}$. (Note that reformulation does not change the distinguished variables of the query) In the former case, since $I$ is applicable to $q_h$ producing $q^{\prime }_h$, $q_h$ is a vertex in $\mathcal G$ and $\mathcal G$ is reformulation-closed, then $\langle q_h,q^{\prime }_h\rangle \in \mathcal H$ with $m _{q^{\prime }_h}=\kappa$ and $\mathsf{avar } (q_h)=\mathsf{avar } (q^{\prime }_h)$. Moreover, $\mathsf{canBeJoined } ({q^{\prime }_h},{m _{q^{\prime }_h}},{jv}) =\mathsf{true }$; this is because $I$ is applicable to $\{{nv}\mid {q_h\cup (q_\alpha )_\kappa }\}$, hence its application can only remove variables that do not appear in $(q_\alpha )_\kappa$. Consequently, condition 1 is satisfied and thus also Property ($\star$). Now we study the case when $I$ is applicable to $(q_\alpha )_\kappa$: First, note that $q_\alpha$ contains exactly one body atom; this follows straightforwardly by the fact that the query for which $\mathcal G _\alpha$ is computed contains exactly one atom and by the fact that the $\mathsf{PerfectRef }$ calculus always produces a new query that contains at most the same number of atoms as one from which it is produced. Hence, by Lemma 2, $I$ is also applicable to $q_\alpha$ and for the result $q^{\prime \prime }_\alpha$ we have $(q^{\prime \prime }_\alpha )_\kappa =q^{\prime }_\alpha$. But since $q_\alpha \in u_\alpha$ and $\mathcal G _\alpha$ is reformulation-closed, then $q^{\prime \prime }_\alpha \in u_\alpha$. Consequently, again condition 2. is satisfied thus also Property ($\star$). Assume now that we have case (ii) from above—that is, for $n\ge 1$ there are atoms of the form $P(u,v),P(z_i,v)$ or of the form $P(u,v),P(z_i,v)$ in $q^+$ such that for $\lambda =\{z_i\mapsto u\mid 1\le i\le n\}$, $I$ is applicable to $q^+_\lambda =\{{nv_{\lambda }}\mid {(q_h){_\lambda }\cup (q_\alpha )_{\kappa \circ \lambda }}\}$ and the new CQ produced by applying $I$ on $q^+_\lambda$, called $q_f$, subsumes $q_{i+1}$. We will show that our algorithm can compute queries $q^+_{\lambda }$ and $q_f$. First note that the existence of atoms of the above form in $q^+$ implies that several restricted reduction steps are applicable between body atoms $P(z_i,v)$ and the atom $P(u,v)$ in $q^{\prime }_j$. Moreover, since $(q_\alpha )_\kappa$ contains a single atom, then these reductions are either applicable over two atoms from $q_h$ or between an atom from $q_h$ and the atom in $(q_\alpha )_\kappa$. In the former case, an application of one of these reductions would produce the CQ $(q_h)_{\lambda _i}\cup (q_\alpha )_{\kappa \circ \lambda _i}$. Since graph $\mathcal G$ is reformulation-closed and by the form of these reductions, also $\langle q_h , q^{\prime }_h \rangle \in \mathcal G$, with $q^{\prime }_h=(q_h)_{\lambda _i}$ and $m _{q^{\prime }_h}=\kappa \circ \lambda _i$; hence, $\mathsf{canBeJoined } ({q^{\prime }_h},{m _{q^{\prime }_h}},{jv}) =\mathsf{true }$. If none of these reductions is performed between $(q_\alpha )_\kappa$ and $q_h$, then for $\lambda$ as defined before we will have $q_h\rightsquigarrow _\mathcal{G } (q_h)_\lambda$ with $m _{(q_h)_\lambda }=\kappa \circ \lambda$ and hence also $\mathsf{canBeJoined } ({(q_h)_\lambda },{m _{(q_h)_\lambda }},{jv}) =\mathsf{true }$. Then, axiom $I$ is applicable to $(q_h)_\lambda$ and since $\mathcal G$ is reformulation-closed we also have $\langle (q_h)_\lambda , q^{\prime \prime } \rangle \in \mathcal H$ and $m _{q^{\prime \prime }}=m _{q_{h\lambda }}$. Finally, $\{{nv^{\prime }}\mid {q^{\prime \prime }\cup (q_\alpha )_{m _{q^{\prime \prime }}}}\}$ for $nv^{\prime }=\mathsf{avar } (q^{\prime \prime })\cup (\mathsf{avar } (q)\cap \mathsf{var }((q_\alpha )_{m _{q^{\prime \prime }}}))$ is $q_f$ and it subsumes $q_{i+1}$, hence Property ($\star$) is satisfied. Assume now that for some $k\le n$, $(q_\alpha )_\kappa$ contains atom $P(z_k,u)$ and one reduction step involves $(q_\alpha )_\kappa$ and atoms from $q_h$. In this case since $(q_\alpha )_\kappa$ contains one atom then this reduction actually eliminates this atom from $q^+$ and hence $q^+_{\lambda _k}$ is of the form $\{ \mathsf{avar }(q)_{\lambda _k} \mid {(q_h)_{\lambda _k}}\}$. Consequently, applying the rest of reductions the final CQ $q^+_\lambda$ would be of the form $\{ \mathsf{avar }(q)_{\lambda } \mid {(q_h)_{\lambda }}\}$ and $q_f$ can be produced by applying $I$ on this CQ. Now, since $\mathcal G$ is reformulation-closed all reductions but $\lambda _k$ have been applied on queries in $\mathcal G$ starting from $q_h$, hence a CQ $(q_h)_\nu$, with $\nu =\lambda \setminus \lambda _k$ exists in $\mathcal G$ such that $q_h\rightsquigarrow _\mathcal G (q_h)_\nu$. Moreover, since $(q_h)_\nu$ does not contain the atom that is in $(q_\alpha )_\kappa I$ is applicable to it and hence $\langle (q_h)_\nu , q^{\prime \prime } \rangle \in \mathcal H$. Then, by definition of function $\mathsf{mergeCQs }$, we have that $\mathsf{mergeCQs } ({(q_\alpha )_\nu },{(q_h){_\nu }})$ contains $\{\lambda _k\}$. Hence, the CQ $q^{\prime \prime }_{\lambda _k}$ is actually $q_f$ that subsumes $q_{i+1}$ and Property ($\star$) is satisfied again.

• 2. Assume now that $q^m$, i.e., $\{{nv}\!\mid \!{q^{\prime }}\}_{\mu ^{\prime }}$ where $q_h\!\rightsquigarrow _\mathcal G \! q^{\prime }$, $\mu ^{\prime }\!=\mathsf{buildSubst } ({\sigma },{m(q^{\prime })})$ and $\sigma \!\in \!\mathsf{mergeCQs } ({(q_\alpha )_\kappa },{q_h})$ subsumes $q_j$. Again by Lemma 1 either $I$ is applicable to $q^m$ and the result (call it $q_f$) subsumes $q_{i+1}$ or further restricted reduction steps are applicable to $q^m$ producing a CQ over which $I$ is applicable and the result (call it again $q_f$) subsumes $q_{i+1}$. Since $q^{\prime }_{m (q^{\prime })}=q^{\prime }$ and since $\mu ^{\prime }$ is constructed from $\sigma$ and $m (q^{\prime })$, then $\{{nv}\mid {q^{\prime }}\}_{\mu ^{\prime }}$ is like $q^{\prime }$ but perhaps with some variable $z\in \mathsf{var }(q^{\prime })$ renamed due to a mapping $z\mapsto y\in \sigma$. Moreover, since $\{{nv}\mid {q^{\prime }}\}_{\mu ^{\prime }}$ does not mention $z$ (it has been renamed by $\mu ^{\prime }$), then neither of the previous steps (application of $I$ or restricted reductions) does involve $z$. Now, due to $\mu ^{\prime }$ either $q^{\prime }$ has fewer bound variables than $\{{nv}\mid {q^{\prime }}\}_{\mu ^{\prime }}$ or $\mu ^{\prime }$ frees a bound variable that is not free in $q^{\prime }$ after which some axiom might be applicable. In the former case ($q^{\prime }$ has fewer bound variables), at least the same sequence of reformulation or restricted reduction steps as to $q^{m}$ are applicable to $q^{\prime }$. Since these do not involve variable $z$, after applying them, a CQ $q^{\prime \prime }$ such that $\{{nv}\mid {q^{\prime \prime }}\}_{\mu ^{\prime \prime }}=q_f$, where $\mu ^{\prime \prime }=\mathsf{buildSubst } ({\sigma },{m(q^{\prime \prime })})$ is generated, as $\mu ^{\prime \prime }$ built from $\sigma$ will perform the same variable renaming on $z$. In addition, since $\mathcal G$ is reformulation-closed $q^{\prime \prime }$ is in $\mathcal G$. Now consider the latter case, i.e., $\mu ^{\prime }$ frees a bound variable in $q^{\prime }$. This implies that $\mu ^{\prime }$ induces a mapping $\{z\mapsto x\}$ that frees some bound variable in $q^{\prime }$. Consequently, a restricted reduction with unifier $\sigma ^{\prime }=\{z\mapsto x\}$ is applicable and since $\mathcal G$ is reformulation-closed we have that $\langle q^{\prime } , q^{\prime }_{\sigma ^{\prime }} \rangle \in \mathcal H$. Subsequently, the same sequence of reformulation and restricted reduction steps as to $q^m$ are applicable to $q^{\prime }_{\sigma ^{\prime }}$. Hence again, we will have a query $q^{\prime \prime }$ such that $\{{nv}\mid {q^{\prime \prime }}\}_{\mu ^{\prime \prime }}=q_f$, where $\mu ^{\prime \prime }=\mathsf{buildSubst } ({\sigma },{m(q^{\prime \prime })})$ is produced in $\mathcal G$. In any case Property ($\star$) is satisfied.$\square$