Also, as $\nu''$ is an extension of $\nu'$, from $\model{\nu'} \models \sigma(\kod{\pat}_2)$, it holds

$$\model{\nu''} \models \sigma(\kod{\pat}_2).$$

Therefore, $\model{\nu''}$ is a model of formula $\sigma(\kod{\pat}_2)$ and its negation as well, which is a contradiction.

As it holds $\mu \in \semdg{\kod{\pat}_1}{\ag}{\kod{\gr}}$ and it holds that there does not exist $\mu_2$ such that $\mu_2 \in \semdg{\kod{\pat}_2}{\ag}{\kod{\gr}}$ and $\mu_2 \comp \mu$, then, by Definition <ref>
$$\mu \in \semdg{\kod{\pat}_1}{\ag}{\kod{\gr}} - \semdg{\kod{\pat}_2}{\ag}{\kod{\gr}}.$$

Then, by Definition <ref>, it holds
$$\mu \in \semdg{\kod{\pat}_1 \  \kod{ minus } \ \kod{\pat}_2}{\ag}{\kod{\gr}}.$$

* $\kod{\pat}$ is $\kod{graph x \{\pat$_1$\}}$

$(\Rightarrow)$	By Definition <ref>,
$$\mu \in \semdg{\kod{ graph x \{\pat$_1$\}}}{\ag}{\kod{\gr}},$$

it holds

$$\mu \in \underset{\kod{i} \in names(\ag)} \bigcup \left(\ \semdg{\kod{\pat}_1}{\ag}{gr_{\,\ag}(\kod{i})} \bowtie \{ \mu_{\kod{x} \rightarrow \kod{i}} \} \ \right).$$

Therefore, $\agfn \not= \varnothing$ and there is an IRI $\kod{i}$ from $names(\ag)$ such that

$$\mu \in \semdg{\kod{\pat}_1}{\ag}{gr_{\,\ag}(\kod{i})} \bowtie \{ \mu_{\kod{x} \rightarrow \kod{i}} \}.$$

By Definition <ref>, there exists mapping $\mu_1$ such that $\mu = \mu_1 \cup \mu_{\kod{x} \rightarrow \kod{i}}$, $\mu_1 \in \semdg{\kod{\pat}_1}{\ag}{gr_{\,\ag}(\kod{i})}$ and $\mu_1 \comp\mu_{\kod{x} \rightarrow \kod{i}}$.
Applying the induction hypothesis on the mapping $\mu_1$ and a valuation $\nu_1$ such that $\mu_1 \povezano \nu_1$, it holds

$$\model{\nu_1} \models \sigma^{gr_{\,\ag}(\kod{i})}(\kod{\pat}_1).$$

By Lemma <ref>, from $\mu = \mu_1 \cup \mu_{\kod{x} \rightarrow \kod{i}}$, $\mu \povezano \nu$, $\mu_1 \povezano \nu_1$ and $\mu_{\kod{x} \rightarrow \kod{i}} \povezano \nu_{x \rightarrow \kod{i}}$, it holds $\nu = \nu_1 \cup \nu_{x \rightarrow \kod{i}}$.
Therefore, $\nu \succeq \nu_1$, and it holds

$$\model{\nu} \models \sigma^{gr_{\,\ag}(\kod{i})}(\kod{\pat}_1).$$

From $\mu = \mu_1 \cup \mu_{\kod{x} \rightarrow \kod{i}}$, it holds $\mu(\kod{x}) = \kod{i}$.
As $\kod{i} \in \kod{I}$, by Definition <ref>, it holds $\kod{i} = \valuation{\kod{i}}{\mu}$, and $\mu(\kod{x}) = \valuation{\kod{i}}{\mu}$.
By Lemma <ref>, from the last equation and $\mu \povezano \nu$, it holds

$$\model{\nu} \models \sigma(\kod{x}) = \sigma(\kod{i}).$$

Then, by Definition <ref>, it holds:

$$\model{\nu} \models \sigma^{gr_{\,\ag}(\kod{i})}(\kod{\pat}_1) \wedge \sigma(\kod{x}) = \sigma(\kod{i}).$$

By Definition <ref>, from $\kod{i} \in names(\ag)$, for $i = \siginv(\kod{i})$, it holds $i \in \agfn$.
Therefore, it holds

$$\model{\nu} \models \underset{i \in \agfn}\bigvee \Big( \sigma^{gr_{\,\ag}(\siginv({i}))}(\kod{\pat}_1) \wedge \sigma(\kod{x}) = i \Big),$$

and, by Definition <ref>,

$$\model{\nu} \models \sigma(\kod{graph x \{\pat$_1$\}}).$$

$(\Leftarrow)$ From

$$dom(\nu) = var(\sigma(\kod{graph x \{\pat$_1$\}})) \text{ and }$$

$$\model{\nu} \models \sigma(\kod{graph x \{\pat$_1$\}}),$$

by Definition <ref>, it holds

$$dom(\nu) = var(\sigma(\kod{\pat}_1)) \cup \{\sigma(\kod{x})\} \text{ and }$$

$$\model{\nu} \models \underset{i \in \agfn}\bigvee \Big( \sigma^{gr_{\,\ag}(\siginv({i}))}(\kod{\pat}_1) \wedge \sigma(\kod{x}) = i \Big).$$

Therefore, there is a constant $i$ from $\agfn$, such that $i = \sigma(\kod{i})$ and

$$\model{\nu} \models \sigma^{gr_{\,\ag}(\kod{i})}(\kod{\pat}_1) \wedge \sigma(\kod{x}) = \sigma(\kod{i}).$$

Then, by Definition <ref>, it holds

$$\model{\nu} \models \sigma^{gr_{\,\ag}(\kod{i})}(\kod{\pat}_1) \text{ and } \model{\nu} \models \sigma(\kod{x}) = \sigma(\kod{i}).$$

By Lemma <ref>, from the second satisfiability and $\mu \povezano \nu$, it holds $\mu(x) = \valuation{\kod{i}}{\mu},$ i.e. by Definition <ref>, it holds
$\mu(x) = \kod{i}$.
We consider two cases:

* If $\sigma(\kod{x}) \in var(\sigma(\kod{\pat}_1))$, i.e. $dom(\nu) = var(\sigma(\kod{\pat}_1))$.
By induction hypothesis, from the first satisfiability and $\mu \povezano \nu$, it holds
$\mu \in \semdg{\kod{\pat}_1}{\ag}{gr_{\,\ag}(\kod{i})}$.
Therefore, $\mu = \mu \cup \mu_{\kod{x} \rightarrow \kod{i}}$.

* If $\sigma(\kod{x}) \notin var(\sigma(\kod{\pat}_1))$, let $\nu'$ denotes a restriction of $\nu$ to the set $var(\sigma(\kod{\pat}_1))$.
Then, it holds $\model{\nu'} \models \sigma^{gr_{\,\ag}(\kod{i})}(\kod{\pat}_1)$.
Then, for a mapping $\mu'$ such that $\mu' \povezano \nu'$, by induction hypothesis, it holds $\mu' \in \semdg{\kod{\pat}_1}{\ag}{gr_{\,\ag}(\kod{i})}$.
By Definition <ref>, from $\mu \povezano \nu$, $\mu' \povezano \nu'$ and $\nu' \preceq \nu$, it holds $\mu' \preceq \mu$.
Also, it holds

\begin{align*}
& \hspace*{20mm} dom(\mu)& = &\\
& \text{(by Def \ref{def:povezano}, as } \mu \povezano \nu \text{)} \hspace*{-4mm} & = & \siginv(dom(\nu)) \\
&  & = & \siginv(var(\sigma(\kod{\pat}_1)) \\
&&& \cup \{\sigma(\kod{x})\}) \\
& \text{(by Def \ref{def:function_over_sets})} & = & \siginv(var(\sigma(\kod{\pat}_1))) \\
&&&\cup \siginv(\{\sigma(\kod{x})\}) \\
& \text{(by Lemma \ref{thm:dom_mu_nu1})} & = & \siginv(\sigma(var(\kod{\pat}_1))) \\
&&&\cup \siginv(\{\sigma(\kod{x})\}) \\
& \text{(by Def \ref{def:sigmat}, \ref{def:sigma})} & = & \kod{var}(\kod{\pat}_1) \cup \{\kod{x}\}
\end{align*}

By Lemma <ref>, as $\mu' \hspace*{1pt} \in \hspace*{1pt} \semdg{\kod{\pat}_1}{\ag}{gr_{\,\ag}(\kod{i})}$, it holds $dom(\mu') = \kod{var}(\kod{\pat}_1)$.
Therefore, it holds $\mu = \mu' \cup \mu_{\kod{x} \rightarrow \kod{i}}$.

Putting both cases together, by Definition <ref> it holds

$$\mu \in \semdg{\kod{\pat}_1}{\ag}{gr_{\,\ag}(\kod{i})} \bowtie \{ \mu_{\kod{x} \rightarrow \kod{i}} \},$$

$$\mu \in \underset{\kod{i} \in names(\ag)} \bigcup \left(\ \semdg{\kod{\pat}_1}{\ag}{gr_{\,\ag}(\kod{i})} \bowtie \{ \mu_{\kod{x} \rightarrow \kod{i}} \} \ \right).$$

Finally, by Definition <ref> it holds that

$$\mu \in \semdg{\kod{ graph x \{\pat$_1$\}}}{\ag}{\kod{\gr}}.$$

* $\kod{\pat}$ is $\kod{graph i \{\pat$_1$\}}$

\begin{align*}
& \mu \in \semdg{\kod{graph i \{\pat$_1$\}}}{\ag}{\kod{\gr}} \hspace*{2mm} \text{ iff } \hspace*{-30mm} \\
& \text{(by Def \ref{definition_sem})} \hspace*{-4mm} & \text{ iff }  & \mu \in \semdg{\kod{\pat}_1}{\ag}{gr_{\,\ag}(\kod{i})} \\
& \text{(by induc.hyp.)} \hspace*{-4mm} & \text{ iff }  & \model{\nu} \hspace*{-1mm} \models \hspace*{-1mm} \sigma^{gr_{\,\ag}(\kod{i})}(\kod{\pat}_1) \text{ and } \\
&&& dom(\nu) = var(\sigma^{gr_{\,\ag}(\kod{i})}(\kod{\pat}_1)) \\
& \text{(by Def \ref{def:var})} \hspace*{-4mm} & \text{ iff }  & \model{\nu} \hspace*{-1mm} \models \hspace*{-1mm} \sigma^{gr_{\,\ag}(\kod{i})}(\kod{\pat}_1) \text{ and } \\
&&& dom(\nu) = var(\sigma(\kod{\pat})) \\
& \text{(by Def \ref{def:sigma})} \hspace*{-4mm} & \text{ iff }  & \model{\nu} \hspace*{-1mm} \models \hspace*{-1mm} \sigma(\kod{graph\,i\,\{\pat$_1$\}}) \text{ and } \\
&&& dom(\nu) = var(\sigma(\kod{\pat}))
\end{align*}

Let $\dataq$ be a dataset. Let Q be a query, $\overline{\kod{rv}}$ a set of its relevant variables and $\Phi(\overline{rv})$ its corresponding formula.
Let $\mu : \kod{VB} \rightarrow \ibl{}$ be a mapping and $\nu : \vars \rightarrow \ibl{}$ be a valuation such that $\mu \povezano \nu$.

$\mu \in \semd{\kod{Q}}{\dataq}$

if and only if

$\model{\nu} \models \Phi(\overline{rv})$  and  $dom(\nu) = var(\Phi(\overline{rv}))$.

Let $\ag$ be a query dataset of Q, $\kod{qpat}$ its query pattern and $\kod{dv}$ a set of its distinguished variables.

By Definition <ref>, from $\mu \hspace*{-2pt} \in \hspace*{-2pt} \semd{\kod{Q}}{\dataq}$, it holds $dom(\mu) \hspace*{-2pt} = \hspace*{-2pt} \overline{\kod{rv}}$.
By Definition <ref>, as $\mu \povezano \nu$, it holds $dom(\nu) = \overline{rv}$.
By Definitions <ref> and <ref>, from $\mu \in \semd{\kod{Q}}{\dataq}$, we conclude that there exists an extension $\mu'$ of $\mu$, such that $\mu' \in \semdg{\kod{qpat}}{\ag}{\mathit{df}(\ag)}$.

By Lemma <ref>, for a valuation $\nu'$ such that $\mu' \povezano \nu'$, it holds

