In our pursuit of generic criteria for decidable ontology-based querying, we introduce finite-cliquewidth sets ($\fcs$) of existential rules, a model-theoretically defined class of rule sets, inspired by the cliquewidth measure from graph theory. By a generic argument, we show that $\bcs$ ensures decidability of entailment for a sizable class of queries (dubbed DaMSOQs) subsuming conjunctive queries (CQs). The $\fcs$ class properly generalizes the class of finite-expansion sets ($\fes$), and for signatures of arity ${\leq}2$, the class of bounded-treewidth sets ($\bts$). For higher arities, $\bts$ is only indirectly subsumed by $\fcs$ by means of reification.

Despite the generality of $\fcs$, we provide a rule set with decidable CQ entailment (by virtue of first-order-rewritability) that falls outside $\fcs$, thus demonstrating the incomparability of $\fcs$ and the class of finite-unification sets ($\fus$).
In spite of this, we show that if we restrict ourselves to single-headed rule sets over signatures of arity ${\leq}2$, then $\fcs$ subsumes $\fus$.

[1]
S. Abiteboul, R. Hull, and V. Vianu.
Foundations of Databases.
Addison-Wesley, 1995.

[2]
J.-F. Baget, M. Bienvenu, M.-L. Mugnier, and S. Rocher.
Combining existential rules and transitivity: Next steps.
In Q. Yang and M. J. Wooldridge, editors, Proceedings of the
24th International Joint Conference on Artificial Intelligence (IJCAI'15),
pages 2720–2726. AAAI Press, 2015.

[3]
J.-F. Baget, M. Leclère, M.-L. Mugnier, and E. Salvat.
On rules with existential variables: Walking the decidability line.
Artificial Intelligence, 175(9):1620–1654, 2011.

[4]
C. Beeri and M. Y. Vardi.
A proof procedure for data dependencies.
Journal of the ACM, 31(4):718–741, 1984.

[5]
P. Bourhis, M. Krötzsch, and S. Rudolph.
How to best nest regular path queries.
In M. Bienvenu, M. Ortiz, R. Rosati, and M. Simkus, editors, Informal Proceedings of the 27th International Workshop on Description
Logics, Vienna, Austria, July 17-20, 2014, volume 1193 of CEUR
Workshop Proceedings, pages 404–415. CEUR-WS.org, 2014.

[6]
P. Bourhis, M. Morak, and A. Pieris.
Making cross products and guarded ontology languages compatible.
In C. Sierra, editor, Proceedings of the 26th International
Joint Conference on Artificial Intelligence (IJCAI'17), pages 880–886.
ijcai.org, 2017.

[7]
A. Calì, G. Gottlob, and M. Kifer.
Taming the infinite chase: Query answering under expressive
relational constraints.
Journal of Artificial Intelligence Research, 48:115–174, 2013.

[8]
A. Calì, G. Gottlob, and A. Pieris.
Towards more expressive ontology languages: The query answering
Artificial Intelligence, 193:87–128, 2012.

[9]
A. K. Chandra, H. R. Lewis, and J. A. Makowsky.
Embedded implicational dependencies and their inference problem.
In Proceedings of the 13th Annual ACM Symposium on Theory of
Computing (STOC'81), pages 342–354. ACM, 1981.

[10]
S. S. Cosmadakis, H. Gaifman, P. C. Kanellakis, and M. Y. Vardi.
Decidable optimization problems for database logic programs
(preliminary report).
In J. Simon, editor, Proceedings of the 20th Annual ACM
Symposium on Theory of Computing (STOC'88), pages 477–490. ACM, 1988.

[11]
B. Courcelle.
The monadic second-order logic of graphs. I. Recognizable sets of
finite graphs.
Information and Computation, 85(1):12–75, 1990.

[12]
B. Courcelle.
Clique-width of countable graphs: A compactness property.
Discrete Mathematics, 276(1-3):127–148, 2004.

[13]
B. Courcelle and J. Engelfriet.
Graph Structure and Monadic Second-Order Logic – A
Language-Theoretic Approach, volume 138 of Encyclopedia of mathematics
and its applications.
Cambridge University Press, 2012.

[14]
A. Deutsch, A. Nash, and J. B. Remmel.
The chase revisited.
In M. Lenzerini and D. Lembo, editors, Proceedings of the 27th
ACM SIGMOD-SIGACT-SIGART Symposium on Principles of Database Systems
(PODS'08), pages 149–158. ACM, 2008.

[15]
D. Florescu, A. Y. Levy, and D. Suciu.
Query containment for conjunctive queries with regular expressions.
In A. O. Mendelzon and J. Paredaens, editors, Proceedings of the
17th ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Database Systems
(PODS'98), pages 139–148. ACM, 1998.

[16]
H. Ganzinger, C. Meyer, and M. Veanes.
The two-variable guarded fragment with transitive relations.
In Proceedings of the 14th Annual IEEE Symposium on Logic in
Computer Science (LICS'99), pages 24–34. IEEE Computer Society, 1999.

[17]
B. Glimm, C. Lutz, I. Horrocks, and U. Sattler.
Conjunctive query answering for the description logic SHIQ.
Journal of Artificial Intelligence Research, 31:157–204, 2008.

[18]
K. Gödel.
Über die Vollständigkeit des Logikkalküls.
PhD thesis, Universität Wien, 1929.

[19]
M. C. Golumbic and U. Rotics.
On the clique-width of perfect graph classes.
In P. Widmayer, G. Neyer, and S. J. Eidenbenz, editors, Proceedings of the 25th International Workshop on Graph-Theoretic Concepts in
Computer Science (WG'99), volume 1665 of LNCS, pages 135–147.
Springer, 1999.

[20]
G. Gottlob.
Datalog+/-: A unified approach to ontologies and integrity
In V. D. Antonellis, S. Castano, B. Catania, and G. Guerrini,
editors, Proceedings of the 17th Italian Symposium on Advanced Database
Systems, (SEBD'09), pages 5–6. Edizioni Seneca, 2009.

[21]
G. Gottlob, G. Orsi, and A. Pieris.
Query rewriting and optimization for ontological databases.
ACM Transactions on Database Systems, 39(3):25:1–25:46,

[22]
M. Grohe and G. Turán.
Learnability and definability in trees and similar structures.
Theory of Computing Systems, 37(1):193–220, 2004.

[23]
E. Kieronski and S. Rudolph.
Finite model theory of the triguarded fragment and related logics.
In Proceedings of the 36th Annual ACM/IEEE Symposium on Logic
in Computer Science (LICS'21), pages 1–13. IEEE, 2021.

[24]
M. Krötzsch and S. Rudolph.
Extending decidable existential rules by joining acyclicity and
In T. Walsh, editor, Proceedings of the 22nd International Joint
Conference on Artificial Intelligence (IJCAI'11), pages 963–968.
IJCAI/AAAI, 2011.

[25]
M. Ortiz, S. Rudolph, and M. Simkus.
Query answering in the horn fragments of the description logics
SHOIQ and SROIQ.
In T. Walsh, editor, Proceedings of the 22nd International Joint
Conference on Artificial Intelligence (IJCAI'11), pages 1039–1044.
IJCAI/AAAI, 2011.

[26]
P. Ostropolski-Nalewaja, J. Marcinkowski, D. Carral, and S. Rudolph.
A journey to the frontiers of query rewritability.
CoRR, abs/2012.11269, 2020.

[27]
M. O. Rabin.
Decidability of second-order theories and automata on infinite trees.
Transactions of the American Mathematical Society, 141:1–35,

[28]
J. L. Reutter, M. Romero, and M. Y. Vardi.
Regular queries on graph databases.
Theory of Computing Systems, 61(1):31–83, 2017.

[29]
R. Rosati.
On the decidability and finite controllability of query processing in
databases with incomplete information.
In S. Vansummeren, editor, Proceedings of the 25th ACM
SIGACT-SIGMOD-SIGART Symposium on Principles of Database Systems
(PODS'06), pages 356–365. ACM, 2006.

[30]
S. Rudolph and M. Krötzsch.
Flag & check: Data access with monadically defined queries.
In R. Hull and W. Fan, editors, Proceedings of the 32nd ACM
SIGMOD-SIGACT-SIGART Symposium on Principles of Database Systems
(PODS'13), pages 151–162. ACM, 2013.

[31]
S. Rudolph, M. Krötzsch, and P. Hitzler.
All elephants are bigger than all mice.
In F. Baader, C. Lutz, and B. Motik, editors, Proceedings of the
21st International Workshop on Description Logics (DL2008), volume 353 of
CEUR Workshop Proceedings. CEUR-WS.org, 2008.

[32]
E. Salvat and M.-L. Mugnier.
Sound and complete forward and backward chainings of graph rules.
In P. W. Eklund, G. Ellis, and G. Mann, editors, Proceedings of
the 4th International Conference on Conceptual Structures (ICCS'96), volume
1115 of LNCS, pages 248–262. Springer, 1996.

[33]
W. Szwast and L. Tendera.
The guarded fragment with transitive guards.
Annals of Pure and Applied Logic, 128(1-3):227–276, 2004.

§ DEFINITION OF $\PHI_\MATHRM{WELL}$ (<REF>)

Recall that a decorated tree $\mathcal{T}$ is called a well-decorated tree

* for every null $s \in \{0,1\}^*$, $\mathcal{T}$ contains exactly one fact $\mathrm{Dec}(s)$ with  $\mathrm{Dec} \in \decorum$,

* for every $\const{c}\in \mathrm{Cnst}$, $\mathcal{T}$ contains at most one fact of the form $\pred{c}_k(s)$,

* if $\pred{Add}_{\rpred,\vk}(s) \in \mathcal{T}$ or $\pred{Recolor}_{k\to k'}(s) \in \mathcal{T}$,
then $\pred{Void}(s0)\not\in \mathcal{T}$ and $\pred{Void}(s1) \in \mathcal{T}$,

* if $\oplus(s) \in \mathcal{T}$, then $\pred{Void}(s0),\pred{Void}(s1) \not\in \mathcal{T}$,

* if $\pred{Void}(s) \in \mathcal{T}$ or $\pred{c}_k(s) \in \mathcal{T}$, then  $\pred{Void}(s0),\pred{Void}(s1) \in \mathcal{T}$.

Here, fixing $\cols$, $\Sigma$, and $\mathrm{Cnst}$,  we will define a first-order sentence $\Phi_\mathrm{well}$ such that for any $(\cols,\mathrm{Cnst},\Sigma)$-decorated tree $\mathcal{T}$, $\mathcal{T}$ is well-decorated $\mathcal{T} \models \Phi_\mathrm{well}$.

Let us denote $\decorum$ with $\Gamma$ and we write $\varphi^i_{\pred{Void}}(x)$ to abbreviate $\exists z (\pred{Succ}_i(x,z) \wedge \pred{Void}(z))$.
Consider the following (where $\pred{c} \in \mathrm{Cnst}$, $\pred{d} \in \mathrm{Cnst} \cup\{\pred{*}\}$):

\begin{align*}
\Phi^{\mathrm{funct}} &= \forall{x} \bigvee_{\mathrm{Dec} \in \Gamma}\Big( \mathrm{Dec}(x) \wedge \scaleobj{0.8}{\bigwedge_{\scaleobj{1.25}{\mathrm{Dec}' \in \Gamma \setminus \{\mathrm{Dec}\}}}} \neg\mathrm{Dec}'(x) \Big)\\
\Phi^{\mathrm{unique}}_{\pred{c}_k} &=  \forall{xy}\; \pred{c}_k(x) \Rightarrow (\pred{c}_k(y) \Rightarrow x = y) \wedge \bigwedge_{k'\in \cols\setminus\{k\}}\neg\pred{c}_{k'}(y)\\
\end{align*}

\begin{align*}
\Phi_{\pred{d}_k} &=  & \forall{x}\; \pred{d}_k(x) & \Rightarrow \ \ \varphi^0_{\pred{Void}}(x) \wedge \varphi^1_{\pred{Void}}(x)\\
\Phi_{\pred{Add}_{\rpred,\vk}} &= & \forall{x}\; \pred{Add}_{\rpred,\vk}(x) & \Rightarrow \neg \varphi^0_{\pred{Void}}(x) \wedge \varphi^1_{\pred{Void}}(x)\\
\Phi_{\pred{Recolor}_{k\to k'}} &= & \forall{x}\; \pred{Recolor}_{k\to k'}(x) & \Rightarrow \neg \varphi^0_{\pred{Void}}(x) \wedge \varphi^1_{\pred{Void}}(x)\\
\Phi_{\oplus} &= & \forall{x}\; \oplus(x) & \Rightarrow \neg \varphi^0_{\pred{Void}}(x) \wedge \neg\varphi^1_{\pred{Void}}(x)\\
\Phi_{\pred{Void}} &= &\forall{x}\; \pred{Void}(x) & \Rightarrow \ \ \varphi^0_{\pred{Void}}(x) \wedge \varphi^1_{\pred{Void}}(x)\\
\end{align*}

Then we let

\Phi_\mathrm{well} =
\Phi^{\mathrm{funct}} \wedge
\hspace{-3ex}\bigwedge_{\hspace{3ex}\pred{c}_k\in \Gamma,\,\pred{c} \in \mathrm{Cnst}}\hspace{-3ex} \Phi^{\mathrm{unique}}_{\pred{c}_k} \wedge
\bigwedge_{\mathrm{Dec}\in \Gamma} \Phi_{\mathrm{Dec}}.

§ PROOFS FOR <REF>

We define

\varphi^\mathrm{dom}(x) =
\hspace{-5ex}\bigvee_{\hspace{5ex}{\const{c} \in \mathrm{Const} \cup\{\const{*}\}}\atop {k \in \cols}}\hspace{-5ex}\const{c}_k(x)
\quad\text{ and }\quad
\varphi^\mathrm{Dom}(X) = \forall x. \Big( x{\in} X \to \varphi^\mathrm{dom}(x) \Big),

which are lifted to variable sequences by

\varphi^\mathrm{dom}(\vx) = \hspace{-4ex} \bigwedge_{\hspace{4ex} x\text{ from }\vx}\hspace{-3ex}\varphi^\mathrm{dom}(x)
\quad\text{ and }\quad
\varphi^\mathrm{Dom}(\VX) = \hspace{-4ex} \bigwedge_{\hspace{4ex} X\text{ from }\VX}\hspace{-3ex}\varphi^\mathrm{Dom}(X).

Furthermore, let

\thephi_\fcn{up}(x,y) = \szero(y,x) \vee \sone(y,x)

\varphi^\mathrm{colIn}_{k}(x,y) = \varphi^\mathrm{dom}(x) \wedge
\forall_{\ell \in \cols} X_\ell.
\Big(\big(\hspace{-3ex} \bigwedge_{\hspace{3ex}\psi \in M_{xy}}\hspace{-3ex}\psi\, \big) \to X_k(y)\Big),

where $X_\ell$ are MSO set variables and $M_{xy}$ contains the following formulae (for all respective elements of $\decorum$):

\begin{align*}
\const{c}_k(x) & \to X_{k}(x)\\
\forall x'\!y'\!. X_k(x') \wedge \thephi_\fcn{up}(x'\!,y') \wedge \pred{Add}_{\rpred,k',k''}(y') & \to X_{k}(y')\\
\forall x'\!y'\!. X_k(x') \wedge \thephi_\fcn{up}(x'\!,y') \wedge \pred{Add}_{\rpred,k'}(y') & \to X_{k}(y')\\
\forall x'\!y'\!. X_k(x') \wedge \thephi_\fcn{up}(x'\!,y') \wedge \pred{Recolor}_{k\to k'}(y') & \to X_{k'}(y')\\
\forall x'\!y'\!. X_k(x') \wedge \thephi_\fcn{up}(x'\!,y') \wedge \pred{Recolor}_{k'\!\to k''}(y') & \to X_{k}(y')\hspace{1.5ex}\text{for }k{\neq} k'\\
\forall x'\!y'\!. X_k(x') \wedge \thephi_\fcn{up}(x'\!,y') \wedge \oplus(y') & \to X_{k}(y')
\end{align*}

For each predicate $\rpred\in \Sigma$ of arity $n$, we define

\begin{align*}
\varphi_{\rpred_{n}}(x_1,\ldots,x_n) & =
\exists z.\hspace{-4ex}
\bigvee_{\hspace{2ex}
\scaleobj{0.9}{(k_1,\ldots,k_n) \in \cols^n}
\scaleobj{0.8}{\Big(}
\,\pred{Add}_{\rpred,k_1,\ldots,k_n}(z) \wedge\! \scaleobj{0.8}{\bigwedge_{\scaleobj{1.25}{1 \leq i \leq n}}} \varphi^\mathrm{colIn}_{k_i}(x_i,z)
\scaleobj{0.8}{\Big)}
\end{align*}

Let $\mathcal{T}$ be a $(\cols,\mathrm{Cnst},\Sigma)$-decorated tree.
For $\const{c}\in \mathrm{Cnst}$, let $\const{c}^\mathcal{T}$ denote the unique $s \in \{0,1\}^*$ with $\pred{c}_k(s)\in \mathcal{T}$. Moreover, we define the injection $\fcn{orig}: \adom{\inst^\mathcal{T}} \to \{0,1\}^*$
by letting $\fcn{orig}(e)=e^\mathcal{T}$ if $e\in \mathrm{Cnst}$, and $\fcn{orig}(e)=e$ otherwise.

Given an $(\cols,\mathrm{Cnst},\Sigma)$-well-decorated tree $\mathcal{T}$, we have:

* $\mathcal{T},\{x \mapsto s\} \models \varphi^\mathrm{dom}(x)$ $s = \fcn{orig}(e)$ for some $e \in \adom{\inst^\mathcal{T}}$,

* $\mathcal{T},\{X \mapsto S\} \models \varphi^\mathrm{Dom}(X)$ $S = \{\fcn{orig}(e) \mid e \in E\}$ for some $E \subseteq \adom{\inst^\mathcal{T}}$,

* $\mathcal{T},\{x \mapsto s,y \mapsto s'\} \models \varphi^\fcn{up}(x,y)$ $s \in \{s'0,s'1\}$,

* $\mathcal{T},\{x \mapsto s,y \mapsto s'\} \models \varphi^\mathrm{colIn}_{k}(x,y)$ $s = \fcn{orig}(e)$ for some $e \in \fcn{ent}^\mathcal{T}(s')$ and $\fcn{col}^\mathcal{T}_{s'}(e) = k$,

* $\mathcal{T},\{\vx \mapsto \vs\} \models \varphi_{\rpred_{n}}(x)$   $\vs = \fcn{orig}(\ve)$ for some $\rpred(\ve) \in \inst^\mathcal{T}$.

Most cases are immediate with earlier cases being used to show latter cases.
For $(4)$, note that $M_{xy}$ serves as a monadic datalog program (for which $x$ acts like a constant) that, following the path from $s$ upward, assigns to each node $s^*$ the appropriate coloring predicate $X_{\fcn{col}^\mathcal{T}_{s^*}(\fcn{orig}^{-1}(s))}$ (to be shown by induction over the distance of $s^*$ from $s$). The subformula
$$\forall_{\ell \in \cols} X_\ell.\Big(\big(\hspace{-3ex} \bigwedge_{\hspace{3ex}\psi \in M_{xy}}\hspace{-3ex}\psi\, \big) \to X_k(y)\Big)$$
then checks if the smallest fixpoint of $M_{xy}$ assigns $X_k$ to $s'$, which means $\fcn{col}^\mathcal{T}_{s'}(\fcn{orig}^{-1}(s))=k$.

An MSO formula $\xi$ over $\Sigma$ and $\mathrm{Cnst}$ is called normalized (i) the only connectives it uses are existential quantifiers (over set and individual variables), conjunction, and negation, and (ii) the constants $\const{c}\in \mathrm{Cnst}$ only occur in equality statements of the form $x=\const{c}$.
We then recursively define the function $\fcn{trans}$, mapping normalized MSO formulae over $\Sigma$ and $\mathrm{Cnst}$ to MSO formulae over $\decorum \cup \{\szero,\sone\}$ as follows (where $\xi(\vx,\VX)$ denotes an MSO formula with free individual variables $\vx$ and free set variables $\VX$):

\begin{align*}
%x=y & \ \mapsto\  \varphi^\mathrm{dom}(xy) \wedge x=y \\
x=y & \ \mapsto\  \varphi^\mathrm{dom}\tight(x) \land \varphi^\mathrm{dom}\tight(y) \wedge x=y \\
x=\const{c} & \ \mapsto\  \pred{c}_k(x) \\
%\rpred(x) & \ \mapsto\  \varphi_{\rpred_{1}}(x) \\
%\rpred(x,y) & \ \mapsto\  \varphi_{\rpred_{2}}(x,y) \\
\rpred(x_{1}, \ldots,x_{n}) & \ \mapsto\  \varphi_{\rpred_{n}}(x_{1}, \ldots,x_{n}) \\
\neg \xi(\vx,\VX) & \ \mapsto\ \varphi^\mathrm{dom}\tight(\vx) \wedge \varphi^\mathrm{Dom}\tight(\VX) \wedge \neg \fcn{trans}\big(\xi(\vx,\VX)\big) \\
\xi_1\tight(\vx_1,\VX_1) \wedge \xi_2\tight(\vx_2,\VX_2) & \ \mapsto\ \fcn{trans}\big(\xi_1\tight(\vx_1,\VX_1)\big) \wedge \fcn{trans}\big(\xi_2\tight(\vx_2,\VX_2)\big) \\
\exists x.\xi(\vx,\VX) & \ \mapsto\ \exists x.\Big(\varphi^\mathrm{dom}\tight(x) \wedge \fcn{trans}\big(\xi(\vx,\VX)\big)\Big)\\
\exists X.\xi(\vx,\VX) & \ \mapsto\ \exists X.\Big(\varphi^\mathrm{Dom}\tight(X) \wedge \fcn{trans}\big(\xi(\vx,\VX)\big)\Big)\\[-7.7ex]
\end{align*}

Every MSO formula can be converted into an equivalent normalized one.
The function $\fcn{trans}$ preserves free individual variables and free set variables.

By making use of standard equivalences (e.g. $\thephi \lor \psi \equiv \neg \thephi \land \neg \psi$,  $\thephi \rightarrow \psi \equiv \neg (\thephi \land \neg \psi)$, $\forall x \thephi \equiv \neg \exists x \neg \thephi$, and $\forall X \thephi \equiv \neg \exists X \neg \thephi$), every MSO formula can be converted into an equivalent normalized MSO formula. By a routine induction on the structure of a given normalized, MSO formula over $\sig$ and $\mathrm{Cnst}$, one can show that free individual and set variables are preserved through applications of $\fcn{trans}$.

Given a finite set of colors $\cols$, a finite set of constants $\mathrm{Cnst}$, and a signature $\Sigma$, let

* $\xi = \xi(\vx,\VX)$ be a normalized MSO formula over $\Sigma$ and $\mathrm{Cnst}$ with free individual variables $\vx$ and free set variables $\VX$,

* $\mathcal{T}$ be a $(\cols,\mathrm{Cnst},\Sigma)$-well-decorated tree,

* $\mathrm{Assig}$ be the set of assignments $\mu$ that map variables from $\vx$ to terms from $\adom{\mathcal{T}}$ and set variables from $\VX$ to subsets of $\adom{\mathcal{T}}$,

* $\mathrm{Assig}'$ be the set of assignments $\mu$ that map variables from $\vx$ to terms from $\adom{\inst^\mathcal{T}}$ and set variables from $\VX$ to subsets of $\adom{\inst^\mathcal{T}}$,

* for some $\mu \in \mathrm{Assig}'$, denote with $\mu_\fcn{orig}$ the assignment from $\mathrm{Assig}$ that satisfies $\mu_\fcn{orig}(x) = \fcn{orig}(\mu(x))$ for every $x$ from $\vx$ and $\mu_\fcn{orig}(X) = \{\fcn{orig}(t) \mid t \in \mu(X)\}$ for every $X$ from $\VX$.

\{ \mu \in \mathrm{Assig} \mid \mathcal{T},\mu \models \fcn{trans}(\xi)\}
\{ \mu_\fcn{orig}' \mid \mu' \in \mathrm{Assig}', \inst^\mathcal{T},\mu' \models \xi\}.

We prove the result by induction on the structure of $\xi$, which we take to be a normalized MSO formula over $\sig$ and $\cnst$.

Base case. We have three cases to consider: either (i) $\xi$ is of the form $x = y$, (ii) $\xi$ is of the form $x = \const{c}$, or (iii) $\xi$ is of the form $\rpred(x_{1}, \ldots, x_{n})$.
We prove cases (i) and (iii) as (ii) is similar, and in both cases we first show that the left side of the equation is a subset of the right, and then that the right side of the equation is a subset of the left.

(i) Suppose that $\mathcal{T},\mu \models \fcn{trans}(x = y)$. By <ref> above, $\fcn{trans}(x = y) = \varphi^\mathrm{dom}(x) \land \varphi^\mathrm{dom}(y) \wedge x=y$, implying that for $\mu(x) = \mu(y) = s \in \{0,1\}^{*}$. Moreover, since $\mathcal{T}, \mu \models \varphi^\mathrm{dom}(x) \land \varphi^\mathrm{dom}(y)$, there exists an $e \in \fcn{ent}^\mathcal{T}\!(\varepsilon)$ (that is, $e$ is a term in $\inst^{\mathcal{T}}$) such that $\orig(e) = s$. Let us define $\mu'(z) = \orig^{-1}(\mu(z))$ for $z \in \{x,y\}$. Then, $\mu'(x) = \orig^{-1}(\mu(x)) = e = \orig^{-1}(\mu(y)) = \mu'(y)$, showing that $\inst^{\mathcal{T}}, \mu' \models x = y$. Therefore, $\mu_{\orig}' = \mu$ is an element of the right side of the equation.

To show the opposite direction, let $\mu' \in \mathrm{Assig}'$ and suppose that $\inst^\mathcal{T},\mu' \models \xi$. Then, there exists a term $e$ in $\inst^{\mathcal{T}}$ (that is, an $e \in \fcn{ent}^\mathcal{T}\!(\varepsilon)$) such that $\mu'(x) = \mu'(y) = e$. As the function $\orig$ is injective, we have that $\mu_{\orig}'(x) = \mu_{\orig}'(y) = s \in \{0,1\}^{*}$, and also, since $e \in \fcn{ent}^\mathcal{T}\!(\varepsilon)$, it follows that $\mathcal{T}, \mu_{\orig}' \models \varphi^\mathrm{dom}(x) \land \varphi^\mathrm{dom}(y)$. Thus, $\mu_{\orig}'$ is an element of the left side of the equation, establishing that the two sets are indeed equal.

(iii) Suppose that $\mathcal{T}, \mu \models \fcn{trans}(\rpred(x_{1}, \ldots, x_{n}))$. By <ref> above, $\fcn{trans}(\rpred(x_{1}, \ldots, x_{n})) = \thephi_{\rpred_{n}}(x_{1}, \ldots, x_{n})$, that is to say,

\mathcal{T}, \mu \models \exists z. \bigvee_{(k_1,\ldots,k_n) \in \cols^{n}} \Big(\pred{Add}_{\rpred,k_1,\ldots,k_n}(z) \wedge \bigwedge_{1 \leq i \leq n} \varphi^\mathrm{colIn}_{k_i}(x_i,z) \Big)

Then, for $\mu[s/z]$ (which is the same as $\mu$, but maps $z$ to $s$) and some $(k_1,\ldots,k_n) \in \cols^{n}$, we know that

\mathcal{T}, \mu[s/z] \models \pred{Add}_{\rpred,k_1,\ldots,k_n}(z) \wedge \bigwedge_{1 \leq i \leq n} \varphi^\mathrm{colIn}_{k_i}(x_i,z).

Let $s_{i} = \mu[s/z](x_{i})$ for $i \in \{1,\ldots,n\}$. By <ref>, there exist $e_{1}, \ldots, e_{n} \in \ent^{\mathcal{T}}(s)$ such that $e_{i} = \orig(s_{i})$ and $\col^{\mathcal{T}}_{s}(e_{i}) = k_{i}$, for $i \in \{1, \ldots,n\}$, and by <ref>, we know that $\rpred(e_{1}, \ldots, e_{n}) \in \inst^{\mathcal{T}}$. Let $\mu'(y) = \orig^{-1}(\mu(y))$ for $y \in \{x_{1},\ldots,x_{n}\}$. Then, it follows that $\inst^{\mathcal{T}}, \mu' \models \rpred(x_{1},\ldots, x_{n})$, showing that $\mu = \mu_{\orig}'$ is an element of the right side of the equation.

For the opposite direction, suppose that $\mu' \in \mathrm{Assig}'$ and $\inst^{\mathcal{T}}, \mu' \models \rpred(x_{1}, \ldots, x_{n})$. Therefore, there exist terms $e_{1}, \ldots, e_{n}$ in $\inst^{\mathcal{T}}$
such that $\mu'(x_{i}) = e_{i}$ for $i \in \{1, \ldots, n\}$, and $\rpred(e_{1}, \ldots, e_{n}) \in \inst^{\mathcal{T}}$. Let $\orig(e_{i}) = s_{i}$, for $i \in \{1, \ldots, n\}$. Since $\rpred(e_{1}, \ldots, e_{n}) \in \inst^{\mathcal{T}}$, by <ref> there must exist an $s$ in $\mathcal{T}$ with $e_{1},\ldots, e_{n} \in \ent^{\mathcal{T}}(s)$ such that $\pred{Add}_{\rpred,k_{1}, \ldots, k_{n}}(s) \in \mathcal{T}$ and $\col_{s}^{\mathcal{T}}(e_{i}) = k_{i}$, for $i \in\{1, \ldots,n\}$. Therefore, $\mathcal{T}, \mu_{\orig}' \models \thephi_{\rpred_{n}}(x_{1}, \ldots,x_{n})$, showing that $\mu_{\orig}'$ is an element of the left side of the equation.

Inductive step. We have four cases to consider: either (i) $\xi$ is of the form $\neg \xi' (\vx,\VX)$, (ii) $\xi$ is of the form $\xi_{1}(\vx_{1},\VX_{1}) \land \xi_{2}(\vx_{2},\VX_{2})$, (iii) $\xi$ is of the form $\exists x. \xi'(\vx,\VX)$, or (iv) $\xi$ is of the form $\exists X. \xi'(\vx,\VX)$. We show cases (ii) and (iv) as the remaining cases are proven in a similar fashion. As before, we first show that the left side of the equation is a subset of the right, and then the opposite.

(ii) Suppose that $\mathcal{T},\mu \models \mathrm{trans}(\xi)$. By our assumption, $\mathrm{trans}(\xi) = \mathrm{trans}(\xi_{1}(\vx_{1},\VX_{1}) \land \xi_{2}(\vx_{2},\VX_{2}))$, which by <ref>, is equal to $\mathrm{trans}(\xi_{1}(\vx_{1},\VX_{1})) \land \mathrm{trans}(\xi_{2}(\vx_{2},\VX_{2}))$. It follows that $\mathcal{T}, (\mu \restriction i) \models \mathrm{trans}(\xi_{i}(\vx_{i},\VX_{i}))$ for $i \in \{1,2\}$ (with $(\mu \restriction i) = \mu \restriction \{\vx_{i},\VX_{i}\}$), from which it follows that there exist $\mu^{1}$ and $\mu^{2}$ such that $\inst^{\mathcal{T}}, \mu^{i} \models \xi_{i}(\vx_{i},\VX_{i})$ and $\mu^{i}_{\orig} = (\mu \restriction i)$ for $i \in \{1,2\}$. Let us define

\[
\mu'(z) =
\begin{cases}
(\mu^{i})(z) & \text{if $z$ is in $\vx_{1},\vx_{2}$} \\
(\mu^{i})(Z) & \text{if $Z$ is in $\VX_{1},\VX_{2}$.}
\end{cases}
\]

Observe that $\inst^{\mathcal{T}}, \mu' \models \xi_{1}(\vx_{1},\VX_{1}) \land \xi_{2}(\vx_{2},\VX_{2})$ and that $\mu_{\orig}' = \mu$, thus showing that $\mu$ is an element of the right side of the equation.

For the opposite direction, let $\mu' \in \mathrm{Assig}'$ and assume that $\inst^{\mathcal{T}}, \mu' \models \xi_{1}(\vx_{1},\VX_{1}) \land \xi_{2}(\vx_{2},\VX_{2})$. Let $(\mu' \restriction i) = \mu' \restriction \{\vx_{i},\VX_{i}\}$ and observe that $\inst^{\mathcal{T}}, (\mu' \restriction i) \models \xi_{i}(\vx_{i},\VX_{i})$ for $i \in \{1,2\}$. Therefore, by IH, we have $\mathcal{T}, (\mu' \restriction i)_{\orig} \models \mathrm{trans}(\xi_{i}(\vx_{i},\VX_{i}))$ for $i \in \{1,2\}$, which entails that $\mathcal{T}, \mu_{\orig}' \models \mathrm{trans}(\xi_{1}(\vx_{1},\VX_{1})) \land \mathrm{trans}(\xi_{2}(\vx_{2},\VX_{2}))$. Hence, $\mu_{\orig}'$ is an element of the left side of the equation.

(iv) Let us suppose that $\mathcal{T},\mu \models \mathrm{trans}(\exists X. \xi(\vx,\VX))$, that is to say,

\mathcal{T}, \mu \models \exists X.\Big(\varphi^\mathrm{Dom}(X) \wedge \fcn{trans}\big(\xi(\vx,\VX)\big)\Big).

It follows that $\mathcal{T}, \mu[X/S] \models \varphi^\mathrm{Dom}(X) \wedge \fcn{trans}\big(\xi(\vx,\VX)\big)$ for some $S \subseteq \{0,1\}^{*}$ with $\mu[X/S]$ the same as the assignment $\mu$, but where the set variable $X$ is mapped to $S$. By IH, we know that $\inst^{\mathcal{T}}, \mu'[X/S] \models \xi(\vx,\VX)$, where $\mu'[X/S](z) = \orig^{-1}(\mu[X/S](z))$ for $z$ in $\vx$ and $\mu'[X/S](Z) = \orig^{-1}(\mu[X/S](Z))$ for $Z$ in $\VX$. Note that $\mu'[X/S]$ is defined because $\mathcal{T}, \mu[X/S] \models \varphi^\mathrm{Dom}(X)$, i.e., there exists a set $E \subseteq \ent^{\mathcal{T}}(\varepsilon)$ such that $S = \{\orig(e) \ | \ e \in E\}$. Hence, $\inst^{\mathcal{T}}, \mu' \models \exists X. \xi(\vx,\VX)$, showing that $\mu_{\orig}' = \mu$ is an element of the right side of the equation.

For the opposite direction, let $\mu' \in \mathrm{Assig}'$ and assume that $\inst^{\mathcal{T}}, \mu' \models \exists X. \xi(\vx,\VX)$. This entails that $\inst^{\mathcal{T}}, \mu'[X/E] \models \xi(\vx,\VX)$ for some set $E$ of terms in $\inst^{\mathcal{T}}$ (i.e., for some $E \subseteq \ent^{\mathcal{T}}(\varepsilon)$) with $\mu'$ being the same as $\mu'$, but where the set variable $X$ is mapped to $E$. By IH, we have that $\mathcal{T}, \mu'[X/E]_{\orig} \models \xi(\vx,\VX)$, where $\mu'[X/E]_{\orig}$ is equal to the assignment $\mu_{\orig}'[X/S]$ with $S = \{\orig(e) \ | \ e \in E\}$. We have that

\mathcal{T}, \mu_{\orig}' \models \exists X.\Big(\varphi^\mathrm{Dom}(X) \wedge \fcn{trans}\big(\xi(\vx,\VX)\big)\Big)

is a consequence, thus showing that $\mu_{\orig}'$ is an element of the left side of the equation.

Given a finite set of colors $\cols$, a finite set of constants $\mathrm{Cnst}$, and a signature $\Sigma$, if

* $\mathcal{T}$ is a $(\cols,\mathrm{Cnst},\Sigma)$-well-decorated tree, and

* $\Xi$ is a normalized MSO sentence over $\Sigma$ and $\mathrm{Cnst}$,

\mathcal{T} \models \fcn{trans}(\Xi) \text{\ \ \ \iffi \ \ }
\inst^\mathcal{T} \models \Xi.

The corollary follows directly from <Ref> above, as it serves as a special case where the normalized MSO formula over $\Sigma$ and $\mathrm{Cnst}$ contains no free variables.

Let $n\in \mathbb{N}$. Determining if a given MSO formula $\Xi$

has a model $\inst$ with $\cw{\inst} \leq n$ is decidable.

Let $\cols=\{1,\ldots,n\}$, $\mathrm{Cnst}$ be the set of all constants mentioned in $\Xi$, and $\Xi' = \fcn{trans}(\Xi)$. By <Ref>, we know that for the sentence $\Xi$ (which uses the signature $\decorum \cup \{\szero,\sone\}$) and any $(\cols,\mathrm{Cnst},\Sigma)$-well-decorated tree $\mathcal{T}$, $\instance^\mathcal{T} \models \Xi$ $\mathcal{T} \models \Xi'$. Hence, in order to check if $\Xi$ is satisfiable in some instance of cliquewidth less than or equal to $n$, we can compute $\Xi'$ and check if it is satisfiable in an $(\cols,\mathrm{Cnst},\Sigma)$-well-decorated tree $\mathcal{T}$. Checking if $\Xi'$ is satisfiable in some well-decorated tree $\mathcal{T}$ is equivalent to checking if $\Xi'\wedge \Phi_\mathrm{well}$ is satisfiable in an arbitrary $(\cols,\mathrm{Cnst},\Sigma)$-decorated tree $\mathcal{T}'$. Let us define $\Xi''$ to be $\Xi'\wedge \Phi_\mathrm{well}$ where (i) all predicates from $\decorum$ are replaced by MSO set variables, which are (ii) quantified over existentially. Observe that $\Xi''$ is an MSO formula over the signature $\{\szero,\sone\}$, which will be valid on $\ibtree$ some decoration exists satisfying $\Xi'\wedge \Phi_\mathrm{well}$. Thus, we have reduced our problem to checking the validity of an MSO sentence on $\ibtree$, which is decidable by Rabin's Tree Theorem [27].

Let $\inst$ be a countable instance over a binary signature.
If $\inst$ has finite treewidth, then $\inst$ has finite cliquewidth.

§ JUSTIFICATION OF <REF> (<REF>)

To provide some insight into why $\inst_\mathrm{tern}$ from <Ref> does not have finite cliquewidth, first observe that the instance has the structure of the natural number line, but with an additional term (viz. $-1$) that stands in a ternary relation with each natrual number and its successor. We will argue that no coloring $\coloring$ exists such that $(\inst_{\mathrm{tern}},\coloring)$ is isomorphic to a colored instance represented by some well-decorated tree $\mathcal{T}$. For a contradiction, let us suppose the contrary. Then, we may assume w.l.o.g. that some node $s$ in $\mathcal{T}$ is decorated with $-1_k(s)$ (if $-1$ is assumed to be a null, introduced by a node $\const{*}_k(s)$, then an almost identical argument can be given). Now, we know that at some node $s'$ along the path from $s$ to the root $\varepsilon$ of $\mathcal{T}$ a disjoint union will occur introducing an infinite amount of pairs of consecutive natural numbers. In order for the ternary edges to be added between $-1$ and each pair of consecutive natural numbers, an infinite number of $\pred{Add}_{\rpred,\vk}$ operations are required. However, since only a finite number of operations can be performed after the introduction of $-1$ (as only a finite number of nodes exist between $s$ and the root $\varepsilon$ of $\mathcal{T}$), all such ternary edges cannot be added, showing that for all colorings $\coloring$, $(\inst_{\mathrm{tern}},\coloring)$ is not isomorphic to a colored instance represented by some well-decorated tree. Concomitantly, the rule set $\ruleset_\mathrm{tern} = \{ \rpred(v,x,y) \to \exists z \rpred(v,y,z) \}$ is $\bts$, but not $\fcs$.

§ PROPERTIES OF REIFICATION (<REF>)

§ PROOFS FOR <REF>

$\se$ is a typed polyforest of bounded degree.

Since $\ruleset$ is a set of single-headed rules over a binary signature, and since we only consider non-datalog rules (as $\se$ only contains atoms derived by the non-datalog rules from $\ruleset$), we know that each rule $\rho$ applied during the Skolem chase (see <ref>) is of the form $\phi(\vec{x},y) \rightarrow head(\rho)$ with $head(\rho) \in \{\exists z \rpred(y,z), \exists z \rpred(z,y),\\ \exists z \exists z' \rpred(z,z')\}$. That is to say, for each rule $\rho$, $\fr(\rho) = 1$ or $\fr(\rho) = 0$. Observe that if a rule of frontier $1$ is applied during the Skolem chase, then it gives rise to a single edge (typed with the predicate $R$ occurring in the head of the rule) in
$\se $ that can either be directed toward (if $\head(\rho) = \exists z \rpred(y,z)$) or away from (if $\head(\rho) = \exists \vec{z} \rpred(z,y)$) the frontier term it is attached to. If a rule of frontier $0$ is applied during the Skolem chase, then it creates a disconnected typed edge that corresponds to, and gives rise to, a new typed polytree in
$\se$. Hence, we can see that
$\se$ is a typed polyforest. Moreover, as we are using the Skolem chase and due to the fact that $\ruleset$ is finite, there can only be a finite number of typed edges added to each vertex in the typed polyforest, ensuring that it is of bounded degree.

$\ksat{1}{\sed, \rulesetnormcon}$ has finite treewidth.

Given an instance $\inst$ and two its terms $t, t'$ define the distance $\ldist{\inst}{t,t'}$ from $t$ to $t'$ in $\inst$ as the minimal length of any path from $t$ to $t'$ treating binary atoms of $\inst$ as undirected edges.

For a null $t$ of $\se$ and a natural number $n$ let neighbourhood $\neigh{n}{t}$ of $t$ of distance $n$ be a following set of terms $\set{t \in \termset(\sed) \;|\; \ldist{\sed}{t, t'} \leq n}$. Also let $\neigh{n}{\db} = \set{t \;|\; \exists{\const{c}\in\adom{\db}}\\ \ldist{\sed}{t,\const{c}} < n}$. Observe that every $t^n$ (and $\neigh{n}{\db}$) is finite as $\sed$ have bounded degree - a direct consequence of Skolem chase usage.

Let $T_n = (V_n, E_n)$ be a following tree decomposition:

* $V_n = \set{\neigh{n}{t} \;|\; t \in \nullset(\se) } \cup \set{\neigh{n}{\db}}$.

* $E_n = \set{(\neigh{n}{t}, \neigh{n}{t'}) \;|\;  \wedge\exists{\rpred\in\sig}\; \se \models \rpred(t,t') \vee \rpred(t', t)} \;\cup\;\\ \set{(\neigh{n}{\db}, \neigh{n}{t}) \;|\;  \exists{\const{c} \in \conset(\db)}\; \exists{\rpred\in\sig} \se \models \rpred(t,\const{c}) \vee \rpred(\const{c}, t)}$.

Now we will argue that for every $n > 1$ tree $T_n$ is a tree decomposition of $\sed$ as:

* $\bigcup_{v\in V_n}v$ is equal to $\termset(\sed)$.

* Each atom $\rpred(t,t')$ of $\sed$ is indeed contained in one of bags of $V_n$, namely $\neigh{n}{t}$, as $n > 1$.

* From the definition of neighbourhood, one can note that for each term $t$ in $\sed$, the subgraph of $T_n$ induced by the nodes $v$ of $V$ such that $t \in v$ is connected.

Let $d \in \mathbb{N}$ be such that for every rule $\rho \in \rulesetnormcon$, with two frontier variables $x,y$, the following holds $d \geq \ldist{\body(\rho)}{x,y}$. Note that such a $d$ exists because $x$ and $y$ share the same connected component of $\body(\rho)$. Finally, observe that for every atom $\rpred(t,t')$ of $\ksat{1}{\sed, \rulesetnormcon} \setminus (\sed)$ we have that $t,t' \in \neigh{d}{t}$ or $t,t' \in \neigh{d}{\db}$. From this we conclude that $T_d$ is a tree decomposition of $\ksat{1}{\sed, \rulesetnormcon}$ of bounded width.

§.§ Recoloring lemma

Let $\inst$ be an

satisfying $\cw{\inst} = n$ and let $\coloring' : \adom{\inst} \to \cols'$ be an arbitrary coloring of $\inst$. Then $\cw{\inst,\coloring'} \leq (n+1) \cdot |\cols'|.$

First, consider the following:

Let $\inst$ be a countable instance over some signature $\sig$. Moreover, let $\coloring : \adom{\inst} \to \cols$ and $\coloring' : \adom{\inst} \to \cols'$ be two colorings and let $\coloring {\times} \coloring'$ denote the coloring
of $\inst$ defined by $\coloring {\times} \coloring'(t) = (\coloring(t), \coloring'(t))$. If $\cw{\inst, \coloring} \leq |\cols|$, then $\cw{\inst, \coloring {\times} \coloring'} \leq |\cols| \cdot |\cols'|$.

Let $(\inst, \coloring)$ be a colored instance and $\coloring'\colon\adom{\inst}\to \cols'$ another coloring for $\inst$. Furthermore, let $\cw{\inst, \lambda} = k$. Then there exists for a finite set of colors $\cols$ a well $(\cols, \mathrm{Cnst}, \Sigma)$-decorated tree $\mathcal{T}$ such that $\inst^{\mathcal{T}}=\inst$ and $\fcn{col}^\mathcal{T} = \coloring$.
We obtain a $(\cols\times\cols', \mathrm{Cnst}, \Sigma)$-decorated tree $\mathcal{T}'$ inductively over the nodes of $\mathcal{T}$ and $\mathcal{T}'$ in the following way:

Transformations. Let $s, s'\in \{ 0,1 \}^{\ast}$ and $N_{p} \subseteq (\{ 0,1 \}^{\ast})^{2}$. Furthermore, let $\sigma \colon \{ 1, \ldots, |\cols'| \} \to \cols'$ be a bijection enumerating every color in $\cols'$.

*  If $\oplus(s)\in \mathcal{T}$, then $\oplus(s') \in \mathcal{T}^{s}$ and add to $N_{p}$ the pairs $(s0, s'0)$ and $(s1, s'1)$.

*  If for $\const{c}\in \mathrm{Cnst} \cup \{ \const{*} \}$ and $\ell\in\cols$, $\pred{c}_{\ell}(s)\in \mathcal{T}$, then $\pred{c}_{(\ell, \lambda'(s))}(s')\in \mathcal{T}^{s}$ and add to $N_{p}$ the pairs $(s0, s'0)$ and $(s1, s'1)$.

*  If $\pred{Void}(s)\in \mathcal{T}_{s}$, then add $\pred{Void}(s')$ to $\mathcal{T}'$ and add to $N_{p}$ the pairs $(s0, s'0)$ and $(s1, s'1)$.

*  If for $\rpred\in\Sigma_1$ and $\ell\in\cols$ $\pred{Add}_{\rpred, \ell}(s)\in\mathcal{T}_{s}$, then add

\[ \{ \pred{Add}_{\rpred, (\ell, \ell')}(0^{i-1}) \, | \,  1\le j \le |\cols'|, \, \sigma(j) = \ell' \} \]
to $\mathcal{T}^{s}$ and add to $N_{p}$ for $1\le i\le k'$ the pairs $(s0, s'0^{i})$ and $(s1, s'0^{i-1}1)$.

*  If for $\rpred\in\Sigma_2$ and $\ell_1, \ell_2\in\cols$ $\pred{Add}_{\rpred, \ell_1, \ell_2}(s)\in\mathcal{T}_s$, then add

\begin{align*}
\{ \pred{Add}_{\rpred, (\ell_1, \ell_1'), (\ell_2, \ell_2')}&(0^{i-1 + (j-1)\cdot |\cols'|}) \, | \\
& 1\le i, j \le |\cols'|, \, \sigma(i) = \ell_1' , \, \sigma(j) = \ell_2'  \}
\end{align*}

to $\mathcal{T}^{s}$ and add to $N_{p}$ for $1\le i, j\le k'$ the pairs $(s0, s'0^{i + (j-1)\cdot k'})$ and $(s1, s'0^{i-1 + (j-1)\cdot k'}1)$.

*  If for $\ell_1, \ell_2\in\cols$ $\pred{Recolor}_{\ell_1 \to \ell_2}(s)\in\mathcal{T}_{s}$, then add

\begin{align*}
\{ \pred{Recolor}_{(\ell_1, \ell_1') \to (\ell_2, \ell_2')}&(0^{i-1 + (j-1)\cdot |\cols'|}) \, |  \\
& 1\le i, j \le |\cols'|, \, \sigma(i) = \ell_1' , \, \sigma(j) = \ell_2' \}
\end{align*}

to $\mathcal{T}^{s}$ and add to $N_{p}$ for $1\le i, j\le k'$ the pairs $(s0, s'0^{i + (j-1)\cdot k'})$ and $(s1, s'0^{i-1 + (j-1)\cdot k'}1)$.

Base case. Initialize $N_{p} = \{ (\varepsilon, \varepsilon) \}$. Then apply the appropriate transformation for the tuple $(\varepsilon, \varepsilon)$.

Induction Step. Suppose $N_p$ has been obtained after a finite amount of transformations. With $\prec$ we denote the usual prefix order on $\{ 0,1 \}^{\ast}$. We define a partial order on $N_p$ in the following way:
\[ (s_1, s_1') < (s_2, s_2') \quad \text{\ifandonlyif} \quad s_1 \prec s_2 \text{ or } s_1 = s_2 \land s_1' \prec s_2' \, . \]
Take the tuple $(s,s')\in N_p$ such that $(s,s')$ is a $|s'|$-minimal and $<$-maximal element in $N_p$. Then apply the appropriate transformation to $(s,s')$.

Finally, obtain $\mathcal{T}' = \mathcal{T}_{\mathrm{bin}}\cup \bigcup_{s\in\ \{0,1\}^{\ast}}\mathcal{T}^{s}$.

We now show some properties of the set $N_p$.

*  If $(s, s')\in N_p$ with $\const{c}\in \mathrm{Cnst} \cup \{ \const{*} \}$ and $\pred{c}_{\ell}(s)\in\mathcal{T}$ for some $\ell\in \cols$, then $\pred{c}_{(\ell, \lambda'(s))}(s')\in \mathcal{T}'$ and $s'$ is the unique $s''\in \{ 0, 1\}^{\ast}$ such that $(s,s'')\in N_p$.

Let $s\in \{ 0,1 \}^{\ast}$ and for some $\ell\in \cols$ and $\const{c}\in \mathrm{Cnst}$ it holds that $\const{c}_{\ell}(s)\in \mathcal{T}$. Furthermore, suppose that $s', s''\in \{ 0,1 \}^{\ast}$ such that $(s, s'), (s,s'')\in N_p$ with $\pred{c}_{(\ell, \lambda'(s))}(s'), \pred{c}_{(\ell, \lambda'(s))}(s'')\in \mathcal{T}^{s}$. This can only happen, if there was previously a transformation applied for $r, s''' \in \{ 0,1 \}^{\ast}$ to $(r, s''')\in N_p$ with $\pred{Succ}_0(r, s)\in \mathcal{T}$ and $s''' \prec s', s''$ such that either

*  for $\rpred\in\Sigma_1$ and $k\in\cols$ $\pred{Add}_{\rpred, k}(r)\in\mathcal{T}$, or

*  for $\rpred\in\Sigma_2$ and $k_1, k_2\in\cols$ $\pred{Add}_{\rpred, k_1, k_2}(r)\in\mathcal{T}$, or

*  for $k_1, k_2\in\cols$ $\pred{Recolor}_{k_1 \to k_2}(r)\in\mathcal{T}$.

But then w.l.o.g. (in case <ref>) $s' = s'''0^{i}$ and $s'' = s'''0^{j}$ with $1\le i < j \le |\cols'|$ or (in cases <ref> and <ref>) $s' = s'''0^{i}$ and $s'' = s'''0^{j}$ with $1\le i < j \le |\cols'|^{2}$. But then, by the Inductions Step, Transformation <ref> is only applied to the tuple $(s, s'''0^{|\cols'|})$ (in case <ref>) or $(s, s'''0^{|\cols'|^{2}})$ (in cases <ref> and <ref>) as this is $<$-maximal for the introduced $N_p$-pairs. Hence $s'''0^{|\cols'|^{2}} = s' = s''$, showing uniqueness. Furthermore, by Transformation <ref> we obtain $\pred{c}_{(\ell, \lambda'(s))}(s'), \pred{c}_{(\ell, \lambda'(s))}(s'')\in \mathcal{T}^{s}$.

*  If $(s, s')\in N_p$ with $\pred{Void}(s)\in\mathcal{T}$, then $\pred{Void}(s')\in \mathcal{T}'$ and for all $s''\in\{ 0,1 \}^{\ast}$ with $s' \prec s''$ we have $\pred{Void}(s'')$.

If $(s, s')\in N_p$, application of Transformation <ref> yields $\pred{Void}(s')\in \mathcal{T}'$. As then $(s0, s'0), (s1, s'1)$ are added to $N_p$, applications of Transformation <ref> to both will yield $\pred{Void}(s'0)\in \mathcal{T}'$ and $\pred{Void}(s'1)\in \mathcal{T}'$. Inductively we obtain for all $s''\in\{ 0,1 \}^{\ast}$ with $s' \prec s''$ we have $\pred{Void}(s'')$.

$\mathcal{T}'$ is a well $(\cols\times\cols', \mathrm{Cnst}, \Sigma)$-decorated tree.

* For every $s\in \{ 0,1 \}^{\ast}$, $\mathrm{Dec}(s)\in\mathcal{T}'(s)$ for exactly one $\mathrm{Dec} \in \mathrm{Dec}(\cols', \mathrm{Cnst}, \Sigma)$ by constructions.

* Since, by construction, if for $\const{c}\in \mathrm{Cnst}$, $(\ell_1, \ell_2)\in \cols\times\cols'$ and $s'\in\{ 0,1 \}^{\ast}$ it holds that $\pred{c}_{(\ell_1, \ell_2)}(s')\in\mathcal{T}'$, then there is a $s\in\{ 0,1 \}^{\ast}$ such that $\pred{c}_{\ell_1}(s')\in\mathcal{T}$ and $(s, s')\in N_p$. By Property <ref> $s'$ is unique for $s$. On the other hand, Transformation <ref> is only executed, if there is a pair $(s, s')\in N_p$ with $\pred{c}_{\ell_1}(s')\in\mathcal{T}$. In conclusion, for every $s'\in \{ 0,1 \}^{\ast}$, $\const{c}\in \mathrm{Cnst}$, and $\ell\in\cols\times\cols'$ there is at most one fact of the form $\pred{c}_{\ell}(s')\in\mathcal{T}'$.

* If $\pred{Void}(s')\in\mathcal{T}'$ or $\pred{c}_{(\ell_1, \ell_2)}(s')\in \mathcal{T}'$, then $\pred{Void}(s'0), \pred{Void}(s'1)$. In the case of $\pred{Void}(s')\in \mathcal{T}'$ this follows immediately from Property <ref>. If on the other hand $\pred{c}_{(\ell_1, \ell_2)}(s')\in \mathcal{T}'$ we observe that there exists by construction exactly one $s\in\{0,1 \}^{\ast}$ such that $\pred{c}_{\ell_1}(s)\in\mathcal{T}$ and $(s, s')\in N_p$. Note that $\pred{c}_{(\ell_1, \ell_2)}(s')$ was then produced by application of Transformation <ref> and $(s0, s'0), (s1, s1')$ will have been added to $N_p$. Application of Transformation <ref> then has yielded $\pred{Void}(s'0), \pred{Void}(s'1)\in \mathcal{T}'$ as $\pred{Void}(s0), \pred{Void}(s1)\in\mathcal{T}$.

* If $\oplus(s')\in\mathcal{T}$ then $\pred{Void}(s'0), \pred{Void}(s'1)\not\in \mathcal{T}'$ follows by construction.

* If for $\ell, \ell'\in\cols\times\cols'$ we have $\pred{Recolor}_{\ell\to \ell'}(s') \in \mathcal{T}'$ or $\pred{Add}_{\rpred,\ell,\ell'}(s') \in \mathcal{T}'$ or $\pred{Add}_{\rpred,\ell}(s') \in \mathcal{T}'$ then by definition of Transformations <ref> - <ref> $\pred{Void}(s'0)\not\in \mathcal{T}'$ and $\pred{Void}(s'1) \in \mathcal{T}'$ hold by construction.

We now show that $\mathcal{I}^{\mathcal{T}'}$ and $\mathcal{I}^{\mathcal{T}}$ are isomorphic and $\fcn{col}_{\epsilon}^{\mathcal{T}'} = \coloring \times \coloring'$.
Obtaining the isomorphism works as follows: By Property <ref> for every $(s,s')\in N_p$ such that for some $\const{c}\in \mathrm{Cnst}\cup\{ \const{*} \}$ and $\ell\in \cols$ it holds that $\pred{c}_{\ell}(s)\in\mathcal{T}$, $s'$ is unique. Furthermore, by construction we obtain
\[ \mathrm{Cnst}\cap ent^{\mathcal{T}}(\varepsilon) = \mathrm{Cnst}\cap ent^{\mathcal{T}'}(\varepsilon) \, . \]
Hence we define $h_{\mathrm{Cnst}}\colon \mathrm{Cnst}\cap \fcn{ent}^{\mathcal{T}}(\varepsilon) \to \mathrm{Cnst} \cap \fcn{ent}^{\mathcal{T}'}(\varepsilon), \const{c}\mapsto \const{c}$, which is a bijection by the discussion beforehand.
We extend $h_{\mathrm{Cnst}}$ to $h$ by mapping each $s\in\{ 0,1 \}^{\ast}$ with $\pred{*}_{k}(s)\in\mathcal{T}$ to the unique $s'\in\{ 0,1 \}^{\ast}$ such that $(s, s')\in N_p$. This yields a bijection $h\colon \fcn{ent}^{\mathcal{T}}(\varepsilon) \to \fcn{ent}^{\mathcal{T}'}(\varepsilon)$. We show that $h$ is an isomorphism $\inst^{\mathcal{T}} \to \inst^{\mathcal{T}'}$. We need only to show that atoms are preserved in both directions.
We show this in the case of binary atoms, the rest will be analogously dealt with. So let $\rpred(t_0, t_1)\in\inst^{\mathcal{T}}$ be an atom. Then there exist a $s\in\{ 0,1 \}^{\ast}$ such that $R(t_0, t_1)\in Atoms_{s}^{\mathcal{T}}$, and $s_0, s_1\in\{ 0, 1\}^{\ast}$ such that the nodes $ss_0 = t_0$ and $ss_1 = t_1$. Then there are $s', s_0', s_1'\in\{ 0,1 \}^{\ast}$, with the later two unique, such that

* $(s, s'), (ss_0, s's_0'), (ss_1, s's_1') \in N_p$,

* $\pred{Add}_{\rpred, k_0, k_1}(s)\in\mathcal{T}$,

* $\fcn{col}_s^{\mathcal{T}}(t_0) = k_0$ and $\fcn{col}_s^{\mathcal{T}}(t_1) = k_1$,

* $\fcn{col}_{ss_0}^{\mathcal{T}}(t_0) = \ell_0$ and $\fcn{col}_{ss_1}^{\mathcal{T}}(t_1) = \ell_1$,

* $\fcn{col}_{s's_0'}^{\mathcal{T}'}(h(t_0)) = (\ell_0, \coloring'(ss_0))$ and $\fcn{col}_{s's_1'}^{\mathcal{T}}(h(t_1)) = (\ell_1, \coloring'(ss_1))$,

* $\pred{Add}_{\rpred, (k_0, \coloring'(ss_0)) , (k_1, \coloring'(ss_1))}(s')\in\mathcal{T}'$, and

* $\fcn{col}_s^{\mathcal{T}'}(h(t_0)) = (k_0, \coloring'(ss_0))$ and $\fcn{col}_s^{\mathcal{T}'}(h(t_1)) = (k_1, \coloring'(ss_1))$.

Hence $\rpred(h(t_0), h(t_1))\in\inst^{\mathcal{T}'}$. The backwards-direction works similarly. For uniqueness note that by construction for every pair $(s,s')\in N_p$ the $s$ will be unique for the $s'$.

Last, $\fcn{col}_{\epsilon}^{\mathcal{T}'} = \coloring \times \coloring'$ is plain as every entity will be introduced with the color given by $\coloring'$ in the second component in $\mathcal{T}'$.

To get <ref> from <ref> we note that it is enough to project colors of $(\inst, \coloring \times \coloring')$ onto to their second components with $\fcn{Recolor}_{(\ell,\ell') \to \ell'}$. Note that the resulting coloring function will have an extended codomain (comparing to $\coloring \times \coloring'$) to $\cols \times \cols' \cup \cols'$.

§ EXTENDED VERSION OF <REF>

We will now prove <ref> implying that for multi-headed rules, $\fus$ is no longer subsumed by $\fcs$. To this end, we exhibit a $\fus$ rule set which may unavoidably lead to universal models of infinite cliquewidth.

We let $\sigi = \set{\hpred, \vpred}$ with $\hpred$ and $\vpred$ being binary predicates. Let us define $\rsgrid$ to be the following rule set over $\sigi$:

\begin{array}{@{}l@{\ \ \ \ \ \ }r@{\ }l@{\ \ \ \ \ \ \ \ }}
\text{(loop)} & \top & \rightarrow \exists x \; (\hpred(x,x) \land \vpred (x,x)) \\[0.5ex]
\text{(grow)} & \top & \rightarrow \exists y \exists y'\; (\hpred(x,y) \land \vpred (x,y')) \\[0.5ex]
\text{(grid)} & \hpred(x,y) \land \vpred(x,x')  & \rightarrow \exists y' \; (\hpred(x',y') \land \vpred(y,y'))
\end{array}

We make use of $\rsgrid$ to establish <ref>, whose proof is split into two parts. First, we provide a database $\dbg$ to form a knowledge base $(\dbg, \rsg)$ for which no universal model of finite cliquewidth exists (<ref>). Second, we show that $\rsg$ is a finite unification set (<ref>).

§.§ $\rsgrid$ is not a finite-cliquewidth set

We devote this section to establishing the subsequent lemma, which is sufficient to conclude <ref>.

Let $\const{a}$ be a constant and let $\dbg = \set{\top(\const{a})}$ be a database. Then, no universal model of finite cliquewidth exists for $\kbaseg$.

With the aim of establishing the lemma above, we define the instance $\ginf$ below, where $\const{a}$ is a constant and $x_{i,j}$ and $y$ are nulls for $i,j \in \mathbb{N}$. To provide the reader with further intuition, a graphical depiction of $\ginf$ is given in <ref>.

\begin{eqnarray*}
\ginf & = & \{\top(\const{a}),\hpred(\const{a},x_{1,0}),\vpred(\const{a},x_{0,1}),\hpred(y,y),\vpred(y,y)\} \\
& & \cup \big\{\hpred(x_{i,j},x_{i+1,j}) \ | \  (i,j) \in (\mathbb{N} \times \mathbb{N}) \setminus \{(0,0)\} \big\} \\
& & \cup \big\{\vpred(x_{i,j},x_{i,j+1}) \ | \  (i,j) \in (\mathbb{N} \times \mathbb{N}) \setminus \{(0,0)\} \big\}
\end{eqnarray*}

It is straightforward to show that $\ginf$ serves as a model of $\kbaseg$, and a routine exercise to prove that $\ginf$ is universal. Hence, we have the following:

$\ginf$ is a universal model of $\kbaseg$.

It is known that the cliquewidth of an $n \times n$ grid tends to infinity as $n$ tends to infinity <cit.>, entailing that any infinite grid will have an infinite cliquewidth since the cliquewidth of any instance bounds the cliquewidth of any induced sub-instance from above. By making use of this fact, along with the subsequent two, we can prove <ref> below.

Let $\sig$ be a binary signature, $\epred$ be a binary predicate,
$\inst$ be an instance over $\sig$, and $\inst' = \set{\epred(t,t') \ | \ \rpred(t,t') \in \inst, \rpred \in \sig}$. Then, $\cw{\inst} \geq \cw{\inst'}$.

Let $\sig$ be a signature consisting of a single binary predicate $\epred$, let $\inst$ be an instance over $\sig$, and let $\inst' = \set{\epred(t',t) \ | \ \epred(t,t') \in \inst} \cup \inst$. Then, $\cw{\inst} \geq \cw{\inst'}$.

$\ginf$ has an infinite cliquewidth.

The observation follows from the previous two facts, the fact that infinite grids have infinite cliquewidth, and the fact that adding a set of the form $\{\hpred(y, y), \vpred(y, y) \}$ with $\const{a}$ a constant and $y$ a null to any instance does not lower its cliquewidth.

We now leverage the above result to demonstrate that every universal model of $\kbaseg$ has an infinite cliquewidth. Observe that if we consider any homomorphism from $\ginf$ to itself, then (i) the null $y$ must be mapped to itself as no other terms are associated with loops, and (ii) the constant $a$ must be mapped to itself, thus anchoring the image of $\ginf$ under the homomorphism at the origin of the grid shown in <ref>, thus ensuring that each term of the grid will map to itself accordingly. It follows that any homomorphism from $\ginf$ to itself will be the identity function, giving rise to the following observation.

If $h: \ginf \to \ginf$ is a homomorphism then $h$ is the identity.

We now make use of the above observation to show that every universal model of $\kbaseg$ contains a sub-instance that is isomorphic to $\ginf$, thus ensuring that every universal model of $\kbaseg$ is of infinite cliquewidth (by <ref> and the fact that the cliquewidth of an instance is greater than or equal to the cliquewidth of any induced sub-instance). From this lemma, we may conclude  <ref> and thus <ref>.

Every universal model of $\kbaseg$ contains an induced sub-instance isomorphic to $\ginf$.

Let $\unimod$ be a universal model of $\kbaseg$. As $\ginf$ is a universal model (by <ref> above), we know that two homomorphisms $h\colon \ginf \to \unimod$ and $h'\colon \unimod \to \ginf$ exist between $\unimod$ and $\ginf$. Let us consider the homomorphism $h' \circ h$. By <ref>, the homomorphism $h'\circ h$ is the identity on $\ginf$, implying that $h$ is injective. Furthermore, $h$ is reflective, and hence, constitutes an embedding. To show this, suppose that $\rpred\in\sigi$ and let $\vt$ be a tuple of length $\arity{\rpred}$ from $\ginf$. If $\rpred(h(\vt))$ holds in $\unimod$ , then $\rpred((h' \circ h)(\vt))$ holds in $\ginf$, but since $h'\circ h$ is the identity on $\ginf$, we immediately obtain that $\rpred(\vt)$  holds in $\ginf$. Finally, note that the image of $\ginf$ under $h$ serves as the induced sub-instance of $\unimod$ that is isomorphic to $\ginf$, completing the proof.

§.§ $\rsgrid$ is a finite-unification set

As we have now shown that $\rsgrid$ is not a finite-cliquewidth set, we focus our attention on demonstrating <ref>, which is restated below, and from which we may conclude the final main result (<ref>).

$\rsg$ is $\fus$.

As the rule $(loop)$ is a member of $\rsg$, every BCQ that is free of constants can be trivially re-written, implying the following:

Every BCQ that is free of constants is FO-rewritable with respect to $\rsg$.

Showing that a provided rule set is $\fus$ is a notoriously difficult task.[This should not be too surprising however, as being $\fus$ is an undecidable property [3].] To this end, we hand-tailor a rewriting algorithm to be used for the proof of <ref>. However, one can refer to existing rewriting algorithms, e.g., XRewrite [21], for additional intuition. Finally, it is important to note that the proof closely follows the ideas provided in [26].

§.§ Necessary definitions

We first introduce special queries, referred to as marked queries, which are queries supplemented with a set of markings, the significance of which, is to keep track of what terms of the CQs are mapped to constants in a given database throughout the course of rewriting. A marked CQ is defined to be a pair $(q, M)$ where $q$ is a CQ and the set of markings $M$ is a subset of terms (i.e., variables and constants) of $q$. Given an instance $\inst$ we say that $\inst \models (q,M)$ $\iffi$ there exists a homomorphism $h$ mapping $q$ to $\inst$ such that for every term $t$ of $q$ we have $t \in M$ $\iffi$ $h(t)$ is a constant in $\inst$.

We now make a useful observation, which follows by considering the structures that arise when applying the rules from $\rsgrid$ to any given database. Afterward, we show that marked queries take on a special form when interpreted on the instance $\sg$, where $\db$ is an arbitrary database.

Let $\db$ be a database. Then,

* if $\hpred(t,t')$ or $\vpred(t,t')$ is an atom of $\sg$ and $t'\in \adom{\db}$, then $t\in \adom{\db}$,

* if there is a cycle $C \subseteq \sg$ that contains at least one constant, then $C \subseteq \db$,

* if $\rpred(t_1,t'), \rpred(t_2,t') \in \sg$ with $\rpred\in\{\hpred, \vpred\}$ and $t_1\in  \adom{\db}$, then $t_2\in  \adom{\db}$,

* if $\rpred(\const{a},t), \rpred(\const{b},t) \in \sg$ with $\rpred\in\{\hpred, \vpred\}$ and $\const{a}\neq \const{b}$ are constants, then $t$ is a constant.

Keeping the above observation in mind, we define the notion of a properly marked CQ.

A marked CQ $(q, M)$ is properly marked when:

* if $\const{a}$ is a constant in $q$, then $\const{a} \in M$,

* if $\hpred(t,t')$ or $\vpred(t,t')$ is an atom in $q$ and $t' \in M$, then $t \in M$,

* if there is a cycle $C$ in $q$ that contains at least one constant, then all terms of $C$ are contained in $M$,

* if $\rpred(t_1,t')$ and $\rpred(t_2,t')$ are two atoms in $q$ with $\rpred\in\{\hpred, \vpred\}$ and $t_1 \in M$, then $t_2 \in M$,

* if $\rpred(\const{a},t)$ and $\rpred(\const{b},t)$ are two atoms in $q$ with $\rpred\in\{\hpred, \vpred\}$ and $\const{a}\neq \const{b}$ are constants, then $t \in M$.

If $\sg \models q$, then there exists a set of markings $M$ such that $(q,M)$ is properly marked and $\sg \models (q,M)$.

Suppose that $\sg \models q$. Then, we know that a homomorphism $h$ exists mapping terms from $q$ into $\sg$. Let $M$ be the set of terms from $q$ such that $h(t)$ is mapped to a constant in $\sg$. One can readily check if $(q,M)$ is properly marked, and if not, add the terms from $q$ to $M$ accordingly until a properly marked CQ $(q,M')$ is constructed such that $\sg \models (q,M)$.

From <ref> and <ref> we immediately conclude the following:

Let $(q, M)$ be a marked query, and $\db$ be any database. If $\sg \models \mq$, then $\mq$ is properly marked.

Let us refer to a marked CQ $(q, M)$ as alive given that it is properly marked and $M$ does not contain all terms of $q$. In the case where every term of a properly marked CQ is marked, we refer to the CQ as dead.

To prove <ref> it suffices to prove the following lemma, which we direct our attention to in the subsequent section.

For any properly marked CQ $(q, \prmark)$ there exists a set of dead queries $\fcn{rew}(q,\prmark)$ such that for any database $\db$ the following holds:

$\sg \models (q,\prmark)$  $\iffi$  $\exists{Q' \in \fcn{rew}(q, \prmark)}, \db \models Q'.$

§.§ Rewriting Alive Queries

We begin this section by proving the following lemma, which will later prove useful in rewriting queries relative to $\rsgrid$.

If a marked CQ $(q,\prmark)$ is alive, then there exists a variable $x$ in $q$ such that no atom of the form $\rpred(x,t)$ occurs in $q$ with $\rpred\in \{\hpred,\vpred\}$.

Let the marked CQ $(q,\prmark)$ be alive. Then, by the definition above, we know that there exists a set of terms in $q$ that are not a members of $M$. Since $(q,\prmark)$ is properly marked, by <ref>, we know that all such terms are not constants, and hence, all such terms must be variables. Let us refer to all such terms as unmarked variables. If we consider the sub-instance of the CQ induced by all unmarked variables, we can see that (i) it forms a directed acyclic graph as all cycles of the CQ must be in $M$ by <ref>, which (ii) is non-empty as $(q,\prmark)$ is alive. Hence, there must exists a variable $x$ in $q$ such that no atom of the form $\rpred(x,t)$ occurs in $q$ with $\rpred\in \{\hpred,\vpred\}$, which corresponds to a sink in the directed acyclic graph described above.

We will refer to unmarked variables – such as those described in the above proof – which possess no out-going edges, as maximal. These maximal variables will be used to initiate our rewriting process.

Let $x$ be a maximal variable of an alive CQ $(q, \prmark)$. Then, one of the following holds:

*  $x$ occurs in exactly one atom  $\rpred(t,x)$, with $\rpred\in \{\hpred,\vpred\}$ for some term $t$ of $q$,

*  $x$ occurs in exactly two atoms $\hpred(t_{\hpred},x)$ and $\vpred(t_{\vpred},x)$ for some terms $t_{\hpred},t_{\vpred}$ of $q$,

*  there exist at least two distinct terms $t\neq t'$ such that $\rpred(t,x)$ and $\rpred(t',x)$ are atoms of $q$ with $\rpred\in \{\hpred,\vpred\}$.

Rewriting Operations.
We now make use of <ref> to define three operations that compute rewritings. When exhaustively applied to a query, we obtain the rewritings required by <ref>. Given an alive CQ $(q, \prmark)$ we define the following three operations:

Let $x$ be a maximal variable of $(q, \prmark)$ satisfying case <ref> of <ref>, i.e., $x$ occurs in exactly one atom $\rpred(t,x)$ of $q$ with $\rpred\in \{\hpred, \vpred\}$. Then, letting $\query = \query' \cup \{\rpred(t,x)\}$, we define

\[
\ \ \ \ \cutop((q,\prmark), \set{x}) =
\begin{cases}
(q' \cup \{\top(\const{c})\}, \prmark)  & \text{if $t$ is a constant $\const{c}$} \\[-1ex]
& \text{not occurring in $\query'$;}\ \ \ \ \ \ \\
(q', \prmark) & \text{otherwise.}\defend
\end{cases}
\]

Let $x, t_{\hpred}$, and $t_{\vpred}$ be as in case <ref> of <ref>, meaning that there exist two atoms of the form $\hpred(t_{\hpred}, x)$ and $\vpred(t_{\vpred}, x)$ in $q$. We define $q'$ to be the same as $q$, but where $\hpred(t_{\hpred}, x)$ and $\vpred(t_{\vpred}, x)$ are replaced by $\hpred(x', t_{\vpred})$ and $\vpred(x', t_{\hpred})$, and where $x'$ is fresh. We now
define $\reduceop((q,\prmark), \set{x}) = \set{ (q', \prmark), (q', \prmark \cup \set{x'})}$.

Let $x, t$, and $t'$ be as in case <ref> of <ref>. We let $q'$ be obtained from $q$ by replacing all occurrences of $t$ in $q$ with $t'$ and define $\mergeop((q, \prmark), \set{x, t, t'}) = (q' \cup \{\top(t)\}, \prmark)$.

Let us briefly describe how rewritings are computed by means of the above operations.
Given an alive CQ $(q,M)$, we know that one of the three rewriting operations will be applicable (by <ref>), which we note, may return a set of rewritings if the $\reduceop$ operation is applied. We ultimately obtain the set $\fcn{rew}(q, \prmark)$ of rewritings of $(q,\prmark)$ by sequentially applying the three rewriting operations to all alive queries within the set of rewritings, until all marked queries in the set are dead, at which point, the rewriting process terminates. As shown below, we can always apply a rewriting operation to a CQ if it is alive (i.e., rewriting is complete), and also, applying such an operation preserves satisfaction on $\sg$ (i.e., rewriting is sound).

If a CQ is alive then at least one of above operations can be applied to it.

Follows from <ref>, and <ref>.

Let us now prove the soundness of the above operations:

Let $\db$ be a database and let $\mquery$ be an alive CQ. If $x$ is as in <ref>, then

$$\sg \models \mquery \ \text{\iffi} \ \sg \models \cutop(\mquery, \set{x}).$$

Let $\mquery = (\query,\prmark)$ be an alive CQ and $\cutop(\mquery, \set{x}) = (q',M)$. The forward direction is trivial. For the backward direction, assume that $\sg \models \cutop(\mquery, \set{x})$. By our assumption, there exists a homormorphism $h$ from $\query'$ into $\sg$ such that for all terms $t$ in $\query'$, $t \in M$ $h(t)$ is a constant in $\sg$. Since the $\cutop$ operation was applied, we know that there exists exactly one atom of the from $\rpred(t,x)$ in $\query$ with $\rpred\in \{\hpred,\vpred\}$ and $x$ a maximal variable. We have two cases to consider: either (i) the term $t$ exists in $\query'$, or (ii) the term $t$ does not exist in $\query'$.

(i) Suppose that the term $t$ exists in $\query'$. Then, $h$ maps $t$ to some element $t'$ of $\sg$. Based on the functionality of the rules in $\rsgrid$, one can see that for every term $t''$ in $\sg$ and $\ppred \in \{\hpred,\vpred\}$, there exists a null $y$ such that $\ppred(t'',y) \in \sg$. Therefore, there exists a null $y$ such that $\rpred(t',y) \in \sg$. Let us define the homomorphism $h'$ such that $h'(s) = h(s)$ for all terms $s \neq x$ in $\query$ and $h'(x) = y$. It follows that $h'$ is a homomorphism from $\query$ to $\sg$, and thus $\sg \models \query$.

To complete the proof of this case, it suffices to show that for all terms $t$ in $\query$ that $t \in M$ $h'(t)$ is a constant in $\sg$. If we consider only the terms $s \neq x$ in $\query$, then the above equivalence holds as $h'(s) = h(s)$ for all such terms and we know that for all terms $s$ in $\query'$ that $s \in M$ $h(s)$ is a constant in $\sg$. The above equivalence also holds for the maximal variable $x$ since $x \not\in M$ and $h'(x) = y$ maps to a null (and not a constant) in $\sg$. This completes the proof of this case.

(ii) Suppose that the term $t$ does not exist in $\query'$. We know that either (a) the term $t$ is a constant $\const{c}$, or (b) the term $t$ is a variable $y$. We prove both cases below.

(a) Assume that $t$ is a constant $\const{c}$. If $\const{c}$ does not occur in the database $\db$, then $\sg \not\models \cutop(\mquery, \set{x})$, contrary to our assumption. Hence, we may assume that $\const{c}$ occurs in $\db$. By the (grow) rule in $\rsgrid$, we know that for the constant $\const{c}$ in $\db$, there exists a null $z$ such that $\rpred(\const{c},z) \in \sg$. Let us extend the homomorphism $h$ to a homomorphism $h'$ such that $h'(s) = h(s)$ for $s \neq x$ and $h'(x) = z$. It is straightforward to show that $h'$ is a homomorphism from $\query$ to $\sg$, and showing that for all terms $t'$ in $\query$ we have $t' \in M$ $h'(t')$ is a constant in $\sg$ is argued similarly as in case (i) above.

(b) Assume that $t$ is a variable $y$. Based on the (loop) rule in $\rsgrid$, we know that there exists a null $z$ such that $\rpred(z,z) \in \sg$. Let us now extend the homomorphism $h$ to a homomorphism $h'$ such that $h'(s) = h(s)$ for $s \not\in\{y,x\}$ and $h'(y) = h'(x) = z$. It is straightforward to show that $\sg \models \mquery$ by making use of $h'$.

Let $\db$ be a database and let $Q$ be an alive CQ. If $x$ is as in <ref> and $\reduceop(\mquery, \set{x}) = \set{\mquery_{1}, \mquery_{2}}$, then

$$\sg \models \mquery \ \text{\iffi} \ \exists i \in \{1,2\}, \sg \models \mquery_{i}.$$

Let $Q = (\query,M)$ and $\mquery_{i} = (\query',M_{i})$ with $i \in \{1,2\}$.

For the forward direction, suppose that $\sg \models \mquery$. It follows that there exists a homomorphism $h$ such that $h$ maps $\query$ to $\sg$ and for all terms $t$ in $\query$, $t \in M$ $h(t)$ is a constant in $\sg$. By our assumption that $\reduceop$ was applied, we know that there exist two atoms of the form $\hpred(t_{\hpred},x)$ and $\vpred(t_{\vpred},x)$ in $\query$ with $x$ maximal and $x$ occurring in no other atoms of $\query$. We have two cases to consider: either (i) both $t_{\hpred}$ and $t_{\vpred}$ are constants, or (ii) at least one term is not a constant. We argue each case accordingly.

(i) Observe that if both $t_{\hpred}$ and $t_{\vpred}$ are constants, then since $\mquery$ is properly marked, we know that $x \in M$ by <ref>. However, this contradicts our assumption that $x$ is maximal, and so, this case cannot occur.

(ii) In the alternative case, by the functionality of the Skolem chase (see <ref>), the fact that our rule set is $\rsgrid$, and since one term maps to a null in $\sg$ via $h$, we know that the (grid) rule must have been applied for $\hpred(h(t_{\hpred}),h(x))$ and $\vpred(h(t_{\vpred}),h(x))$ to occur in $\sg$. It follows that for some term $t$, $\hpred(t,h(t_{\vpred}))$ and $\vpred(t,h(t_{\hpred}))$ must occur in $\sg$. Let us define the homomorphism $h'$ such that $h'(s) = h(s)$ for each term $s \neq x$ in $\query$ and $h'(x') = t$. Then, we have that $\sg \models \query'$. Note that if $t$ is a null, then $\sg \models Q_{1}$ and if $t$ is a constant, then $\sg \models Q_{2}$, thus showing the desired conclusion.

Let us now show the backward direction and assume that there exists an $i \in \{1,2\}$ such that $\sg \models \mquery_{i}$. We have that $\sg \models \query'$, meaning that there exists a homomorphism $h$ mapping $\query'$ into $\sg$. Due to the fact that $\reduceop$ was applied, it follows that there exist atoms $\hpred(x',t_{\vpred})$ and $\vpred(x',t_{\hpred})$ in $\query'$ that are mapped into $\sg$, that is to say, $\hpred(h(x'),h(t_{\vpred})),\vpred(h(x'),h(t_{\hpred})) \in \sg$. By the (grid) rule and the functionality of the Skolem chase, there exists a null $y$ such that $\hpred(h(t_{\hpred}),y),\vpred(h(t_{\vpred}),y) \in \sg$. Let us define the homomorphism $h'$ such that $h'(s) = h(s)$ for all terms $s \neq x'$ in $\query'$ and $h'(x) = y$. Then, $h'$ is a homomorphism from $\query$ to $\sg$ and it is straightforward to show that for all terms $t'$ in $\query$, $t' \in M$ $h'(t')$ maps to a constant in $\sg$.

Let $\db$ be a database and let $\mquery$ be an alive CQ. If $x, t$, and $t'$ are as in <ref>, then

$$\sg \models \mquery \ \text{\iffi} \ \sg \models \mergeop(\mquery, \set{x, t, t'}).$$

Let $Q = (\query,M)$, $\mergeop(\mquery, \set{x, t, t'}) = (\query',M )$, $\rpred \in \{\hpred, \vpred\}$, and $\query' = \query'' \cup \{\top(t)\}$.

For the forward direction, assume that $\sg \models \mquery$. It follows that there exists a homomorphism $h$ such that $h$ maps $\query$ into $\sg$ and for all terms $s$ in $\query$, $s \in M$ $h(s)$ is a constant in $\sg$. Also, since $\mergeop$ was applied, we know that there are at least two terms $t \neq t'$ such that $\rpred(t,x)$ and $\rpred(t',x)$ are in $\query$ and that $t'$ was substituted for $t$ in $\query$ to obtain $\query'$. Hence, $\rpred(h(t),h(x)), \rpred(h(t'),h(x)) \in \sg$, however, since we are using rules from $\rsgrid$ and by the functionality of the Skolem chase (see <ref>), it must be the case that either (i) $h(t)$, $h(x)$, and $h(t')$ all occur in $\db$, or (ii) $h(t) = h(x) = h(t') = y$ with $y$ the null generated by the (loop) rule. In case (i), $h(x)$ will be a constant as all terms of $\db$ are constants, meaning that $x$ will not be maximal, in contradiction to our assumption. Let us consider case (ii) then.
Note that in case (ii), the entire connected component of $\query$ containing $t$, $x$, and $t'$ is mapped to $y$ via $h$, meaning that the entire connected component of $\query'$ containing $x$ and $t'$ will be mapped to $y$ via $h$ as well. If we restrict our attention to the remaining connected components of $\query'$, then we can see that $h$ maps all such components homomorphically into $\sg$, showing that $h$ serves a homomorphism from $\query'$ to $\sg$. Last, we must show that for all terms $s'$ in $\query'$, $s' \in M$ $h(s')$ is a constant in $\sg$, however, this follows from the fact that $\query$ and $\query'$ have the same set of terms.

For the backward direction, suppose that $\sg \models \mergeop(\mquery, \set{x, t, t'})$. Then, there exists a homomorphism $h$ such that $h$ maps $\query'$ into $\sg$ and for all terms $s$ in $\query'$, $s \in M$ $h(s)$ is a constant in $\sg$. In addition, as $\mergeop$ was applied, there are at least two terms $t \neq t'$ such that $\rpred(t,x)$ and $\rpred(t',x)$ are in $\query$ with $t'$ substituted for $t$ in $\query$ to obtain $\query'$. Let us define a homomorphism $h'$ such that $h'(s) = s$ for all terms $s \neq t$ and $h'(t) = t'$. Then, $h'$ is a homomorphism from $\query$ to $\query'$, and since $h$ is a homomorphism from $\query'$ to $\sg$, we have that $h \circ h'$ is a homomorphism from $\query'$ to $\sg$. To finish the proof of the backward direction, we need to show that for all terms $s'$ in $\query$, $s' \in M$ $(h \circ h')(s')$ is a constant in $\sg$.

Let $s'$ be a term in $\query$. Suppose that $s' \in M$. Then, if $s' \neq t$, we have that $h(s')$ is a constant in $\sg$, and since $h(s') = (h \circ h')(s')$, it follows that $(h \circ h')(s')$ is a constant in $\sg$. If $s' = t$, then by <ref>, $t' \in M$, from which it follows that $h(t') = (h \circ h')(t)$ is a constant in $\sg$. Let us now suppose that $(h \circ h')(s')$ is a constant in $\sg$. If $s' \neq t$, then $(h \circ h')(s') = h(s')$ is a constant in $\sg$, implying that $s' \in M$; however, if $s' = t$, then $(h \circ h')(s') = (h \circ h')(t) = h(t')$ is a constant in $\sg$, implying that $t' \in M$, so by <ref>, $t \in M$ as well.

Given two queries $\mquery$ and $\mquery'$, we write $\mquery \stepop \mquery'$ $\mquery'$ can be obtained from $\mquery$ by applying $\reduceop$, $\cutop$, or $\mergeop$. We let $\stepop^*$ denote the transitive closure of $\stepop$.

For any properly marked CQ $\mquery$ the set of properly marked queries $\set{Q' \;|\; \mquery \stepop^* \mquery'}$ is finite.

Observe that $\cutop$ deletes the only atom containing the considered maximal variable and $\mergeop$ reduces the number of atoms containing the considered maximal variable. Moreover, neither $\cutop$ nor $\mergeop$ introduce converging atoms of the form $\hpred(t_{1},t)$ and $\vpred(t_{2},t)$ when applied. Since the operation $\reduceop$ reduces the number of such converging atoms in a properly marked CQ as well, and since all such operations either preserve or decrease the number of terms occurring the query, it follows that the rewriting process will eventually terminate.

By <ref> (Completeness), <ref> (Soundness), and <ref> (Termination), we may conclude <ref>, thus completing the proof of <ref>.

§ PROOFS FOR <REF>

<ref>[Soundness — $\cutop$]
Let $\db$ be a database and let $\mquery$ be an alive CQ. If $x$ is as in <ref>, then

$$\sg \models \mquery \ \text{\iffi} \ \sg \models \cutop(\mquery, \set{x}).$$

Let $\mquery = (\query,\prmark)$ be an alive CQ and $\cutop(\mquery, \set{x}) = (q',M)$. The forward direction is trivial, so we focus on the backward direction and assume that $\sg \models \cutop(\mquery, \set{x})$. By our assumption, there exists a homormorphism $h$ from $\query'$ into $\sg$ such that for all terms $t$ in $\query'$, $t \in M$ $h(t)$ is a constant in $\sg$. Since the $\cutop$ operation was applied, we know that there exists exactly one atom of the from $\rpred(t,x)$ in $\query$ with $\rpred\in \{\hpred,\vpred\}$ and $x$ a maximal variable. We have two cases to consider: either (i) the term $t$ exists in $\query'$, or (ii) the term $t$ does not exist in $\query'$.

(i) Suppose that the term $t$ exists in $\query'$. Then, $h$ maps $t$ to some element $t'$ of $\sg$. Based on the functionality of the rules in $\rsgrid$, one can see that for every term $t''$ in $\sg$ and $\ppred \in \{\hpred,\vpred\}$, there exists a null $y$ such that $\ppred(t'',y) \in \sg$. Therefore, there exists a null $y$ such that $\rpred(t',y) \in \sg$. Let us define the homomorphism $h'$ such that $h'(s) = h(s)$ for all terms $s \neq x$ in $\query$ and $h'(x) = y$. It follows that $h'$ is a homomorphism from $\query$ to $\sg$, and thus $\sg \models \query$.

To complete the proof of this case, it suffices to show that for all terms $t$ in $\query$ that $t \in M$ $h'(t)$ is a constant in $\sg$. If we consider only the terms $s \neq x$ in $\query$, then the above equivalence holds as $h'(s) = h(s)$ for all such terms and we know that for all terms $s$ in $\query'$ that $s \in M$ $h(s)$ is a constant in $\sg$. The above equivalence also holds for the maximal variable $x$ since $x \not\in M$ and $h'(x) = y$ maps to a null (and not a constant) in $\sg$. This completes the proof of this case.

(ii) Suppose that the term $t$ does not exist in $\query'$. We know that either (a) the term $t$ is a constant $c$, or (b) the term $t$ is a variable $y$. We prove both cases below.

(a) Assume that $t$ is a constant $c$. If $c$ does not occur in the database $\db$, then $\sg \not\models \cutop(\mquery, \set{x})$, contrary to our assumption. Hence, we may assume that $c$ occurs in $\db$. By the (grow) rule in $\rsgrid$, we know that for the constant $c$ in $\db$, there exists a null $z$ such that $\rpred(c,z) \in \sg$. Let us extend the homomorphism $h$ to a homomorphism $h'$ such that $h'(s) = h(s)$ for $s \neq x$ and $h'(x) = z$. It is straightforward to show that $h'$ is a homomorphism from $\query$ to $\sg$, and showing that for all terms $t'$ in $\query$ we have $t' \in M$ $h'(t')$ is a constant in $\sg$ is argued similarly as in case (i) above.

(b) Assume that $t$ is a variable $y$. Based on the (loop) rule in $\rsgrid$, we know that there exists a null $z$ such that $\rpred(z,z) \in \sg$. Let us now extend the homomorphism $h$ to a homomorphism $h'$ such that $h'(s) = h(s)$ for $s \not\in\{y,x\}$ and $h'(y) = h'(x) = z$. It is straightforward to show that $\sg \models \mquery$ by making use of $h'$.

<ref>[Soundness — $\reduceop$]
Let $\db$ be a database and let $Q$ be an alive CQ. If $x$ is as in <ref> and $\reduceop(\mquery, \set{x}) = \set{\mquery_{1}, \mquery_{2}}$, then

$$\sg \models \mquery \ \text{\iffi} \ \exists i \in \{1,2\}, \sg \models \mquery_{i}.$$

Let $Q = (\query,M)$ and $\mquery_{i} = (\query',M_{i})$ with $i \in \{1,2\}$.

For the forward direction, suppose that $\sg \models \mquery$. It follows that there exists a homomorphism $h$ such that $h$ maps $\query$ to $\sg$ and for all terms $t$ in $\query$, $t \in M$ $h(t)$ is a constant in $\sg$. By our assumption that $\reduceop$ was applied, we know that there exist two atoms of the form $\hpred(t_{\hpred},x)$ and $\vpred(t_{\vpred},x)$ in $\query$ with $x$ maximal and $x$ occurring in no other atoms of $\query$. We have two cases to consider: either (i) both $t_{\hpred}$ and $t_{\vpred}$ are constants, or (ii) at least one term is not a constant. We argue each case accordingly.

(i) Observe that if both $t_{\hpred}$ and $t_{\vpred}$ are constants, then since $\mquery$ is properly marked, we know that $x \in M$ by <ref>. However, this contradicts our assumption that $x$ is maximal, and so, this case cannot occur.

(ii) In the alternative case, by the functionality of the Skolem chase (see <ref>), the fact that our rule set is $\rsgrid$, and since one term maps to a null in $\sg$ via $h$, we know that the (grid) rule must have been applied for $\hpred(h(t_{\hpred}),h(x))$ and $\vpred(h(t_{\vpred}),h(x))$ to occur in $\sg$. It follows that for some term $t$, $\hpred(t,h(t_{\vpred}))$ and $\vpred(t,h(t_{\hpred}))$ must occur in $\sg$. Let us define the homomorphism $h'$ such that $h'(s) = h(s)$ for each term $s \neq x$ in $\query$ and $h'(x') = t$. Then, we have that $\sg \models \query'$. Note that if $t$ is a null, then $\sg \models Q_{1}$ and if $t$ is a constant, then $\sg \models Q_{2}$, thus showing the desired conclusion.

Let us now show the backward direction and assume that there exists an $i \in \{1,2\}$ such that $\sg \models \mquery_{i}$. We have that $\sg \models \query'$, meaning that there exists a homomorphism $h$ mapping $\query'$ into $\sg$. Due to the fact that $\reduceop$ was applied, it follows that there exist atoms $\hpred(x',t_{\vpred})$ and $\vpred(x',t_{\hpred})$ in $\query'$ that are mapped into $\sg$, that is to say, $\hpred(h(x'),h(t_{\vpred})),\vpred(h(x'),h(t_{\hpred})) \in \sg$. By the (grid) rule and the functionality of the Skolem chase, there exists a null $y$ such that $\hpred(h(t_{\hpred}),y),\vpred(h(t_{\vpred}),y) \in \sg$. Let us define the homomorphism $h'$ such that $h'(s) = h(s)$ for all terms $s \neq x'$ in $\query'$ and $h'(x) = y$. Then, $h'$ is a homomorphism from $\query$ to $\sg$ and it is straightforward to show that for all terms $t'$ in $\query$, $t' \in M$ $h'(t')$ maps to a constant in $\sg$.

<ref>[Soundness — $\mergeop$]
Let $\db$ be a database and let $\mquery$ be an alive CQ. If $x, t$, and $t'$ are as in <ref>, then

$$\sg \models \mquery \ \text{\iffi} \ \sg \models \mergeop(\mquery, \set{x, t, t'}).$$

Let $Q = (\query,M)$, $\mergeop(\mquery, \set{x, t, t'}) = (\query',M )$, $\rpred \in \{\hpred, \vpred\}$, and $\query' = \query'' \cup \{\top(t)\}$.

For the forward direction, assume that $\sg \models \mquery$. It follows that there exists a homomorphism $h$ such that $h$ maps $\query$ into $\sg$ and for all terms $s$ in $\query$, $s \in M$ $h(s)$ is a constant in $\sg$. Also, since $\mergeop$ was applied, we know that there are at least two terms $t \neq t'$ such that $\rpred(t,x)$ and $\rpred(t',x)$ are in $\query$ and that $t'$ was substituted for $t$ in $\query$ to obtain $\query'$. Hence, $\rpred(h(t),h(x)), \rpred(h(t'),h(x)) \in \sg$, however, since we are using rules from $\rsgrid$ and by the functionality of the Skolem chase (see <ref>), it must be the case that either (i) $h(t)$, $h(x)$, and $h(t')$ all occur in $\db$, or (ii) $h(t) = h(x) = h(t') = y$ with $y$ the null generated by the (loop) rule. In case (i), $h(x)$ will be a constant as all terms of $\db$ are constants, meaning that $x$ will not be maximal, in contradiction to our assumption. Let us consider case (ii) then.
Note that in case (ii), the entire connected component of $\query$ containing $t$, $x$, and $t'$ is mapped to $y$ via $h$, meaning that the entire connected component of $\query'$ containing $x$ and $t'$ will be mapped to $y$ via $h$ as well. If we restrict our attention to the remaining connected components of $\query'$, then we can see that $h$ maps all such components homomorphically into $\sg$, showing that $h$ serves a homomorphism from $\query'$ to $\sg$. Last, we must show that for all terms $s'$ in $\query'$, $s' \in M$ $h(s')$ is a constant in $\sg$, however, this follows from the fact that $\query$ and $\query'$ have the same set of terms.

For the backward direction, suppose that $\sg \models \mergeop(\mquery, \set{x, t, t'})$. Then, there exists a homomorphism $h$ such that $h$ maps $\query'$ into $\sg$ and for all terms $s$ in $\query'$, $s \in M$ $h(s)$ is a constant in $\sg$. In addition, as $\mergeop$ was applied, there are at least two terms $t \neq t'$ such that $\rpred(t,x)$ and $\rpred(t',x)$ are in $\query$ with $t'$ substituted for $t$ in $\query$ to obtain $\query'$. Let us define a homomorphism $h'$ such that $h'(s) = s$ for all terms $s \neq t$ and $h'(t) = t'$. Then, $h'$ is a homomorphism from $\query$ to $\query'$, and since $h$ is a homomorphism from $\query'$ to $\sg$, we have that $h \circ h'$ is a homomorphism from $\query'$ to $\sg$. To finish the proof of the backward direction, we need to show that for all terms $s'$ in $\query$, $s' \in M$ $(h \circ h')(s')$ is a constant in $\sg$.

Let $s'$ be a term in $\query$. Suppose that $s' \in M$. Then, if $s' \neq t$, we have that $h(s')$ is a constant in $\sg$, and since $h(s') = (h \circ h')(s')$, it follows that $(h \circ h')(s')$ is a constant in $\sg$. If $s' = t$, then by <ref>, $t' \in M$, from which it follows that $h(t') = (h \circ h')(t)$ is a constant in $\sg$. Let us now suppose that $(h \circ h')(s')$ is a constant in $\sg$. If $s' \neq t$, then $(h \circ h')(s') = h(s')$ is a constant in $\sg$, implying that $s' \in M$; however, if $s' = t$, then $(h \circ h')(s') = (h \circ h')(t) = h(t')$ is a constant in $\sg$, implying that $t' \in M$, so by <ref>, $t \in M$ as well.