$$\model{\nu'} \models \sigma^{\mathit{df}(\ag)}(\kod{qpat}) \text{ ~and~ }$$

$$dom(\nu') = var(\sigma^{\mathit{df}(\ag)}(\kod{qpat})).$$

Therefore, it holds

$$\model{\nu'} \models \exists \overline{ov} \  \sigma^{\mathit{df}(\ag)}(\kod{qpat}),$$

i.e. by Definition <ref>,

$$\model{\nu'} \models \Phi(\overline{rv}).$$

By Definitions <ref> and <ref>, from $\mu \povezano \nu$, $\mu' \povezano \nu'$ and $\mu \preceq \mu'$, it holds $\nu \preceq \nu'$.
By Lemma <ref>, it holds $dom(\nu) = var(\Phi(\overline{rv})$.
Therefore, $\nu$ is a restriction of $\nu'$ defined on all free variables from $\Phi(\overline{rv})$, and then it holds

$$\model{\nu} \models \Phi(\overline{rv}).$$

($\Leftarrow$) By Definition <ref>, from $\model{\nu} \models \Phi(\overline{rv})$, it holds

$$\model{\nu} \models \exists \overline{ov} \ \sigma^{\mathit{df}(\ag)}(\kod{qpat}).$$

Then, there exists an extension $\nu'$ of $\nu$ defined on $dom(\nu) \cup \overline{ov}$, such that

$$\model{\nu'} \models \sigma^{\mathit{df}(\ag)}(\kod{qpat}).$$

Therefore, from $dom(\nu) = var(\exists \overline{ov} \ \sigma^{\mathit{df}(\ag)}(\kod{qpat}))$, it holds

$$dom(\nu') = var(\sigma^{\mathit{df}(\ag)}(\kod{qpat})).$$

By Lemma <ref>, for a mapping $\mu'$ such that $\mu' \povezano \nu'$, it holds that $\mu' \in \semdg{\kod{qpat}}{\ag}{\mathit{df}(\ag)}$.
By Definitions <ref> and <ref>, from $\mu \povezano \nu$, $\mu' \povezano \nu'$ and $\nu \preceq \nu'$, it holds $\mu \preceq \mu'$.
Therefore, $\mu$ is a restriction of $\mu'$ with the following domain:

\begin{align*}
& \hspace*{27mm} dom(\mu) \hspace*{-10mm} &=\; \\
&\text{(by Def \ref{def:povezano}, as $\mu \povezano \nu$)}&=\;& \siginv(dom(\nu)) \\
& \text{(by Lemma \ref{thm:var_phi})} &=\;& \siginv(\overline{rv})\\
& &=\;& \overline{\kod{rv}} \\
& \text{(by Lemma \ref{thm:query_domain})} &=\;& \kod{var}(\kod{qpat}) \cap \overline{\kod{dv}} \\
& \text{(by Lemma \ref{thm:pattern_domain})}&=\;& dom(\mu') \cap \overline{\kod{dv}}
\end{align*}

Therefore, by Definition <ref>, $\mu = \mu'_{\overline{\kod{dv}}}$, and by Definitions <ref> and <ref>

$$\mu \in \semd{\kod{Q}}{\dataq}.$$

Note that a mapping $\mu$ is always considered as a mapping from VB to . However, in Lemma <ref>, the actual $dom(\mu)$ is a subset of V and it does not contain blank nodes (according to Definition <ref>).

$\Theta$ is valid if and only if $\kod{Q}_1$ is unsatisfiable.

($\Rightarrow$) Assume that $\kod{Q}_1$ is satisfiable.
By Definition <ref>, there exist a dataset $\dataq$ and a mapping $\mu$ such that $\mu \in \semdq{\kod{Q}}$.
Then, by Lemma <ref>, for a valuation $\nu$ such that $\mu \povezano \nu$, it holds

$$\model{\nu} \models \Phi_1(\overline{rv_1}),$$

where $\overline{\kod{rv}_1}$ is a set of relevant variables of $\kod{Q}_1$ and formula $\Phi_1(\overline{rv_1})$ corresponds to $\kod{Q}_1$.
Therefore, it holds

$$\model{\nu} \models \exists \overline{rv_1} \ \Phi_1(\overline{rv_1}).$$

By Definition <ref>, from the validity of $\Theta$, it holds

$$\model{\nu} \models \neg \big(\exists \overline{rv_1} \ \Phi_1(\overline{rv_1})\big).$$

Therefore, $\model{\nu}$ is a model of a formula and its negation, that is not possible, i.e. $\kod{Q}_1$ is unsatisfiable.

($\Leftarrow$) Assume that $\Theta$ is not valid.
Therefore, there exists an $\mathcal{L}$-structure $\mathfrak{D'} = (\mathcal{D'}, \intrprt^\mathcal{D'})$, such that $\mathfrak{D'} \models \neg \Theta$.
By Definition <ref>, $\neg \Theta$ is equal to

$$\exists \overline{rv_1} \ \Phi_1(\overline{rv_1}).$$

Note that this formula is a sentence (all variables are quantified).
By Lemma <ref>, there exists a dataset $\dataq$ and the corresponding $\mathcal{L}$-structure $\mathfrak{D} = (\mathcal{D}, \intrprt^{\mathcal{D}})$, such that

$$\mathfrak{D} \models \exists \overline{rv_1} \ \Phi_1(\overline{rv_1}).$$

Therefore, there exists a valuation $\nu$ defined on $\overline{rv_1}$, such that

$$(\mathfrak{D}, \nu) \models \Phi_1(\overline{rv_1}),$$

i.e. by Definition <ref>,

$$\model{\nu} \models \Phi_1(\overline{rv_1}).$$

By Lemma <ref>, it holds $dom(\nu) = var(\Phi_1(\overline{rv_1}))$.
Therefore, by Lemma <ref>, for a mapping $\mu$ such that $\mu \povezano \nu$, it holds

$$\mu \in \semd{\kod{Q}_1}{\dataq}.$$

This is a contradiction with the unsatisfiability of $\kod{Q}_1$.
Therefore, $\Theta$ is valid.

§.§ Soundness

The following soundness theorem states that if the Procedure <ref> claims that two queries are in the containment relation, they really are.

Let $\kod{Q}_1$ and $\kod{Q}_2$ be queries, $\Theta$ be a formula generated from $\kod{Q}_1$ (Def <ref>) and $\Psi$ be a formula generated from $\kod{Q}_1$ and $\kod{Q}_2$ (Def <ref>).
It holds $\kod{Q}_1 \sqsubseteq \kod{Q}_2$ if one of the following conditions is satisfied:

(1) $\Theta$ is valid, or

(2) $\kod{Q}_1 \seleq \kod{Q}_2$ holds and $\Psi$ is valid.

Case (1):  $\Theta$ is valid.

By Lemma <ref>, $\kod{Q}_1$ is unsatisfiable.
By Definition <ref>, $\semd{\kod{Q}_1}{\dataq}$ is an empty set for any dataset $\dataq$.
Therefore, it holds $\semd{\kod{Q}_1}{\dataq} \subseteq \semd{\kod{Q}_2}{\dataq}$, i.e. by Definition <ref>, $\kod{Q}_1 \sqsubseteq \kod{Q}_2$.

Case (2): It holds $\kod{Q}_1 \seleq \kod{Q}_2$ and $\Psi$ is valid.

Let $\dataq$ be any dataset, and $\mu$ a mapping such that

$$\mu \in \semd{\kod{Q}_1}{\dataq}.$$

By Lemma <ref>, for a valuation $\nu$ such that $\mu \povezano \nu$, it holds

$$\model{\nu} \models \Phi_1(\overline{rv_1}) \text{ and } dom(\nu) = var(\Phi_1(\overline{rv_1})).$$

By Lemma <ref>, it holds $dom(\nu) = \overline{rv_1}$.
By Lemma <ref>, as $\kod{Q}_1 \seleq \kod{Q}_2$ and $\kod{Q}_2$ does not contain projections, it holds

$$\overline{\kod{rv}_1} = \kod{var}(\kod{qpat}_2),$$

$$\sigma(\overline{\kod{rv}_1}) = \sigma(\kod{var}(\kod{qpat}_2)).$$

Then, by Lemma <ref>, it holds

$$\overline{rv_1} = var(\sigma(\kod{qpat}_2)).$$

Therefore, $dom(\nu)$ is equal to $var(\sigma(\kod{qpat}_2))$, as well.
By Lemma <ref>, as $\kod{Q}_1 \seleq \kod{Q}_2$, $\kod{Q}_2$ does not contain projections and $\Psi$ is valid, it holds

$$\model{\nu} \models \forall \overline{rv_1} \ (\Phi_1(\overline{rv_1}) \Rightarrow \sigma^{\mathit{df}({\ag_2})}(\kod{qpat}_2)).$$

As $\nu$ is defined on all free variables from formula $\Phi_1(\overline{rv_1}) \Rightarrow \sigma^{\mathit{df}({\ag_2})}(\kod{qpat}_2)$, it holds:

$$\model{\nu} \models \Phi_1(\overline{rv_1}) \Rightarrow \sigma^{\mathit{df}({\ag_2})}(\kod{qpat}_2).$$

From $\model{\nu} \models \Phi_1(\overline{rv_1})$, it holds

$$\model{\nu} \models \sigma^{\mathit{df}({\ag_2})}(\kod{qpat}_2).$$

Then, by Lemma <ref>, as $\mu \povezano \nu$ and $dom(\nu) = var(\sigma(\kod{qpat}_2))$, it holds

$$\mu \in \semdg{\kod{qpat}_2}{{\ag_2}}{\mathit{df}({\ag_2})},$$

i.e. by Definition <ref>, as $\kod{Q}_2$ does not contain projections, it holds

$$\mu \in \semd{\kod{Q}_2}{\dataq}.$$

Therefore, each element of the set $\semd{\kod{Q}_1}{\dataq}$ belongs to the set $\semd{\kod{Q}_2}{\dataq}$ for any dataset $\dataq$, i.e. $\semd{\kod{Q}_1}{\dataq} \subseteq \semd{\kod{Q}_2}{\dataq}$.
By Definition <ref>, it holds $\kod{Q}_1 \sqsubseteq \kod{Q}_2$.

Soundness theorem for subsumption (dual to Theorem <ref>) can be proved as well.
It validates the results of Procedure <ref>.

Let $\kod{Q}_1$ and $\kod{Q}_2$ be queries, $\Theta$ be a formula generated from $\kod{Q}_1$ (Def <ref>) and $\Psi$ be a formula generated from $\kod{Q}_1$ and $\kod{Q}_2$ (Def <ref>).
It holds $\kod{Q}_1 \dot{\sqsubseteq} \kod{Q}_2$ if one of the following conditions is satisfied:

(1) $\Theta$ is valid, or

(2) $\kod{Q}_1 \dot{\seleq} \kod{Q}_2$ holds and $\Psi$ is valid.

This proof is equal to the proof of Theorem <ref>, from beginning to the applying Lemma <ref>.
Instead of it, in the subsumption case, we apply its dual lemma, i.e. Lemma <ref>, and from $\kod{Q}_1 \dot{\seleq} \kod{Q}_2$ it holds

$$\overline{\kod{rv}_1} \subseteq \kod{var}(\kod{qpat}_2) \cap \overline{\kod{dv}_2},$$

$$\sigma(\overline{\kod{rv}_1}) \subseteq \sigma(\kod{var}(\kod{qpat}_2) \cap \overline{\kod{dv}_2}),$$

and, by Definition <ref>, it holds

$$\sigma(\overline{\kod{rv}_1}) \subseteq \sigma(\kod{var}(\kod{qpat}_2)) \cap \sigma(\overline{\kod{dv}_2}).$$

Therefore, by Lemma <ref>, it holds

\begin{equation}
\label{eq:subsumpt1}
\overline{rv_1} \subseteq var(\sigma(\kod{qpat}_2)) \cap \overline{dv_2},
\end{equation}

The rest of the proof follows.

Let $\nu'$ denote any extension of $\nu$, such that $dom(\nu') = dom(\nu) \cup (var(\sigma(\kod{qpat}_2)) \setminus \overline{ov_2})$.
By Definitions <ref> and <ref>, as $\Psi$ is valid, it holds

$$\model{\nu'} \models \forall \overline{rv_1} \ (\Phi_1(\overline{rv_1}) \Rightarrow \exists \overline{ov_2} \ \sigma^{\mathit{df}({\ag_2})}(\kod{qpat}_2)).$$

As $\nu'$ is defined on all free variables from formula $\Phi_1(\overline{rv_1}) \Rightarrow \exists \overline{ov_2} \ \sigma^{\mathit{df}({\ag_2})}(\kod{qpat}_2)$, it holds:

$$\model{\nu'} \models \Phi_1(\overline{rv_1}) \Rightarrow \exists \overline{ov_2} \ \sigma^{\mathit{df}({\ag_2})}(\kod{qpat}_2).$$

From $\model{\nu} \models \Phi_1(\overline{rv_1})$, as $\nu' \succeq \nu$ it holds $\model{\nu'} \models \Phi_1(\overline{rv_1})$.
Therefore, it holds

$$\model{\nu'} \models \exists \overline{ov_2} \ \sigma^{\mathit{df}({\ag_2})}(\kod{qpat}_2).$$

Then, there exists $\nu''$, an extension of $\nu'$, such that $dom(\nu'') = dom(\nu') \cup \overline{ov_2}$ and

$$\model{\nu''} \models \sigma^{\mathit{df}({\ag_2})}(\kod{qpat}_2).$$

\begin{align*}
& \text{Also: } dom(\nu'') \hspace*{-3mm}& = & \\
& \text{(by constr.)} & = & dom(\nu) \cup (var(\sigma(\kod{qpat}_2)) \setminus \overline{ov_2}) \cup \overline{ov_2} \\
&  & = & dom(\nu) \cup var(\sigma(\kod{qpat}_2)) \cup \overline{ov_2}\\
& \text{(by Def \ref{def:phi})} & = & dom(\nu) \cup var(\sigma(\kod{qpat}_2)) \cup \\
&&& (var(\sigma(\kod{qpat}_2)) \setminus \overline{rv}_1)\\
&  & = & dom(\nu) \cup var(\sigma(\kod{qpat}_2)) \\
& \text{(} dom(\nu) = \overline{rv_1}\text{)} \hspace*{-3mm} & = & \overline{rv_1} \cup var(\sigma(\kod{qpat}_2))\\
& \text{(by (\ref{eq:subsumpt1}))} & = & var(\sigma(\kod{qpat}_2)).
\end{align*}

Therefore, by Lemma <ref>, for a mapping $\mu''$ such that $\mu'' \povezano \nu''$, it holds

$$\mu'' \in \semdg{\kod{qpat}_2}{{\ag_2}}{\mathit{df}({\ag_2})}.$$

By Lemma <ref>, $dom(\mu'') = \kod{var}(\kod{qpat}_2)$.
By Definition <ref>, it holds $\mu''_{\overline{\kod{dv}_2}} \in \semd{\kod{Q}_2}{\dataq}$, while

$$dom(\mu''_{\overline{\kod{dv}_2}}) = \kod{var}(\kod{qpat}_2) \cap \overline{\kod{dv}_2}.$$

By Definitions <ref> and <ref>, from $\mu \povezano \nu$, $\mu'' \povezano \nu''$ and $\nu \preceq \nu''$, it holds $\mu \preceq \mu''$.
Therefore, $\mu$ and $\mu''_{\overline{\kod{dv}_2}}$ are restrictions of $\mu''$.
By Definition <ref>, as $\kod{Q}_1 \dot{\seleq} \kod{Q}_2$, it holds $\overline{\kod{rv}_1} \subseteq \overline{\kod{rv}_2}$.
Then, by Lemma <ref>, it holds $\kod{var}(\kod{qpat}_1) \cap \overline{\kod{dv}_1} \subseteq \kod{var}(\kod{qpat}_2) \cap \overline{\kod{dv}_2}$, i.e. $dom(\mu) \subseteq dom(\mu''_{\overline{\kod{dv}_2}})$ and $\mu \preceq \mu''_{\overline{\kod{dv}_2}}$.
Therefore, for each element of the set $\semd{\kod{Q}_1}{\dataq}$ there exists an extension that belongs to the set $\semd{\kod{Q}_2}{\dataq}$ for any dataset $\dataq$.
By Definition <ref>, it holds $\kod{Q}_1 \dot{\sqsubseteq} \kod{Q}_2$.

§.§ Completeness

The following completeness theorem states that for each pair of queries satisfying the containment relation, the Procedure <ref> will confirm that.

Let $\kod{Q}_1$ and $\kod{Q}_2$ be queries, $\Theta$ be a formula generated from $\kod{Q}_1$ (Def <ref>) and $\Psi$ be a formula generated from $\kod{Q}_1$ and $\kod{Q}_2$ (Def <ref>).
If $\kod{Q}_1 \sqsubseteq \kod{Q}_2$ holds, then one of the following conditions is satisfied:

(1) $\Theta$ is valid, or

(2) $\kod{Q}_1 \seleq \kod{Q}_2$ holds and $\Psi$ is valid.

Case (1): $\kod{Q}_1$ is unsatisfiable.

By Lemma <ref>, from the unsatisfiability of $\kod{Q}_1$, $\Theta$ is valid.

Case (2): $\kod{Q}_1$ is satisfiable.

We prove $\kod{Q}_1 \seleq \kod{Q}_2$ and the validity of $\Psi$.
As query $\kod{Q}_1$ is satisfiable, there exists a dataset $\dataq$ and a mapping $\mu$ such that $\mu \in \semd{\kod{Q}_1}{\dataq}$.
By Definition <ref>, from $\kod{Q}_1 \sqsubseteq \kod{Q}_2$, it holds $\semd{\kod{Q}_1}{\dataq} \subseteq \semd{\kod{Q}_2}{\dataq}$.
Therefore, it holds $\mu \in \semd{\kod{Q}_2}{\dataq}$.
By Definition <ref>, it holds $dom(\mu) = \overline{\kod{rv}_1}$ and $dom(\mu) = \overline{\kod{rv}_2}$.

Therefore, it holds $\overline{\kod{rv}_1} = \overline{\kod{rv}_2}$, i.e. by Definition <ref>, $\kod{Q}_1 \seleq \kod{Q}_2$.

Let us assume that $\Psi$ is not valid.
Therefore, there exists an $\mathcal{L}$-structure $\mathfrak{D'} = (\mathcal{D'}, \intrprt^\mathcal{D'})$, such that $\mathfrak{D'} \models \neg \Psi$.
By Lemma <ref>, as $\kod{Q}_1 \seleq \kod{Q}_2$ and $\kod{Q}_2$ does not contain projections, $\neg \Psi$ is equal to

\begin{align}
\label{eq:for_subsumption0}
\neg \Big(\forall \overline{rv_1} \big( \Phi_1(\overline{rv}_1) \Rightarrow \sigma^{{\mathit{df}({\ag_2})}}(\kod{qpat}_2)\big)\Big),
\end{align}

where $\ag_2$ is a query dataset of $\kod{Q}_2$, i.e.

\begin{align}
\label{eq:for_subsumption1}
\exists \overline{rv_1} \ \big( \Phi_1(\overline{rv}_1) \wedge \neg \sigma^{{\mathit{df}({\ag_2})}}(\kod{qpat}_2) \big).
\end{align}

Note that this formula is a sentence (all variables are quantified).
By Lemma <ref>, there exists a dataset $\dataq$ and the corresponding $\mathcal{L}$-structure $\mathfrak{D} = (\mathcal{D}, \intrprt^{\mathcal{D}})$, such that

\begin{align}
\label{eq:for_subsumption2}
\mathfrak{D} \models \exists \overline{rv_1} \ \big( \Phi_1(\overline{rv}_1) \wedge \neg \sigma^{{\mathit{df}({\ag_2})}}(\kod{qpat}_2) \big).
\end{align}

Therefore, there exists a valuation $\nu$ defined on $\overline{rv_1}$, such that

\begin{align}
\label{eq:for_subsumption3}
(\mathfrak{D}, \nu) \models \Phi_1(\overline{rv}_1) \wedge \neg \sigma^{{\mathit{df}({\ag_2})}}(\kod{qpat}_2),
\end{align}

i.e. by Definition <ref>,

\begin{align}
\label{eq:for_subsumption4}
\model{\nu} \models \Phi_1(\overline{rv}_1) \text{~~~and~~~} \model{\nu} \models \neg \sigma^{{\mathit{df}({\ag_2})}}(\kod{qpat}_2).
\end{align}

By Lemma <ref>, it holds $dom(\nu) = var(\Phi_1(\overline{rv_1}))$.
Therefore, by Lemma <ref>, for a mapping $\mu$ such that $\mu \povezano \nu$, it holds

$$\mu \in \semd{\kod{Q}_1}{\dataq}.$$

By Lemma <ref>, as $\kod{Q}_1 \seleq \kod{Q}_2$ and $\kod{Q}_2$ does not contain projection, it holds

$$\overline{\kod{rv}_1} = \kod{var}(\kod{qpat}_2).$$

Therefore, it holds

$$\sigma(\overline{\kod{rv}_1}) = \sigma(\kod{var}(\kod{qpat}_2)),$$

i.e. by Lemma <ref>,

$$\overline{rv_1} = var(\sigma(\kod{qpat}_2)).$$

Therefore, $dom(\nu)$ is equal to $var(\sigma(\kod{qpat}_2))$, and then, by Lemma <ref>, it holds

$$\mu \notin \semdg{\kod{qpat}_2}{{\ag_2}}{{\mathit{df}({\ag_2})}}.$$

Then, by Definition <ref>, as query $\kod{Q}_2$ does not have projections, it holds

$$\mu \notin \semd{\kod{Q}_2}{{\dataq}}.$$

We conclude that $\semd{\kod{Q}_1}{\dataq} \subseteq \semd{\kod{Q}_2}{\dataq}$ does not hold, i.e. by Definition <ref>, it does not hold $\kod{Q}_1 \sqsubseteq \kod{Q}_2$.
This is a contradiction with the theorem assumption.
Therefore, $\Psi$ is valid.

Completeness theorem for subsumption (dual to Theorem <ref>) can be proved as well.

Let $\kod{Q}_1$ and $\kod{Q}_2$ be queries, $\Theta$ be a formula generated from $\kod{Q}_1$ (Def <ref>) and $\Psi$ be a formula generated from $\kod{Q}_1$ and $\kod{Q}_2$ (Def <ref>).
If $\kod{Q}_1 \dot{\sqsubseteq} \kod{Q}_2$ holds, then one of the following conditions is satisfied:

(1) $\Theta$ is valid, or

(2) $\kod{Q}_1 \dot{\seleq} \kod{Q}_2$ holds and $\Psi$ is valid.

In the case when $\kod{Q}_1$ is unsatisfiable, the proof is exactly the same as the proof of Theorem <ref>.
Otherwise, the proof of $\kod{Q}_1 \dot{\seleq} \kod{Q}_2$ is done in the similar way as in the proof of Theorem <ref>:
By Definition <ref>, as query $\kod{Q}_1$ is satisfiable, there exists a dataset $\dataq$ and a mapping $\mu$ such that $\mu \in \semd{\kod{Q}_1}{\dataq}$.
By Definition <ref>, from $\kod{Q}_1 \dot{\sqsubseteq} \kod{Q}_2$, there exists an extension $\mu'$ of $\mu$ ($dom(\mu) \subseteq dom(\mu')$) such that $\mu' \in \semd{\kod{Q}_2}{\dataq}$.
By Definition <ref>, it holds $dom(\mu) = \overline{\kod{rv}_1}$ and $dom(\mu') = \overline{\kod{rv}_2}$.
Therefore, it holds $\overline{\kod{rv}_1} \subseteq \overline{\kod{rv}_2}$, i.e. by Definition <ref>, $\kod{Q}_1 \dot{\seleq} \kod{Q}_2$.

In the rest of the proof, until the applying Lemma <ref>, the following changes are necessary.
Instead of satisfiabilities (<ref>), (<ref>), (<ref>), (<ref>) and (<ref>), in the subsumption case, as $\kod{Q}_2$ can contain projections, it holds respectively:

\begin{align*}
\neg \Big(\forall \overline{rv_1} \big( \Phi_1(\overline{rv}_1) \Rightarrow \exists \overline{ov_2} \  \sigma^{{\mathit{df}({\ag_2})}}(\kod{qpat}_2)\big)\Big)\\
\exists \overline{rv_1} \ \big( \Phi_1(\overline{rv}_1) \wedge \neg (\exists \overline{ov_2} \ \sigma^{{\mathit{df}({\ag_2})}}(\kod{qpat}_2)) \big)\\
\mathfrak{D} \models \exists \overline{rv_1} \ \big( \Phi_1(\overline{rv}_1) \wedge \forall \overline{ov_2} \ \neg \sigma^{{\mathit{df}({\ag_2})}}(\kod{qpat}_2) \big)\\
(\mathfrak{D}, \nu) \models \Phi_1(\overline{rv}_1) \wedge \forall \overline{ov_2} \ \neg \sigma^{{\mathit{df}({\ag_2})}}(\kod{qpat}_2)\\
\model{\nu} \models \Phi_1(\overline{rv}_1) \text{~~~and~~~} \model{\nu} \models \forall \overline{ov_2} \ \neg \sigma^{{\mathit{df}({\ag_2})}}(\kod{qpat}_2)
\end{align*}

The rest of the proof follows.
By Definition <ref>, from $\mu \in \semd{\kod{Q}_1}{\dataq}$ and $\kod{Q}_1 \dot{\sqsubseteq} \kod{Q}_2$, there exists a mapping $\mu'$ such that $\mu \preceq \mu'$ and $\mu' \in \semd{\kod{Q}_2}{\dataq}$.

By Lemma <ref>, for a valuation $\nu'$, such that $\mu' \povezano \nu'$, it holds

$$\model{\nu'} \models \Phi_2(\overline{rv_2}),$$

i.e. by Definition <ref>,

$$\model{\nu'} \models \exists \dot{\overline{ov_2}} \ \sigma^{{\mathit{df}({\ag_2})}}(\kod{qpat}_2),$$

where $\dot{\overline{ov_2}} = var(\sigma^{{\mathit{df}({\ag_2})}}(\kod{qpat}_2)) \setminus \overline{rv_2}$.
Note that by Definitions <ref> and <ref>, as $\mu \povezano \nu$, $\mu' \povezano \nu'$, and $\mu \preceq \mu'$, it holds $\nu \preceq \nu'$.
There exists an extension $\nu''$ of $\nu'$ to the variables from $\dot{\overline{ov_2}}$, such that

$$\model{\nu''} \models \sigma^{{\mathit{df}({\ag_2})}}(\kod{qpat}_2),$$

but also

$$\model{\nu''} \models \exists \overline{ov_2} \ \sigma^{{\mathit{df}({\ag_2})}}(\kod{qpat}_2).$$

From $\nu \preceq \nu'$ and $\nu' \preceq \nu''$, $\nu$ is a restriction of $\nu''$.
Therefore, it holds

$$\model{\nu''} \models \forall \overline{ov_2} \ \neg \sigma^{{\mathit{df}({\ag_2})}}(\kod{qpat}_2).$$

This is a contradiction, as $\model{\nu''}$ is a model of both, a formula and its negation.
Therefore, $\Psi$ is valid.

§ DEALING WITH NON-CONJUNCTIVE QUERIES

The containment problem of non-conjunctive queries, or more precisely queries containing the operators union (Section <ref>) and optional (Section <ref>), and containing subqueries (Section <ref>) can be transformed and/or reduced to the containment problem over (a set of) conjunctive queries presented in Section <ref>.
Having correctness proved for conjunctive queries (Section <ref>), the query containment problem for non-conjunctive queries presented in this section is reduced to a sound and complete approach.

§.§ Operator union

Dealing with queries containing the union operator requires a transformation of their graph patterns into a special equivalent form where the union operator can appear only outside the scope of other operators.
This condition is presented in the following definition.

A simple normal form of a graph pattern is a graph pattern containing $n$ union-free graph patterns $\kod{\pat}^\kod{i} \; \; (1 \le \kod{i} \le \kod{n})$ connected with $n-1$ union operators:

$$\kod{\pat}^1 \ \kod{union} \ \kod{\pat}^2  \ \dots \ \kod{union} \ \kod{\pat}^\kod{n}$$

Each graph pattern can be reduced to an equivalent pattern in a simple normal form following a standard DNF-style expansion [Pérez et al., 2006].

For queries $\kod{Q}_\kod{1}$ and $\kod{Q}_\kod{2}$ of the form $\kod{select} ~ \overline{\kod{dv}} \ \kod{qpat}_\kod{1}$ and $\kod{select} \ \kod{*} \ \kod{qpat}_\kod{2}$ respectively, where query patterns $\kod{qpat}_\kod{1}$ and $\kod{qpat}_\kod{2}$ are in simple normal form consisting of union-free  graph patterns $\kod{\pat}_\kod{1}^\kod{i}$ ($1 \le \kod{i} \le \kod{m}$) and $\kod{\pat}_\kod{2}^\kod{j}$ ($1 \le \kod{j} \le \kod{n}$) respectively, queries $\kod{Q}_\kod{1}^\kod{i}$ ($1 \le \kod{i} \le \kod{m}$) and
$\kod{Q}_\kod{2}^\kod{j}$ ($1 \le \kod{j} \le \kod{n}$) are defined as:

$\kod{Q}_\kod{1}^\kod{i} = \kod{select} ~ \overline{\kod{dv}} \ \kod{\{} \kod{\pat}_\kod{1}^\kod{i} \kod{\}}$,

$\kod{Q}_\kod{2}^\kod{j} = \kod{select} \ \kod{*}  \kod{\{} \kod{\pat}_\kod{2}^\kod{j} \kod{\}}$,

where from and from named clauses of queries $\kod{Q}_\kod{1}$ and $\kod{Q}_\kod{2}$ are propagated to the queries $\kod{Q}_\kod{1}^\kod{i}$ and $\kod{Q}_\kod{2}^\kod{j}$, respectively.
It holds:

$\kod{Q}_\kod{1} \sqsubseteq \kod{Q}_\kod{2}$

if and only if

for each $i$, $1 \le \kod{i} \le \kod{m}$

there exists $j$, $1 \le \kod{j} \le \kod{n}$,

such that  $\kod{Q}_\kod{1}^\kod{i} \sqsubseteq \kod{Q}_\kod{2}^\kod{j}$.

In order to prove this direction of lemma,
for any $\kod{i}=\kod{1}..\kod{m}$, there should be $\kod{j}=\kod{1}..\kod{n}$ such that $\kod{Q}_\kod{1}^\kod{i} \sqsubseteq \kod{Q}_\kod{2}^\kod{j}$.
Assume that

$$\mu \in \semd{\kod{Q}_\kod{1}^\kod{i}}{\dataq},$$

for some $\kod{i}$, $\kod{i} \in \{\kod{1}, \dots, \kod{m}\}$ and some dataset $\dataq$.
By Definitions <ref> and <ref>, there exists a mapping $\mu'$, such that $\mu = \mu'_{\overline{\kod{dv}}}$, and $\mu' \in \semdg{\kod{\pat}_\kod{1}^\kod{i}}{\ag_1}{\mathit{df}(\ag_1)}$, where $\ag_1$ is a query dataset specified by the from and from named clauses of query $\kod{Q}_\kod{1}^\kod{i}$, and also of query $\kod{Q}_\kod{1}$.
By Definition <ref>, it holds

$$\mu' \in \semdg{\kod{\pat}_\kod{1}^\kod{1} \ \kod{union} \ \dots \ \kod{union} \ \kod{\pat}_\kod{1}^\kod{m}}{\ag_1}{\mathit{df}(\ag_1)}.$$

By Definitions <ref> and <ref>, it holds

$$\mu \in \semd{\kod{Q}_\kod{1}}{\dataq},$$

and also, as $\kod{Q}_\kod{1} \sqsubseteq \kod{Q}_\kod{2}$,

$$\mu \in \semd{\kod{Q}_\kod{2}}{\dataq}.$$

By Definitions <ref> and <ref>, as there is no projections in $\kod{Q}_\kod{2}$,

$$\mu \in \semdg{\kod{\pat}_\kod{2}^\kod{1} \ \kod{union} \ \dots \ \kod{union} \ \kod{\pat}_\kod{2}^\kod{n}}{\ag_2}{\mathit{df}(\ag_2)},$$

where $\ag_2$ is a query dataset specified by the from and from named clauses of query $\kod{Q}_\kod{2}$, and also of every query $\kod{Q}_\kod{2}^\kod{j}, \kod{j}=\kod{1}..\kod{n}$.
By Definition <ref>, it holds

$$\mu \in \semdg{\kod{\pat}_\kod{2}^\kod{j}}{\ag_2}{\mathit{df}(\ag_2)},$$

for some index $\kod{j}$, $\kod{j} \in \{\kod{1}, \dots ,\kod{n}\}$.
By Definitions <ref> and <ref>, as there is no projections in $\kod{Q}_\kod{2}^\kod{j}$, it holds

$$\mu \in \semd{\kod{Q}_\kod{2}^\kod{j}}{\dataq}.$$

Let $\mu$ be a mapping, and $\dataq$ a dataset.
Assume that

$$\mu \in \semd{\kod{Q}_\kod{1}}{\dataq}.$$

By Definitions <ref> and <ref>, there exists a mapping $\mu'$, such that $\mu = \mu'_{\overline{\kod{dv}}}$, and

$$\mu' \in \semdg{\kod{\pat}_\kod{1}^\kod{1} \ \kod{union} \ \dots \ \kod{union} \ \kod{\pat}_\kod{1}^\kod{m}}{\ag_1}{\mathit{df}(\ag_1)},$$

where $\ag_1$ is a query dataset specified by the from and from named clauses of query $\kod{Q}_\kod{1}$, and also of every query $\kod{Q}_\kod{1}^\kod{i}, \kod{i}=\kod{1}..\kod{m}$.
By Definition <ref>, there exists an index $\kod{i}$, $\kod{i} \in \{\kod{1}, \dots, \kod{m}\}$, such that $\mu' \in \semdg{\kod{\pat}_\kod{1}^\kod{i}}{\ag_1}{\mathit{df}(\ag_1)}$.
By Definitions <ref> and <ref>,
it holds

$$\mu \in \semd{\kod{Q}_\kod{1}^\kod{i}}{\dataq}.$$

By the assumption, there exists an index $\kod{j}$, $\kod{j} \in \{\kod{1}, \dots, \kod{n}\}$, such that

$$\mu \in \semd{\kod{Q}_\kod{2}^\kod{j}}{\dataq}.$$

By Definitions <ref> and <ref>, as there is no projections in $\kod{Q}_\kod{2}^\kod{j}$,

$$\mu \in \semdg{\kod{\pat}_\kod{2}^\kod{j}}{\ag_2}{\mathit{df}(\ag_2)},$$

where $\ag_2$ is a query dataset specified by the from and from named clauses of query $\kod{Q}_\kod{2}^\kod{j}$, and also of query $\kod{Q}_\kod{2}$.
By Definition <ref>, it holds

$$\mu \in \semdg{\kod{\pat}_\kod{2}^\kod{1} \ \kod{union} \ \dots \ \kod{union} \ \kod{\pat}_\kod{2}^\kod{n}}{\ag_2}{\mathit{df}(\ag_2)},$$

i.e. by Definitions <ref> and <ref>,

$$\mu \in \semd{\kod{Q}_\kod{2}}{\dataq}.$$

Following Lemma <ref>, the query containment problem of queries $\kod{Q}_\kod{1}$ and $\kod{Q}_\kod{2}$ can be reduced to the checks if for each $i$ ($1 \le \kod{i} \le \kod{m}$) there exists $j$ ($1 \le \kod{j} \le \kod{n}$) such that $\kod{Q}_\kod{1}^\kod{i} \sqsubseteq \kod{Q}_\kod{2}^\kod{j}$.
The soundness and the completeness of the proposed modeling are a direct consequence of this lemma.

For the query subsumption problem, a weaker form of Lemma <ref> is needed, considering relation $\dot{\sqsubseteq}$ instead of $\sqsubseteq$, whose proof is analogous.

§.§ Operator optional

All graph patterns explained so far demand to be matched completely. However, it is very useful to have possibility to add an information to the solution where the information is available, but do not reject the solution because some part of the query pattern does not match. Optional matching provides this facility.

For efficient usage of operator optional in practice, it is necessary to consider only well-designed graph patterns [Pichler and Skritek, 2014, Pérez et al., 2009, Pérez et al., 2006].

A pattern $\kod{pat}$ is well-designed if for all its subpatterns of the form $\kod{\pat}_1 \; \kod{optional} \; \kod{\pat}_2$, it holds that all variables appearing in $\kod{\pat}_2$, but not in $\kod{\pat}_1$, cannot appear in $\kod{pat}$ anywhere else except in $\kod{\pat}_2$.

The same restriction is also necessary for operators minus and diff.

Operator optional can be reduced to a union of a conjunction and a negation, as proved in Lemma <ref>.

Let $\ag$ be an  dataset,  a graph within $\ag$, $\kod{\pat}_1$ and $\kod{\pat}_2$ graph patterns.

$\semdg{\kod{\pat}_1 \kod{ optional } \kod{\pat}_2}{\ag}{\kod{\gr}} = \semdg{\kod{\pat}_1 \, \kod{.} \,  \kod{\pat}_2 \ \kod{ union } \  \kod{\pat}_1 \; \kod{diff} \; \kod{\pat}_2}{\ag}{\kod{\gr}}$.

This is a direct corollary of Definitions <ref> and <ref>.

Note that a graph pattern being introduced by a previously described reduction of a well-designed optional pattern is, by  Definition <ref>, also a well-designed pattern.

§.§ Subqueries as Graph Patterns

Subqueries allow embedding queries within other queries in order to facilitate a composition of new queries and a reuse of existing queries.
Subqueries are simpler than queries because they cannot contain from and from named clauses, and are used in a place of a graph pattern [Angles and Gutiérrez, 2011].
During the evaluation of a query, the inner most subquery is evaluated first (according to Definition <ref>), its results are projected up to the outer query, and only distinguished variables are visible (in scope) to the outer query (according to Definition <ref>).

In this section, we present a subquery elimination procedure, i.e. reduction of a query to an equivalent query without a subquery. We prove the correctness of this procedure.
In order to simplify the proofs, we assume that queries do not contain graph, diff, and minus operators. If these operators are present, the subquery elimination is also possible, as the expressive power of the  language with and without subqueries is the same [Kaminski et al., 2016].

Definition <ref> presents a special form of a graph pattern that simplifies reducing a graph pattern with a subquery into an equivalent query (by Definition <ref>) without the subquery.

A graph pattern $\kod{\pat}$ is in filter-normal form if:

(i) $\kod{\pat}$ is a triple pattern,

(ii) $\kod{\pat}$ is $\kod{\{Q$_\kod{sq}$\}}$ and the query pattern $\kod{qpat}_\kod{sq}$ of $\kod{Q$_\kod{sq}$}$ is in filter-normal form,

(iii) $\kod{\pat}$ is $\kod{\pat}_1 \kod{.} \kod{\pat}_2$, where $\kod{\pat}_1$ and $\kod{\pat}_2$ are in filter-normal form (i), (ii) or (iii),

(iv) $\kod{\pat}$ is $\kod{\pat}_1 \kod{ filter R}$ and $\kod{\pat}_1$ is in filter-normal form (i), (ii) or (iii).

The following lemma shows that any graph pattern (considered so far) can be reduced to a graph pattern in filter-normal form.

Let $\ag$ be an  dataset and  a graph within $\ag$.
For any graph pattern $\kod{\pat}$ there exists a graph pattern $\kod{\pat}'$ in filter-normal form such that:

$\semdg{\kod{\pat}}{\ag}{\kod{G}} = \semdg{\kod{\pat}'}{\ag}{\kod{G}}.$

The lemma is proved by induction over graph pattern $\kod{\pat}$.

*  is

By Definition <ref>, $\kod{\pat}$ is in filter-normal form.

* $\kod{\pat}$ is $\kod{\pat}_1 . \kod{\pat}_2$

By Definition <ref>, it holds

$$\semdg{\kod{\pat}}{\ag}{\kod{G}} = \semdg{\kod{\pat}_1}{\ag}{\kod{G}} \bowtie \semdg{\kod{\pat}_2}{\ag}{\kod{G}}.$$

By induction hypothesis, for $\kod{\pat}_1$ and $\kod{\pat}_2$ there exist graph patterns $\kod{\pat}_1'$ and $\kod{\pat}_2'$ in filter-normal form such that
$$\semdg{\kod{\pat}_1}{\ag}{\kod{G}} = \semdg{\kod{\pat}_1'}{\ag}{\kod{G}} \text{ and }$$

$$\semdg{\kod{\pat}_2}{\ag}{\kod{G}} = \semdg{\kod{\pat}_2'}{\ag}{\kod{G}}.~~~~~~~$$

Case 1: $\kod{\pat}_1'$ and $\kod{\pat}_2'$ are of the form (i), (ii) or (iii).

Let $\kod{\pat}'$ denote $\kod{\pat}_1' . \kod{\pat}_2'$.
Then, by Definition <ref>, it holds

$$\semdg{\kod{\pat}'}{\ag}{\kod{G}} = \semdg{\kod{\pat}_1'}{\ag}{\kod{G}} \bowtie \semdg{\kod{\pat}_2'}{\ag}{\kod{G}},$$

$$\semdg{\kod{\pat}'}{\ag}{\kod{G}} = \semdg{\kod{\pat}_1}{\ag}{\kod{G}} \bowtie \semdg{\kod{\pat}_2}{\ag}{\kod{G}}.$$

Therefore, it holds $\semdg{\kod{\pat}}{\ag}{\kod{G}} = \semdg{\kod{\pat}'}{\ag}{\kod{G}}$ and by Definition <ref>, $\kod{\pat}'$ is in filter-normal form.

Case 2: $\kod{\pat}_1'$ has the form (iv), i.e.

$\kod{\pat}_1' = \kod{\pat}_1'' \kod{ filter R}_1$,
while $\kod{\pat}_2'$ is of the form (i), (ii) or (iii).

Then, it holds

$$\semdg{\kod{\pat}_1'}{\ag}{\kod{G}} \bowtie \semdg{\kod{\pat}_2'}{\ag}{\kod{G}} = \semdg{\kod{\pat}_1'' \kod{ filter R}_1}{\ag}{\kod{G}} \bowtie \semdg{\kod{\pat}_2'}{\ag}{\kod{G}},$$

i.e. by Definition <ref>,

$$\semdg{\kod{\pat}_1'}{\ag}{\kod{G}} \hspace*{-2pt} \bowtie \hspace*{-2pt} \semdg{\kod{\pat}_2'}{\ag}{\kod{G}} \hspace*{-2pt} = \hspace*{-2pt} \{ \mu \hspace*{-2pt} \in \hspace*{-2pt} \semdg{\kod{\pat}_1''}{\ag}{\kod{\gr}} \ | \ \mu \zadovoljava \kod{R}_1 \} \hspace*{-1pt} \bowtie \hspace*{-1pt} \semdg{\kod{\pat}_2'}{\ag}{\kod{G}}.$$

By Definition <ref>, if for a mapping $\mu \in \semdg{\kod{\pat}_1''}{\ag}{\kod{\gr}}$, it holds $\mu \zadovoljava \kod{R}_1$, then for its extension $\mu \cup \mu_2$, where $\mu_2 \in \semdg{\kod{\pat}_2'}{\ag}{\kod{G}}$ and $\mu_2 \comp \mu$, it holds $\mu \cup \mu_2 \zadovoljava \kod{R}_1$.
Therefore, it holds:

$$\semdg{\kod{\pat}_1'}{\ag}{\kod{G}} \bowtie \semdg{\kod{\pat}_2'}{\ag}{\kod{G}} = $$

$$\{ \mu \cup \mu_2 \in \semdg{\kod{\pat}_1''}{\ag}{\kod{\gr}} \bowtie \semdg{\kod{\pat}_2'}{\ag}{\kod{\gr}} \ | \ \mu  \cup \mu_2 \zadovoljava \kod{R}_1 \},$$

i.e. by Definition <ref>,

$$\semdg{\kod{\pat}_1'}{\ag}{\kod{G}} \bowtie \semdg{\kod{\pat}_2'}{\ag}{\kod{G}} = \semdg{(\kod{\pat}_1'' \kod{.} \kod{\pat}_2') \kod{ filter R}_1}{\ag}{\kod{G}}.$$

By Definition <ref>, $(\kod{\pat}_1'' \kod{.} \kod{\pat}_2') \kod{ filter R}_1$ is in the filter-normal form, and it holds

$$\semdg{\kod{\pat}}{\ag}{\kod{G}} = \semdg{(\kod{\pat}_1'' \kod{.} \kod{\pat}_2') \kod{ filter R}_1}{\ag}{\kod{G}}.$$

Case 3: $\kod{\pat}_2'$ is in the form (iv), while $\kod{\pat}_1'$ is in the form (i), (ii) or (iii).

This case is reduced to the previous one because of the commutativity of the  operator . [Pérez et al., 2006], i.e.

$$\semdg{\kod{\pat}_1'}{\ag}{\kod{G}} \bowtie \semdg{\kod{\pat}_2'}{\ag}{\kod{G}} = \semdg{\kod{\pat}_2'}{\ag}{\kod{G}} \bowtie \semdg{\kod{\pat}_1'}{\ag}{\kod{G}}.$$

Case 4: $\kod{\pat}_1'$ and $\kod{\pat}_2'$ are in the form (iv), i.e. in the form $\kod{\pat}_1'' \kod{ filter R}_1$ and $\kod{\pat}_2'' \kod{ filter R}_2$, respectively.

Applying construction of a normal form from the cases 2 and 3, we get:

$$\semdg{\kod{\pat}}{\ag}{\kod{G}} = \semdg{(\kod{\pat}_1'' \kod{.} \kod{\pat}_2'') \kod{ filter R}_1 \kod{ filter R}_2}{\ag}{\kod{G}},$$

i.e. by Definition <ref>, it holds

$$\semdg{\kod{\pat}}{\ag}{\kod{G}} = \semdg{(\kod{\pat}_1'' \kod{.} \kod{\pat}_2'') \kod{ filter R}_1 \kod{\&\&R}_2}{\ag}{\kod{G}}.$$

By Definition <ref>, $(\kod{\pat}_1'' \kod{.} \kod{\pat}_2'') \kod{ filter R}_1 \kod{\&\&R}_2$ is in the filter-normal form.

Note that all the variables appearing in filter clause (cases 2, 3 and 4) appear also in the graph pattern in front of it.
This is a consequence of the same feature that holds for the initial graph patterns, while this transformation preserves it.

* $\kod{\pat}$ is $\kod{\pat}_1 \kod{ filter } \kod{R}$

By Definition <ref>, it holds

$$\semdg{\kod{\pat}}{\ag}{\kod{G}} = \{ \mu \in \semdg{\kod{\pat}_1}{\ag}{\kod{\gr}} \ | \ \mu \zadovoljava \kod{R} \}.$$

By induction hypothesis, for $\kod{\pat}_1$ there exists a graph pattern $\kod{\pat}_1'$ in the filter-normal form such that

$$\semdg{\kod{\pat}_1}{\ag}{\kod{G}} = \semdg{\kod{\pat}_1'}{\ag}{\kod{G}}.$$

Therefore, it holds

$$\semdg{\kod{\pat}}{\ag}{\kod{G}} = \{ \mu \in \semdg{\kod{\pat}_1'}{\ag}{\kod{\gr}} \ | \ \mu \zadovoljava \kod{R} \},$$

i.e. by Definition <ref>,
$$\semdg{\kod{\pat}}{\ag}{\kod{G}} = \semdg{\kod{\pat}_1' \kod{ filter } \kod{R}}{\ag}{\kod{G}}.$$

If $\kod{\pat}_1'$ is in the form (i), (ii) or (iii) , let $\kod{\pat}'$ denote $\kod{\pat}_1' \kod{ filter } \kod{R}$.
Then, it holds $\semdg{\kod{\pat}}{\ag}{\kod{G}} = \semdg{\kod{\pat}'}{\ag}{\kod{G}}$ and by Definition <ref>, $\kod{\pat}'$ is in the filter-normal form.

If $\kod{\pat}_1'$ is in the form (iv), i.e. $\kod{\pat}_1'' \kod{ filter R}_1$, let $\kod{\pat}'$ denote $\kod{\pat}_1'' \kod{ filter } \kod{R\&\&R}_1$.
By Definition <ref>, it holds

$$\semdg{\kod{\pat}_1'' \kod{ filter R}_1 \kod{ filter } \kod{R}}{\ag}{\kod{G}} =$$

$$\semdg{\kod{\pat}_1'' \kod{ filter } \kod{R\&\&R}_1}{\ag}{\kod{G}}.$$

Then, it holds $\semdg{\kod{\pat}}{\ag}{\kod{G}} = \semdg{\kod{\pat}'}{\ag}{\kod{G}}$ and by Definition <ref>, $\kod{\pat}'$ is in filter-normal form.

Note that it holds

$$\kod{var}(\kod{R\&\&R}_1) \subseteq \kod{var}(\kod{\pat}_1''),$$

i.e. this feature holds for the transformed graph pattern as well.

* $\kod{\pat}$ is $\kod{\{\pat}_1\kod{\}}$

By Definition <ref>, it holds

$$\semdg{\kod{\{\pat}_1\kod{\}}}{\ag}{\kod{G}} = \semdg{\kod{\pat}_1}{\ag}{\kod{G}}.$$

By induction hypothesis, for $\kod{\pat}_1$ there exists a graph pattern $\kod{\pat}_1'$ in filter-normal form such that

$$\semdg{\kod{\pat}_1}{\ag}{\kod{G}} = \semdg{\kod{\pat}_1'}{\ag}{\kod{G}}.$$

Therefore, by Definition <ref>,
$$\semdg{\kod{\pat}}{\ag}{\kod{G}} = \semdg{\kod{\pat}_1'}{\ag}{\kod{G}},$$

where $\kod{\pat}_1'$ is in filter-normal form.

* $\kod{\pat}$ is $\kod{\{Q$_\kod{sq}$\}}$

By induction hypothesis, for $\kod{qpat}_\kod{sq}$ there exists a graph pattern $\kod{qpat}_\kod{sq}'$ in filter-normal form such that

$$\semdg{\kod{qpat}_\kod{sq}}{\ag}{\kod{G}} = \semdg{\kod{qpat}_\kod{sq}'}{\ag}{\kod{G}}.$$

Let $\kod{Q}_\kod{sq}'$ be a query obtained from $\kod{Q}_\kod{sq}$ by switching the query pattern $\kod{qpat}_\kod{sq}$ with $\kod{qpat}_\kod{sq}'$.
Therefore, by Definition <ref>, it holds

$$\semd{\kod{Q}_\kod{sq}}{\ag} = \semd{\kod{Q}_\kod{sq}'}{\ag},$$

i.e. by Definition <ref>,

$$\semdg{\kod{qpat}}{\ag}{\kod{G}} = \semdg{\kod{\{Q$_\kod{sq}'$\}}}{\ag}{\kod{G}}.$$

By Definition <ref>, $\kod{\{Q$_\kod{sq}'$\}}$ is in filter-normal form.

An example of a graph pattern $\kod{\pat}$ not satisfying filter-normal form is given in Figure <ref> (left), while its equivalent pattern $\kod{\pat}'$ in filter-normal form is given in the same figure (right).

Graph pattern $\kod{\pat}$

?y a ?t
filter (?t = :SoloArtist) .
?y :hometown ?z .
?z :name ?w
filter (?w = "Los Angeles")

Graph pattern $\kod{\pat}'$

?y a ?t .
?y :hometown ?z .
?z :name ?w

filter (?t = :SoloArtist
?w = "Los Angeles")

Reducing the graph pattern $\kod{\pat}$ to its equivalent pattern $\kod{\pat}'$ in the filter-normal form

Let $\ag$ be an  dataset and  a graph within $\ag$.
For a graph pattern $\kod{\pat}$ that contains a subquery $\kod{\{Q$_\kod{sq}$\}}$, there exists a graph pattern $\kod{\pat}'$ such that it holds
$\semdg{\kod{\pat}}{\ag}{\kod{G}} = \semdg{\kod{\pat}'}{\ag}{\kod{G}}$, and $\kod{\pat}'$ has one of the following forms:

* $\kod{\{Q$_\kod{sq}'$\}}$,

* $\kod{\{Q$_\kod{sq}'$\}} \; \kod{filter R}$,

* $\kod{\pat}_1 \kod{.} \kod{\{Q$_\kod{sq}'$\}}$,

* $\kod{\pat}_1 \kod{.} \kod{\{Q$_\kod{sq}'$\}} \; \kod{ filter R}$

where $\kod{\pat}_1$ is in filter-normal form (i), (ii) or (iii) and $\kod{\{Q$_\kod{sq}'$\}}$ is in filter-normal.

A proof of this lemma is a direct consequence of Definition <ref>, Lemma <ref> and the associativity and commutativity of the SPARQL operator . [Pérez et al., 2006].

Some variables in a query can be renamed, while the evaluation of the transformed query remains the same, as stated in the following lemma.

Let $\dataq$ be an  dataset.
Let $\kod{Q}$ be a query, $\kod{qpat}$ and $\overline{\kod{dv}}$ its query pattern and its set of distinguished variables, respectively.
Let $\kod{qpat}'$ be a graph pattern obtained from $\kod{qpat}$ by renaming all the variables from $\kod{var}(\kod{qpat}) \setminus \overline{\kod{dv}}$, while introducing fresh new ones.
Let $\kod{Q}'$ be a query obtained from $\kod{Q}$ by changing its query pattern $\kod{qpat}$ with $\kod{qpat}'$.
Then it holds:

$\semd{\kod{Q}}{\dataq} = \semd{\kod{Q}'}{\dataq}$.

By Definition <ref>, it holds

$$\semd{\kod{Q}}{\dataq} = \PP_{\overline{\kod{dv}}}(\semdg{\kod{qpat}}{\ag}{\mathit{df}(\ag)}),$$

i.e. by Definition <ref>,

$$\semd{\kod{Q}}{\dataq} = \{\mu_{\overline{\kod{dv}}} \;|\; \mu \in \semdg{\kod{qpat}}{\ag}{\mathit{df}(\ag)}\}.$$

By the construction of $\kod{qpat}'$, it holds

$$\{\mu_{\overline{\kod{dv}}} \;|\; \mu \in \semdg{\kod{qpat}}{\ag}{\mathit{df}(\ag)}\} = $$

$$\{\mu'_{\overline{\kod{dv}}} \;|\; \mu' \in \semdg{\kod{qpat}'}{\ag}{\mathit{df}(\ag)}\},$$

as, by Definition <ref>, mappings from $\semdg{\kod{qpat}}{\ag}{\mathit{df}(\ag)}$ and from $\semdg{\kod{qpat}'}{\ag}{\mathit{df}(\ag)}$ match on variables from $\overline{\kod{dv}}$.

Therefore, it holds

$$\semd{\kod{Q}}{\dataq} = \{\mu'_{\overline{\kod{dv}}} \;|\; \mu' \in \semdg{\kod{qpat}'}{\ag}{\mathit{df}(\ag)}\}.$$

By Definition <ref> it holds

$$\semd{\kod{Q}}{\dataq} = \PP_{\overline{\kod{dv}}}(\semdg{\kod{qpat}'}{\ag}{\mathit{df}(\ag)}).$$

By Definition <ref> and the construction of the query $\kod{Q}'$, it holds

$$\semd{\kod{Q}}{\dataq} = \semd{\kod{Q}'}{\dataq}.$$

Any query $\kod{Q}$ containing a subquery $\kod{Q}_\kod{sq}$ can be reduced to an equivalent query $\kod{Q}'$ that does not contain this subquery. The construction of such query $\kod{Q}'$ is given in the proof of the following lemma.

Let $\dataq$ be an  dataset.
Let $\kod{Q}$ be a query such that its query pattern contains a subquery $\kod{\{Q$_\kod{sq}$\}}$.
Then, there exists a graph pattern $\kod{\pat}_\kod{sq}$ such that it is not a subquery and if it is used within
Q instead of $\kod{\{Q$_\kod{sq}$\}}$, forming a new query $\kod{Q}'$, it holds
$\semd{\kod{Q}}{\dataq} = \semd{\kod{Q}'}{\dataq}$.

According to Lemma <ref>, there exists a query pattern that is in a form defined by the lemma, and that is equivalent to the original query pattern of the query Q. Therefore, we can assume that the query Q already contains a query pattern in such form.

We prove the case when the query pattern $\kod{qpat}$ of the query Q is equal to $\kod{\pat}_1 \kod{.} \kod{\{Q$_\kod{sq}$\}} \; \kod{ filter R}$. All other cases are simpler and can be proved in analogous way.

In the subquery $\kod{Q}_\kod{sq}$ of the query pattern $\kod{qpat}$, we can rename all the variables that are not distinguished ($\kod{var}(\kod{qpat}_\kod{sq}) \setminus \overline{\kod{dv}_\kod{sq}}$), by introducing fresh new variables that do not appear in the outer query Q (anywhere else except in the subquery $\kod{Q}_\kod{sq}$).
This step is possible as a set of variables $\kod{V}$ is countable. 	After this renaming, by Lemma <ref>, it holds that the evaluation of the subquery $\kod{Q}'_\kod{sq}$ that contains renamed variables, has not been changed compared to the subquery $\kod{Q}_\kod{sq}$ . Let $\kod{qpat}_\kod{sq}'$ denote the query pattern of $\kod{Q}'_\kod{sq}$.

The set of variables from the outer query Q includes distinguished variables $\overline{\kod{dv}}$ and
variables of the graph pattern $\kod{\pat}_1$, i.e. $\kod{var}(\kod{\pat}_1)$.
Therefore, it holds:

$$\kod{var}(\kod{qpat}'_\kod{sq}) \cap (\kod{var}(\kod{\pat}_1) \cup \overline{\kod{dv}}) \subseteq \overline{\kod{dv}_\kod{sq}}$$

\begin{align}
\kod{var}(\kod{qpat}'_\kod{sq}) \cap \kod{var}(\kod{\pat}_1) \subseteq \overline{\kod{dv}_\kod{sq}} \label{eq:subquery1}\\
\text{and } \kod{var}(\kod{qpat}'_\kod{sq}) \cap \overline{\kod{dv}} \subseteq \overline{\kod{dv}_\kod{sq}} \label{eq:subquery2}
\end{align}

Note that it also holds
$\kod{var}(\kod{R}) \subseteq \kod{var}(\kod{\pat}_1) \cup \kod{var}(\kod{\{Q}_\kod{sq}\kod{\}}).$
i.e. by Definition <ref>,

\begin{align}
\kod{var}(\kod{R}) \subseteq \kod{var}(\kod{\pat}_1) \cup \overline{\kod{dv}_\kod{sq}}.\label{eq:subquery0}
\end{align}

Let $\kod{qpat}'$ be a query pattern such that in query pattern $\kod{qpat}$, the subquery $\kod{Q}'_\kod{sq}$ is replaced with $\{\kod{qpat}'_\kod{sq}\}$.  Let $\kod{Q}'$ be a query such that in the query $\kod{Q}$, its query pattern qpat is replaced with $\kod{qpat}'$.
Let us prove that $\semd{\kod{Q}}{\dataq} = \semd{\kod{Q}'}{\dataq}$.

Let $\mu$ be a mapping such that $\mu \in \semd{\kod{Q}}{\dataq}$.
By Definition <ref>, there exists a mapping $\mu^{\rm i}$, such that

$$\mu = \mu^{\rm i}_{\overline{\kod{dv}}} \text{~~~and~~~} \mu^{\rm i} \in \semdg{\kod{qpat}}{\ag}{\mathit{df}(\ag)}.$$

Therefore, by Definitions <ref> and <ref>, it holds

$$\mu^{\rm i} \in \semdg{\kod{\pat}_1}{\ag}{\mathit{df}(\ag)} \bowtie \semd{\kod{Q}'_\kod{sq}}{\ag} \text{~~~and~~~}  \mu^{\rm i} \zadovoljava \kod{R}.$$

By Definition <ref>, there exist compatible mappings $\mu_1$ and $\mu^{\rm ii}$ such that

$$\mu^{\rm i} = \mu_1 \cup \mu^{\rm ii} \text{~~~and~~~} \mu_1 \in \semdg{\kod{\pat}_1}{\ag}{\mathit{df}(\ag)} \text{~~~and~~~} \mu^{\rm ii} \in \semd{\kod{Q}'_\kod{sq}}{\ag}.$$

By Definition <ref>, there exists a mapping $\mu^{\rm iii}$ such that

$$\mu^{\rm ii} = \mu^{\rm iii}_{\overline{\kod{dv}_\kod{sq}}} \text{~~~and~~~} \mu^{\rm iii} \in \semdg{\kod{qpat}'_\kod{sq}}{\ag}{\mathit{df}(\ag)}.$$

By Definition <ref>, from $\mu_1 \comp \mu^{\rm ii}$, it holds $\mu_1 \comp \mu^{\rm iii}$, as there is no variable in $\kod{var}(\kod{qpat}'_\kod{sq})$ apart from $\overline{\kod{dv}_\kod{sq}}$ that can appear in $\kod{var}(\kod{\pat}_1)$ because of (<ref>).
Let $\mu^{\rm iv}$ denote mapping $\mu_1 \cup \mu^{\rm iii}$.
By Definition <ref>, it holds

$$\mu^{\rm iv} \in \semdg{\kod{\pat}_1}{\ag}{\mathit{df}(\ag)} \bowtie \semdg{\kod{qpat}'_\kod{sq}}{\ag}{\mathit{df}(\ag)}.$$

By Definition <ref>, as $\mu^{\rm iv} = \mu_1 \cup \mu^{\rm iii}$, $\mu^{\rm i} = \mu_1 \cup \mu^{\rm ii}$ and $\mu^{\rm iii} \succeq \mu^{\rm ii}$, it holds $\mu^{\rm iv} \succeq \mu^{\rm i}$.
Then, for $\mu^{\rm iv}$ as an extenstion of $\mu^{\rm i}$, from $\mu^{\rm i} \zadovoljava \kod{R}$, it holds:

$$\mu^{\rm iv} \zadovoljava \kod{R}.$$

Therefore, by Definition <ref>, it holds

$$\mu^{\rm iv} \in \semdg{\kod{qpat}'}{\ag}{\mathit{df}(\ag)},$$

i.e. by Definition <ref>,

$$\mu^{\rm iv}_{\overline{\kod{dv}}} \in \semd{\kod{Q}'}{\dataq}.$$

Let us prove that $\mu^{\rm iv}_{\overline{\kod{dv}}} = \mu$.
By Definition <ref>, from $\mu^{\rm iv} \succeq \mu^{\rm i}$, it holds $\mu^{\rm iv}_{\overline{\kod{dv}}} \succeq \mu^{\rm i}_{\overline{\kod{dv}}}$, i.e. $\mu^{\rm iv}_{\overline{\kod{dv}}} \succeq \mu$.
Also, it holds:

\begin{align*}
&\hspace*{18mm} dom(\mu) \hspace*{-20mm} & = \;\\
&\text{(by Def \ref{def:extension_restriction})} &=\;& dom(\mu^{\rm i}) \cap \overline{\kod{dv}} \\
& \text{(as } \mu^{\rm i} = \mu_1 \cup \mu^{\rm ii} \text{)}&=\;& (dom(\mu_1) \cup dom(\mu^{\rm ii})) \cap \overline{\kod{dv}}\\
&\text{(by dist.of } \cap &=\;&  (dom(\mu_1) \cap \overline{\kod{dv}} ) \cup\\
&\text{ over} \cup \text{)}&& (dom(\mu^{\rm ii}) \cap \overline{\kod{dv}})\\
& \text{(by Def \ref{def:extension_restriction})} &=\;& (dom(\mu_1) \cap \overline{\kod{dv}} ) \cup\\
&&& (dom(\mu^{\rm iii}) \cap \overline{\kod{dv}_\kod{sq}} \cap \overline{\kod{dv}})\\
& \text{(by Lemma \ref{thm:pattern_domain})} &=\;& (dom(\mu_1) \cap \overline{\kod{dv}} ) \cup\\
&&& (\kod{var}(\kod{qpat}'_\kod{sq}) \cap \overline{\kod{dv}_\kod{sq}} \cap \overline{\kod{dv}})\\
& \text{(from (\ref{eq:subquery2}) )} &=\;& (dom(\mu_1) \cap \overline{\kod{dv}} ) \cup\\
&&& (\kod{var}(\kod{qpat}'_\kod{sq}) \cap \overline{\kod{dv}})\\
& \text{(by Lemma \ref{thm:pattern_domain})} &=\;& (dom(\mu_1) \cap \overline{\kod{dv}} ) \cup\\
&&& (dom(\mu^{\rm iii}) \cap \overline{\kod{dv}})\\
&\text{(by dist.of} \cap \text{over} \cup \text{)} \hspace*{-4mm} &=\;& (dom(\mu_1) \cup dom(\mu^{\rm iii})) \cap \overline{\kod{dv}}\\
& \text{(as } \mu^{\rm iv} = \mu_1 \cup \mu^{\rm iii} \text{)}&=\;& dom(\mu^{\rm iv}) \cap \overline{\kod{dv}}\\
& \text{(by Def \ref{def:extension_restriction})}&=\;& dom(\mu^{\rm iv}_{\overline{\kod{dv}}})
\end{align*}

Therefore, it holds $\mu^{\rm iv}_{\overline{\kod{dv}}} = \mu$, and

$$\mu \in \semd{\kod{Q}'}{\dataq}.$$

Let $\mu$ be a mapping such that $\mu \in \semd{\kod{Q}'}{\dataq}$.
By Definition <ref>, there exists a mapping $\mu^{\rm i}$, such that

$$\mu = \mu^{\rm i}_{\overline{\kod{dv}}} \text{~~~and~~~} \mu^{\rm i} \in \semdg{\kod{qpat}'}{\ag}{\mathit{df}(\ag)}.$$

Therefore, by Definition <ref>, it holds

$$\mu^{\rm i} \in \semdg{\kod{\pat}_1}{\ag}{\mathit{df}(\ag)} \bowtie \semdg{\kod{qpat}'_\kod{sq}}{\ag}{\mathit{df}(\ag)} \text{~~~and~~~} \mu^{\rm i} \zadovoljava \kod{R}.$$

By Definition <ref>, there exist compatible mappings $\mu_1$ and $\mu^{\rm ii}$ such that

$$\mu^{\rm i} = \mu_1 \cup \mu^{\rm ii} \text{~~and~~} \mu_1 \in \semdg{\kod{\pat}_1}{\ag}{\mathit{df}(\ag)} \text{~~and~~} \mu^{\rm ii} \in \semdg{\kod{qpat}'_\kod{sq}}{\ag}{\mathit{df}(\ag)}.$$

By Definition <ref>, it holds

$$\mu^{\rm ii}_{\overline{\kod{dv}_\kod{sq}}} \in \semd{\kod{Q}'_\kod{sq}}{\ag}.$$

By Definitions <ref> and <ref>, as $\mu_1 \comp \mu^{\rm ii}$, it holds $\mu_1 \comp \mu^{\rm ii}_{\overline{\kod{dv}_\kod{sq}}}$.
Let $\mu^{\rm iii}$ denote mapping $\mu_1 \cup \mu^{\rm ii}_{\overline{\kod{dv}_\kod{sq}}}$.
By Definition <ref>, it holds

$$\mu^{\rm iii} \in \semdg{\kod{\pat}_1}{\ag}{\mathit{df}(\ag)} \bowtie \semd{\kod{Q}'_\kod{sq}}{\ag}.$$

By Definition <ref>, it holds $\mu_1 \cup \mu^{\rm ii} \succeq \mu_1 \cup \mu^{\rm ii}_{\overline{\kod{dv}_\kod{sq}}}$, i.e. $\mu^{\rm i} \succeq \mu^{\rm iii}$.
Note that $dom(\mu^{\rm i}) = dom(\mu_1) \cup dom(\mu^{\rm ii})$ and $dom(\mu^{\rm iii}) = dom(\mu_1) \cup (dom(\mu^{\rm ii}) \cap \overline{\kod{dv}_\kod{sq}})$, i.e. by Lemma <ref>,

$$dom(\mu^{\rm i}) = \kod{var}(\kod{\pat}_1) \cup \kod{var}(\kod{qpat}'_\kod{sq}),$$

$$dom(\mu^{\rm iii}) = \kod{var}(\kod{\pat}_1) \cup (\kod{var}(\kod{qpat}'_\kod{sq}) \cap \overline{\kod{dv}_\kod{sq}}).$$

$$dom(\mu^{\rm i}) \setminus dom(\mu^{\rm iii}) = \kod{var}(\kod{qpat}'_\kod{sq}) \setminus \overline{\kod{dv}_\kod{sq}}.$$

All of the variables from $dom(\mu^{\rm i}) \setminus dom(\mu^{\rm iii})$ are renamed, and they cannot belong to $\kod{var}(\kod{R})$, because of (<ref>).
Therefore, from $\mu^{\rm i} \zadovoljava \kod{R}$ it holds

$$\mu^{\rm iii} \zadovoljava \kod{R}.$$

Then, by Definition <ref>, it holds

$$\mu^{\rm iii}_{\overline{\kod{dv}}} \in \semd{\kod{Q}}{\dataq}.$$

Let us prove that $\mu^{\rm iii}_{\overline{\kod{dv}}} = \mu$.
By Definition <ref>, from $\mu^{\rm iii} \preceq \mu^{\rm i}$, it holds $\mu^{\rm iii}_{\overline{\kod{dv}}} \preceq \mu^{\rm i}_{\overline{\kod{dv}}}$, i.e. $\mu^{\rm iii}_{\overline{\kod{dv}}} \preceq \mu$.
Also, it holds:

\begin{align*}
&\hspace*{20mm} dom(\mu) \hspace*{-20mm} & = \;\\
&\text{(by Def \ref{def:extension_restriction})} &=\;& dom(\mu^{\rm i}) \cap \overline{\kod{dv}} \\
& \text{(as } \mu^{\rm i} = \mu_1 \cup \mu^{\rm ii} \text{)}&=\;& (dom(\mu_1) \cup dom(\mu^{\rm ii})) \cap \overline{\kod{dv}}\\
&\text{(by dist.of } \cap &=\;&  (dom(\mu_1) \cap \overline{\kod{dv}} ) \cup\\
&\text{ over } \cup \text{)}&& (dom(\mu^{\rm ii}) \cap \overline{\kod{dv}})\\
&\text{(by Lemma \ref{thm:pattern_domain})} &=\;& (dom(\mu_1) \cap \overline{\kod{dv}} ) \cup\\
&&& (\kod{var}(\kod{qpat}'_\kod{sq}) \cap \overline{\kod{dv}})\\
&\text{(from (\ref{eq:subquery2}) )} &=\;& (dom(\mu_1) \cap \overline{\kod{dv}} ) \cup\\
&&& (\kod{var}(\kod{qpat}'_\kod{sq}) \cap \overline{\kod{dv}_\kod{sq}} \cap \overline{\kod{dv}})\\
&\text{(by Lemma \ref{thm:pattern_domain})} &=\;& (dom(\mu_1) \cap \overline{\kod{dv}} ) \cup\\
&&& (dom(\mu^{\rm ii}) \cap \overline{\kod{dv}_\kod{sq}} \cap \overline{\kod{dv}})\\
&\text{(by Def \ref{defn:query_evaluation})} &=\;& (dom(\mu_1) \cap \overline{\kod{dv}} ) \cup\\
&&& (dom(\mu^{\rm ii}_{\overline{\kod{dv}_\kod{sq}}}) \cap \overline{\kod{dv}})\\
&\text{(by dist.of} \cap \text{over} \cup \text{)} \hspace*{-4mm} &=\;& (dom(\mu_1) \cup dom(\mu^{\rm ii}_{\overline{\kod{dv}_\kod{sq}}})) \cap \overline{\kod{dv}}\\
& \text{(as } \mu^{\rm iii} = \mu_1 \cup \mu^{\rm ii}_{\overline{\kod{dv}_\kod{sq}}} \text{)}&=\;& dom(\mu^{\rm iii}) \cap \overline{\kod{dv}}\\
& \text{(by Def \ref{def:extension_restriction})}&=\;& dom(\mu^{\rm iii}_{\overline{\kod{dv}}})
\end{align*}

Therefore, it holds $\mu^{\rm iii}_{\overline{\kod{dv}}} = \mu$, and

$$\mu \in \semd{\kod{Q}}{\dataq}.$$

If a query Q contains more than one subquery, then the elimination of subqueries should be applied starting from the inner most subquery.
This way, the containment problem concerning queries with subqueries is reduced to the containment problem of queries that do not contain subqueries.

For the containment problem, we assume that there is no subqueries in the query $\kod{Q}_2$ or in cases where they are present in $\kod{Q}_2$, all their variables are projected up to $\kod{Q}_2$.
Otherwise, the construction of an equivalent query $\kod{Q}_2'$ from the proof of Lemma <ref> would make projections present within $\kod{Q}_2'$, leading to an undecidable problem.
When considering the subsumption relation, this restriction is not necessary, as the query subsumption problem is decidable in cases when a super-query contains projections [Pichler and Skritek, 2014].

§ CONCLUSIONS AND FURTHER WORK

In this paper we proved correctness of the approach described in [Spasić and Vujošević Janičić, 2022] and implemented by a tool  [Spasić and Vujošević Janičić, 2022]. Correctness, i.e. soundness and completeness, are proved for modeling conjunctive queries for both  containment and subsumption relation. Soundness and completeness proofs are extended to cover non-conjunctive queries containing operator union, operator optional and subqueries in cases when well designed patterns and filter-normal form are considered.

There are several possible directions for further work: extending the language coverage while keeping the soundness and completeness of the approach if possible, considering containment and subsumption in the context of  schema, considering containment and subsumption when a wider set of axioms is included (e.g. $\mathcal{SHI}$ axioms [Horrocks et al., 1999, Chekol et al., 2012] or code refactoring context [Spasić and Vujošević Janičić, 2021]), applying a similar approach for different graph query languages (e.g. XPath [Schwentick, 2004, Miklau and Suciu, 2004], GQL [Hartig and Pérez, 2018]), and making the presented proofs formal within a proof assistant [Nipkow et al., 2002, Bertot and Castran, 2010].

[Angles and Gutierrez, 2008]
authorAngles, R., authorGutierrez, C.,
titleThe Expressive Power of SPARQL, in:
booktitleProceedings of the 7th International Conference on The
Semantic Web, publisherSpringer. pp. pages114–129.

[Angles and Gutiérrez, 2011]
authorAngles, R., authorGutiérrez, C.,
titleSubqueries in SPARQL, in:
booktitleProceedings of the 5th Alberto Mendelzon International
Workshop on Foundations of Data Management, Santiago, Chile, May, 2011,
publisherCEUR-WS.org. pp. pages1–12.

[Angles and Gutiérrez, 2016]
authorAngles, R., authorGutiérrez, C.,
titleNegation in SPARQL, in:
booktitleProceedings of the 10th Alberto Mendelzon International
Workshop on Foundations of Data Management, Panama City, Panama, 2016,
publisherCEUR-WS.org. pp. pages1–10.

[Angles and Gutierrez, 2016]
authorAngles, R., authorGutierrez, C.,
titleThe Multiset Semantics of SPARQL Patterns, in:
booktitleThe Semantic Web – ISWC 2016,
publisherSpringer. pp. pages20–36.

[Arenas and Perez, 2011]
authorArenas, M., authorPerez, J.,
titleQuerying Semantic Web Data with SPARQL, in:
booktitleProceedings of the 13th ACM SIGMOD-SIGACT-SIGART
Symposium on Principles of Database Systems, pp. pages305–316.

[Auer et al., 2011]
authorAuer, S., authorLehmann, J.,
authorNgomo, A.C.N., year2011.
titleIntroduction to Linked Data and Its Lifecycle on the
Web, in: booktitleReasoning Web. Semantic Technologies for the
Web of Data. publisherSpringer, pp. pages1–75.

[Barrett et al., 2009]
authorBarrett, C., authorSebastiani, R.,
authorSeshia, S.A., authorTinelli, C.,
titleSatisfiability Modulo Theories, in:
booktitleHandbook of Satisfiability, publisherIOS
Press. pp. pages825–885.

[Bertot and Castran, 2010]
authorBertot, Y., authorCastran, P.,
titleInteractive Theorem Proving and Program Development:
Coq'Art The Calculus of Inductive Constructions.

[Calvanese et al., 2000]
authorCalvanese, D., authorGiacomo, G.D.,
authorLenzerini, M., authorVardi, M.Y.,
titleContainment of Conjunctive Regular Path Queries With
Inverse, in: booktitleProceedings of the 7th International
Conference on Principles of Knowledge Representation and Reasoning,
publisherMorgan Kaufmann. pp. pages176–185.

[Chandra and Merlin, 1977]
authorChandra, A.K., authorMerlin, P.M.,
titleOptimal Implementation of Conjunctive Queries in
Relational Data Bases, in: booktitleSTOC,
publisherACM. pp. pages77–90.

[Chang and Keisler, 1976]
authorChang, C.C., authorKeisler, H.J.,
titleModel Theory.
journalJournal of Symbolic Logic volume41,

[Chaudhuri and Vardi, 1993]
authorChaudhuri, S., authorVardi, M.Y.,
titleOptimization of Real Conjunctive Queries, in:
booktitlePODS, publisherACM. pp.

[Chekol et al., 2018]
authorChekol, M., authorEuzenat, J.,
authorGenevès, P., authorLayaïda, N.,
titleSPARQL Query Containment under Schema.
journalJournal on Data Semantics volume7,

[Chekol et al., 2012]
authorChekol, M.W., authorEuzenat, J.,
authorGenevès, P., authorLayaïda, N.,
titleSPARQL Query Containment under RDFS Entailment
Regime, in: booktitleProceedings of the 6th International Joint
Conference on Automated Reasoning, publisherSpringer. p.

[Chekol et al., 2012]
authorChekol, M.W., authorEuzenat, J.,
authorGenevès, P., authorLayaïda, N.,
titleSPARQL Query Containment Under SHI Axioms, in:
booktitleProceedings of the 26th AAAI Conference on Artificial
Intelligence, publisherAAAI Press. pp. pages10–16.

[Chekol et al., 2013]
authorChekol, M.W., authorEuzenat, J.,
authorGenevès, P., authorLayaïda, N.,
titleEvaluating and Benchmarking SPARQL Query Containment
Solvers, in: booktitleThe Semantic Web – ISWC 2013,
publisherSpringer. pp. pages408–423.

[Dijkstra, 1972]
authorDijkstra, E.W., year1972.
titleChapter I: Notes on Structured Programming.
publisherAcademic Press Ltd., addressGBR.
chapter chapter1.
pp. pages1–82.

[Dürst and Suignard, 2005]
authorDürst, M.J., authorSuignard, M.,
titleInternationalized Resource Identifiers (IRIs).
journalRFC volume3987,

[Fernández et al., 1999]
authorFernández, M., authorFlorescu, D.,
authorLevy, A., authorSuciu, D.,
titleVerifying Integrity Constraints on Web Sites, in:
booktitleProceedings of the 16th International Joint Conference on
Artifical Intelligence, pp. pages614–619.

[Friedman et al., 1999]
authorFriedman, M., authorLevy, A.,
authorMillstein, T., year1999.
titleNavigational Plans for Data Integration, in:
booktitleProceedings of the 1999 International Conference on
Intelligent Information Integration - Volume 23,
publisherCEUR-WS.org, addressAachen, DEU. pp.

[Genevès et al., 2015]
authorGenevès, P., authorLayaïda, N.,
authorSchmitt, A., authorGesbert, N.,
titleEfficiently Deciding $\mu$-Calculus with Converse
over Finite Trees.
journalACM Trans. Comput. Logic volume16.

[22]
authorGenevès, P., authorLayaïda, N.,
authorSchmitt, A., authorGesbert, N.,
authorKnyttl, V., .
titleThe Tree Reasoning Solver.

[Gupta et al., 1994]
authorGupta, A., authorSagiv, Y.,
authorUllman, J.D., authorWidom, J.,
titleConstraint Checking with Partial Information, in:
booktitleProceedings of the 13th ACM SIGACT-SIGMOD-SIGART
Symposium on Principles of Database Systems, publisherACM. pp.

[Gutierrez et al., 2004]
authorGutierrez, C., authorHurtado, C.,
authorMendelzon, A.O., year2004.
titleFoundations of Semantic Web Databases, in:
booktitleProceedings of the 23rd ACM SIGMOD-SIGACT-SIGART
Symposium on Principles of Database Systems, publisherACM. pp.

[Hartig and Pérez, 2018]
authorHartig, O., authorPérez, J.,
titleSemantics and complexity of graphql, in:
booktitleProceedings of the 2018 World Wide Web Conference,
publisherInternational World Wide Web Conferences Steering
Committee, addressRepublic and Canton of Geneva, CHE. p.

[Hitzler et al., 2009]
authorHitzler, P., authorKrotzsch, M.,
authorRudolph, S., year2009.
titleFoundations of Semantic Web Technologies.
publisherChapman and Hall/CRC.

[Hogan, 2020]
authorHogan, A., year2020.
titleThe Semantic Web: Two decades on.
journalSemantic Web volume11,

[Horrocks et al., 1999]
authorHorrocks, I., authorSattler, U.,
authorTobies, S., year1999.
titlePractical reasoning for expressive description
logics, in: editorGanzinger, H., editorMcAllester,
D., editorVoronkov, A. (Eds.), booktitleLogic for
Programming and Automated Reasoning, publisherSpringer Berlin
Heidelberg, addressBerlin, Heidelberg. pp.

[Kaminski et al., 2016]
authorKaminski, M., authorKostylev, E.V.,
authorCuenca Grau, B., year2016.
titleSemantics and Expressive Power of Subqueries and
Aggregates in SPARQL 1.1, in: booktitleProceedings of the 25th
International Conference on World Wide Web,
publisherInternational World Wide Web Conferences Steering
Committee, addressRepublic and Canton of Geneva, CHE. p.

[Kashyap et al., 2008]
authorKashyap, V., authorBussler, C.,
authorMoran, M., year2008.
titleThe Semantic Web.

[Klyne et al., 2004]
authorKlyne, G., authorCarroll, J.,
authorMcBride, B., year2004.
titleResource Description Framework (RDF): Concepts and
Abstract Syntax.

[Kozen, 1982]
authorKozen, D., year1982.
titleResults on the Propositional $\mu$-Calculus, in:
booktitleProceedings of the 9th Colloquium on Automata, Languages
and Programming, publisherSpringer. pp.

[Lassila and Swick, 1999]
authorLassila, O., authorSwick, R.R.,
titleResource Description Framework (RDF): Model and
Syntax Specification.

[Leroy, 2009]
authorLeroy, X., year2009.
titleFormal verification of a realistic compiler.
journalCommun. ACM volume52,

[Letelier et al., 2013]
authorLetelier, A., authorPérez, J.,
authorPichler, R., authorSkritek, S.,
titleStatic Analysis and Optimization of Semantic Web
journalACM Trans. Database Syst. volume38,

[Levy et al., 1996]
authorLevy, A.Y., authorRajaraman, A.,
authorOrdille, J.J., year1996.
titleQuery-Answering Algorithms for Information Agents,
in: booktitleProceedings of the 13th National Conference on
Artificial Intelligence - Volume 1, publisherAAAI Press. pp.

[Levy and Rousset, 1998]
authorLevy, A.Y., authorRousset, M.C.,
titleCombining Horn rules and description logics in
journalArtificial Intelligence volume104,
pages165 – 209.

[Marić, 2010]
authorMarić, F., year2010.
titleFormal verification of a modern sat solver by shallow
embedding into isabelle/hol.
journalTheoretical Computer Science
volume411, pages4333–4356.

[Marker, 2002]
authorMarker, D., year2002.
titleModel Theory : An Introduction.
Graduate Texts in Mathematics, publisherSpringer.

[40]
authorMcCrae, J.P., .
titleThe Linked Open Data Cloud.
<https://lod-cloud.net/>. noteInsight
Centre for Data Analytics, retrieved February 20th, 2022.

[Miklau and Suciu, 2004]
authorMiklau, G., authorSuciu, D.,
titleContainment and Equivalence for a Fragment of
journalJ. ACM volume51,

[Nipkow et al., 2002]
authorNipkow, T., authorPaulson, L.C.,
authorWenzel, M., year2002.
titleIsabelle/HOL. A proof assistant for higher-order
logic. volume volume2283 of seriesLect. Notes
Comput. Sci.
publisherBerlin: Springer.

[Pérez et al., 2006]
authorPérez, J., authorArenas, M.,
authorGutierrez, C., year2006.
titleSemantics and Complexity of SPARQL, in:
editorCruz, I., editorDecker, S.,
editorAllemang, D., editorPreist, C.,
editorSchwabe, D., editorMika, P.,
editorUschold, M., editorAroyo, L.M. (Eds.),
booktitleThe Semantic Web - ISWC 2006,
publisherSpringer. pp. pages30–43.

[Pérez et al., 2009]
authorPérez, J., authorArenas, M.,
authorGutierrez, C., year2009.
titleSemantics and Complexity of SPARQL.
journalACM Trans. Database Syst. volume34,

[Pichler and Skritek, 2014]
authorPichler, R., authorSkritek, S.,
titleContainment and Equivalence of Well-Designed
SPARQL, in: booktitleProceedings of the 33rd ACM
SIGMOD-SIGACT-SIGART Symposium on Principles of Database Systems,
publisherACM. pp. pages39–50.

[Prud'hommeaux and Seaborne, 2008]
authorPrud'hommeaux, E., authorSeaborne, A.,
titleSPARQL Query Language for RDF, W3C Recommendation.

[Prud'hommeaux and Seaborne, 2013]
authorPrud'hommeaux, E., authorSeaborne, A.,
titleSPARQL 1.1 Query Language.

[Salas and Hogan, 2018]
authorSalas, J., authorHogan, A.,
titleCanonicalisation of Monotone SPARQL Queries, in:
booktitleThe Semantic Web – ISWC 2018,
publisherSpringer. pp. pages600–616.

[Salas and Hogan, 2018]
authorSalas, J., authorHogan, A.,
titleQCan: Normalising Congruent SPARQL Queries, in:
booktitleProceedings of the 17th International Semantic Web
Conference (ISWC), 2018 - Posters & Demos,
publisherCEUR-WS.org. pp. pages1–4.

[Saleem et al., 2017]
authorSaleem, M., authorStadler, C.,
authorMehmood, Q., authorLehmann, J.,
authorNgomo, A.C.N., year2017.
titleSQCFramework: SPARQL Query Containment Benchmark
Generation Framework, in: booktitleProceedings of the Knowledge
Capture Conference, publisherACM. pp.

[Schmidt et al., 2010]
authorSchmidt, M., authorMeier, M.,
authorLausen, G., year2010.
titleFoundations of SPARQL Query Optimization, in:
booktitleProceedings of the 13th International Conference on
Database Theory, publisherACM. pp. pages4–33.

[Schwentick, 2004]
authorSchwentick, T., year2004.
titleXPath Query Containment.
journalSIGMOD Rec. volume33,

[Spasić and Vujošević Janičić, 2021]
authorSpasić, M.,
authorVujošević Janičić, M.,
titleVerification Supported Refactoring of Embedded
journalSoftware Quality Journal volume29,

[Spasić and Vujošević Janičić, 2022]
authorSpasić, M.,
authorVujošević Janičić, M.,
title Web page.

[Spasić and Marić, 2012]
authorSpasić, M., authorMarić, F.,
titleFormalization of Incremental Simplex Algorithm
by Stepwise Refinement, in: editorGiannakopoulou, D.,
editorMéry, D. (Eds.), booktitleFM 2012:
Formal Methods - 18th International Symposium, Paris, France, August 27-31,
2012. Proceedings, publisherSpringer. pp.

[Spasić and Vujošević Janičić, 2022]
authorSpasić, M., authorVujošević Janičić, M.,
titleSolving the sparql query containment problem with
journalsubmitted to Journal of Web Semantics .

[Stadler et al., 2018]
authorStadler, C., authorSaleem, M.,
authorNgomo, A.C.N., authorLehmann, J.,
titleEfficiently Pinpointing SPARQL Query Containments,
in: editorMikkonen, T., editorKlamma, R.,
editorHernández, J. (Eds.), booktitleWeb
Engineering, publisherSpringer. pp. pages210–224.

[Tanabe et al., 2005]
authorTanabe, Y., authorTakahashi, K.,
authorYamamoto, M., authorTozawa, A.,
authorHagiya, M., year2005.
titleA Decision Procedure for the Alternation-Free
Two-Way Modal $\mu$-Calculus, in: editorBeckert, B. (Ed.),
booktitleAutomated Reasoning with Analytic Tableaux and Related
Methods, publisherSpringer. pp. pages277–291.