---
author:
- |
    JAMES BAILEY,\
    The University of Melbourne
- |
    GUOZHU DONG,\
    Wright State University
- |
    ANTHONY WIDJAJA TO\
    University of Edinburgh
bibliography:
- 'mvq.bib'
title: 'Logical Queries over Views: Decidability and Expressiveness[^1]'
---

Introduction
============

The study of views in relational databases has attracted much attention over the years.  Views are an indispensable component for activities such as data integration and data warehousing [@Wid95; @GQPRS95; @LRO96], where they can be used as “mediators” for source information that is not directly accessible to users.  This is especially helpful in modelling the integration of data from diverse sources, such as legacy systems and/or the world wide web. 

Much of the research related to views has addressed fundamental problems such as containment and rewriting/optimisation of queries using views (e.g. see [@U97; @Levy01]).  In this paper, we examine the use of views in a somewhat different context, where they are used as the basic unit for writing logical expressions.  We provide results on the related decision problem in this paper, for a range of possible view definitions.  In particular, for the case where views are monadic/unary conjunctive queries, we show that the corresponding query logic is decidable.  This corresponds to an interesting new fragment of first order logic.  On the application side, this decidable query language also has some interesting potential applications for areas such as implication of complex dependencies, ontology reasoning and termination results for active rules. 

Informal Statement of the Problem
---------------------------------

Consider a relational vocabulary $R_1, \ldots, R_p$ and a set of views $V_1, \ldots , V_n$. Each view definition corresponds to a first order formula over the vocabulary.  Some example views (using horn clause style notation) are

$V_1(x_1,y_1) \leftarrow R_1(x_1,y_1), R_2(y_1,y_1,z_1), R_3(z_1,z_2,x_1), R_4(z_2,x_1)$\
$V_2(z_1) \leftarrow R_1(z_1,z_1)$

Each such view can be expanded into to a first order sentence, e.g. $V_1(x_1,y_1) \Leftrightarrow \exists z_1,z_2 (R_1(x_1,y_1) \wedge
R_2(y_1,y_1,z_1), R_3(z_1,z_2,x_1) \wedge \neg R_4(z_2,x_1))$. A [*first order view query*]{} is a first order formula expressed [*solely*]{} in terms of the given views.  e.g. $q_1=\exists x_1,y_1
((V_1(x_1,y_1) \vee V_1(y_1,x_1)) \wedge \neg V_2(x_1)) \wedge
\forall z_1 (V_2(z_1) \Rightarrow V_1(z_1,z_1))$ is an example first order view query, but $q_2=\exists x_1,y_1 (V_1(x_1,y_1) \vee
R(y_1,x_1))$ is not.  By expanding the view definitions, every first order view query can clearly be re-written to eliminate the views.  Hence, first order view queries can be thought of as a fragment of first order logic, with the exact nature of the fragment varying according to how expressive the views are permitted to be. 

From a database perspective, first order view queries are particularly suited to applications where the source data is unavailable, but summary data (in the form of views) is.  Since many database and reasoning languages are based on first order logic (or extensions thereof), this makes it a useful choice for manipulating the views. 

Our purpose in this paper is to determine, for what types of view definitions, satisfiability (over both finite and infinite models) is decidable for the language.  If views can be binary, then this language is clearly as powerful as first order logic over binary base relations, and hence undecidable (see [@BGG96]).  The situation becomes far more interesting, when we restrict the form that views may take — in particular, when their arity must be unary.  Such a restriction has the effect of constraining which parts of the underlying database can be “seen” by the view formula and also constrains how such parts may be connected. 

Contributions
-------------

The main contribution of this paper is the definition of a language called the [*first order unary conjunctive view language*]{} (${\ensuremath{\text{UCV}}}$) and a proof of its decidability.  As its name suggests, it uses unary arity views defined by conjunctive queries[^2].  We demonstrate that it is a maximal decidable class, in the sense that increasing the expressiveness of the view definitions results in undecidability.  Some interesting aspects of this decidability result are:

-   It is well known that first order logic solely over monadic relations is decidable [@lowenheim], but the extension to dyadic relations is undecidable [@BGG97].  The first order unary conjunctive view language can be seen as an interesting intermediate case between the two, since although only monadic predicates (views) appear in the query, they are intimately related to database relations of higher arity. 

-   The language is able to express some interesting properties, which might be applied to various kinds of reasoning over ontologies.  It can also be thought of as a powerful generalisation of unary inclusion dependencies [@CKV90].  Furthermore, it has an interesting characterisation as a decidable class of rules (triggers) for active databases. 

To briefly give a feel for this decidable language, we next provide some example unary conjunctive views and a first order unary conjunctive view query defined over them:

$V_1(x) \leftarrow R_1(x,y), R_2(y,z), R_3(z,x'), R_4(x',x)$\
$V_2(x) \leftarrow R_1(x,y), R_1(x,z), R_4(y,z) $\
$V_3(x) \leftarrow R_1(x,y), R_1(x,z), R_4(y,y), R_4(z,x) $\
$V_4(x) \leftarrow R_1(x,y), R_3(y,z), R_4(z,x'), R_4(x',y'), R_3(y',x) $\
$\exists x (V_2(x) \wedge \neg V_1(x)) \wedge \neg\exists y (V_3(y) \wedge \neg V_4(y))$

Paper Outline
-------------

The paper is structured as follows: Section \[sec:prelim\] defines the necessary preliminaries and background concepts.  Section \[sec:ucvdef\] presents the definition of the logic ${\ensuremath{\text{UCV}}}$. Section \[sec:decid\] is the core section of the paper, where the decidability result for the class ${\ensuremath{\text{UCV}}}$ is proved.  Section \[extend\] shows that extensions to the language, such as allowing negation, inequality or recursion in views, result in undecidability.  Section \[sec:app\] covers applications of the decidability results and then Section \[sec:expressive\] provides some results on expressivity.  Section \[sec:related\] discusses related work and section \[sec:summary\] summarises and discusses future work. 

Preliminaries {#sec:prelim}
=============

In this section, we state basic definitions and relevant results.  The reader is assumed to be familiar with standard results and notations from mathematical logic (e.g. see [@End2001]).  In the following, formulas are always first-order.  The symbol ${\ensuremath{{\ensuremath{\mathcal{FO}}}}}$ denotes the set of first order formulas over any vocabulary $\sigma$. In addition, if ${\ensuremath{\mathcal{L}}} \subseteq {\ensuremath{{\ensuremath{\mathcal{FO}}}}}$ (i.e. ${\ensuremath{\mathcal{L}}}$ is a fragment of ${\ensuremath{{\ensuremath{\mathcal{FO}}}}}$), we denote by ${\ensuremath{\mathcal{L}}}(\sigma)$ the set of formulas in ${\ensuremath{\mathcal{L}}}$ over the vocabulary $\sigma$.

First-order logic
-----------------

A (relational) [vocabulary]{} $\sigma$ is a tuple $\langle R_1,\ldots,R_n
\rangle$ of relation symbols with each $R_i$ associated with a specified arity $r_i$. A (relational) $\sigma$-[structure]{} ${\ensuremath{\mbox{\textbf{{A}}}}}$ is the tuple $$\langle A; R_1^{{\ensuremath{\mbox{\textbf{{A}}}}}},\ldots,R_n^{{\ensuremath{\mbox{\textbf{{A}}}}}} \rangle$$ where $A$ is a non-empty set, called the [universe]{} (of ${\ensuremath{\mbox{\textbf{{A}}}}}$), and $R_i^{{\ensuremath{\mbox{\textbf{{A}}}}}}$ is an $r_i$-ary relation over $A$ interpreting $R_i$. We refer to the elements in the set $A$ as [the elements in ${\ensuremath{\mbox{\textbf{{A}}}}}$]{}, or simply by [constants]{}[^3] (of ${\ensuremath{\mbox{\textbf{{A}}}}}$).  In the sequel, we write $R_i$ instead of $R_i^{{\ensuremath{\mbox{\textbf{{A}}}}}}$ when the meaning is clear from the context.  We also use $STRUCT(\sigma)$ to denote the set of all $\sigma$-structures.  We assume a countably infinite set VAR of variables.  An [instantiation]{} (or [valuation]{}) of a structure ${\ensuremath{\mbox{\textbf{{{\ensuremath{\mbox{\textbf{I}}}}}}}}}$ is a function $v: \text{VAR}
{\ensuremath{\rightarrow}}I$. Extend this function to free tuples (i.e. tuple of variables) in the obvious way.  We use the usual Tarskian notion of satisfaction to define ${\ensuremath{\mbox{\textbf{I}}}}\models \phi[v]$, i.e., whether $\phi$ is true in ${\ensuremath{\mbox{\textbf{I}}}}$ under $v$. If $\phi$ is a sentence, we simply write ${\ensuremath{\mbox{\textbf{I}}}}\models \phi$. The [image]{} of a structure ${\ensuremath{\mbox{\textbf{I}}}}$ under a formula $\phi(x_1,\ldots,x_n)$ is $$\phi({\ensuremath{\mbox{\textbf{I}}}}) {\ensuremath{\overset{\mbox{\tiny def}}{=}}}\{ v(x_1,\ldots, x_n): \text{$v$ is an instantiation of
            {\ensuremath{\mbox{\textbf{I}}}}, and ${\ensuremath{\mbox{\textbf{I}}}}\models \phi[v]$} \}.$$ In particular, if $n = 0$, we have that $\phi({\ensuremath{\mbox{\textbf{I}}}}) \neq \emptyset$ iff ${\ensuremath{\mbox{\textbf{I}}}}\models \phi$. We say that two $\sigma$-structures ${\ensuremath{\mbox{\textbf{{A}}}}}$ and ${\ensuremath{\mbox{\textbf{{B}}}}}$ [*agree*]{} on ${\cal L}$ iff for all $\phi \in {\cal L}(\sigma)$ we have ${\ensuremath{\mbox{\textbf{{A}}}}} \models \phi \Leftrightarrow {\ensuremath{\mbox{\textbf{{B}}}}} \models \phi$.

Following the convention in database theory, the [(tuple) database ${\ensuremath{\mathcal{D}}}({\ensuremath{\mbox{\textbf{{A}}}}})$ corresponding to the structure ${\ensuremath{\mbox{\textbf{{A}}}}}$]{} (defined above) is the set $$\{ R_i(t) : \text{$1 \leq i \leq n$ and $t \in R_i^{{\ensuremath{\mbox{\textbf{{A}}}}}}$} \}.$$ It is easy to see that such a database can be considered a structure with universe $adom({\ensuremath{\mbox{\textbf{{A}}}}})$, which is defined to be the set of all elements of ${\ensuremath{\mbox{\textbf{{A}}}}}$ occurring in at least one relation $R_i$, and relations built appropriately from ${\ensuremath{\mathcal{D}}}({\ensuremath{\mbox{\textbf{{A}}}}})$. Abusing terminologies, we refer to the elements of ${\ensuremath{\mathcal{D}}}({\ensuremath{\mbox{\textbf{{A}}}}})$ as [tuples (associated with ${\ensuremath{\mbox{\textbf{{A}}}}}$)]{}.  In addition, when the meaning is clear from the context, we shall also abuse the term [free tuple]{} to mean an atomic formula $R(u)$, where $R \in \sigma$ and $u$ is a tuple of variables. 

A formula $\phi$ is said to be [satisfiable]{} if there exists a structure ${\ensuremath{\mbox{\textbf{{A}}}}}$ (either of finite or infinite size) such that $\phi({\ensuremath{\mbox{\textbf{{A}}}}}) \neq
\emptyset$; such a structure is said to be a [model]{} for $\phi$. We say that $\phi$ is [finitely satisfiable]{} if there exists a finite structure ${\ensuremath{\mbox{\textbf{I}}}}$ such that $\phi({\ensuremath{\mbox{\textbf{I}}}}) \neq \emptyset$. Without loss of generality, we shall focus only on sentences when we are dealing with the satisfiability problem.  In fact, if $\phi$ has some free variables, taking its existential closure preserves satisfiability \[Indeed we shall see that the languages we consider are closed under first-order quantification\]. 

Given two $\sigma$-structures ${\ensuremath{\mbox{\textbf{{A}}}}}, {\ensuremath{\mbox{\textbf{{B}}}}}$, recall that ${\ensuremath{\mbox{\textbf{{A}}}}}$ is a [substructure]{} of ${\ensuremath{\mbox{\textbf{{B}}}}}$ (written ${\ensuremath{\mbox{\textbf{{A}}}}} {\ensuremath{\subseteq}}{\ensuremath{\mbox{\textbf{{B}}}}}$) if $A \subseteq B$ and $R^{{\ensuremath{\mbox{\textbf{{A}}}}}} \subseteq R^{{\ensuremath{\mbox{\textbf{{B}}}}}}$ for every relation symbol $R$ in $\sigma$. We say that ${\ensuremath{\mbox{\textbf{{A}}}}}$ is an [induced]{} substructure of ${\ensuremath{\mbox{\textbf{{B}}}}}$ (i.e. [induced]{} by $A
\subseteq B$) if for every relation symbol $R$ in $\sigma$, $R^{{\ensuremath{\mbox{\textbf{{A}}}}}} = R^{{\ensuremath{\mbox{\textbf{{B}}}}}} \cap A^r$, where $r$ is the arity of $R$. Now, a [homomorphism]{} from [$\mbox{\textbf{{A}}}$]{} to [$\mbox{\textbf{{B}}}$]{} is a function $h: A {\ensuremath{\rightarrow}}B$ such that, for every relation symbol $R$ in $\sigma$ and ${\ensuremath{\mbox{\textbf{{a}}}}} = (a_1,\ldots,a_r) \in R^{{\ensuremath{\mbox{\textbf{{A}}}}}}$, it is the case that $h({\ensuremath{\mbox{\textbf{{a}}}}}) {\ensuremath{\overset{\mbox{\tiny def}}{=}}}(h(a_1),\ldots,h(a_r)) \in R^{{\ensuremath{\mbox{\textbf{{B}}}}}}$. An [isomorphism]{} is a bijective homomorphism whose inverse is a homomorphism. 

The [quantifier rank]{} ${\ensuremath{\mbox{qrank}}}(\phi)$ of of a formula $\phi$ is the maximum nesting depth of quantifiers in $\phi$.

Views
-----

For our purpose, a [view]{} over $\sigma$ can be thought of as an arbitrary FO formula over $\sigma$. We say that a view $V$ is [conjunctive]{} if it can be written as a [conjunctive query]{}, i.e. of the form $$\exists x_1,\ldots,x_n( R_1(u_1) \wedge \ldots \wedge R_k(u_k) )$$ where each $R_i$ is a relation symbol, and each $u_i$ is a [free tuple]{} of appropriate arity.  We adopt the horn clause style notation for writing conjunctive views.  For example, if $\{y_1,\ldots,y_n\}$ is the set of free variables in the above conjunctive query, then we can rewrite it as $$V(y_1,\ldots,y_n) {\ensuremath{\leftarrow}}R_1(u_1), \ldots, R_k(u_k)$$ where $V(y_1, \ldots, y_n)$ is called the [head]{} of $V$, and the conjunction $R_1(u_1), \ldots, R_k(u_k)$ the [body]{} of $V$. The [length]{} of the conjunctive view $V$ is defined to be the sum of the arities of the relation symbols in the *multiset* $\{R_1,\ldots,R_k\}$. For example, the lengths of the two views $V$ and $V'$ defined as $$\begin{aligned}
    V(x) & {\ensuremath{\leftarrow}}& E(x,y) \\
    V'(x) & {\ensuremath{\leftarrow}}& E(x,y), E(y,z)\end{aligned}$$ are, respectively, two and four.  Additionally, if $n = 1$ (i.e. has a head of arity 1), the view is said to be unary. [* Unless stated otherwise, we shall say “view” to mean “unary-conjunctive view with neither equality nor negation in its body”*]{}. 

Graphs
------

We use standard definitions from graph theory (e.g. see [@Dies05]).  A [graph]{} is a structure ${\ensuremath{{\ensuremath{\mbox{\textbf{{G}}}}}}}= (G,E)$ where $E$ is a binary relation.  The [girth]{} of a graph is the length of its shortest cycle.  For two vertices $x,y \in G$, we denote their distance by $d_{{\ensuremath{{\ensuremath{\mbox{\textbf{{G}}}}}}}}(x,y)$ (or just $d(x,y)$ when ${\ensuremath{{\ensuremath{\mbox{\textbf{{G}}}}}}}$ is clear from the context).  For two sets $S_1$ and $S_2$ of vertices in ${\ensuremath{{\ensuremath{\mbox{\textbf{{G}}}}}}}$, we define their distance to be $$d_{{\ensuremath{{\ensuremath{\mbox{\textbf{{G}}}}}}}}(S_1,S_2) := \min\{ d_{{\ensuremath{{\ensuremath{\mbox{\textbf{{G}}}}}}}}(a,b) : \text{$a \in S_1$ and
                            $b \in S_2$} \}.$$ In a weighted graph ${\ensuremath{{\ensuremath{\mbox{\textbf{{G}}}}}}}$ with weight $w_{{\ensuremath{{\ensuremath{\mbox{\textbf{{G}}}}}}}}: E {\ensuremath{\rightarrow}}\mathbb{N}$, the weight $w_{{\ensuremath{{\ensuremath{\mbox{\textbf{{G}}}}}}}}(P)$ of a path $P$ in ${\ensuremath{{\ensuremath{\mbox{\textbf{{G}}}}}}}$ is just $\sum_{e \in E(P)}
w_{{\ensuremath{{\ensuremath{\mbox{\textbf{{G}}}}}}}}(e)$. We shall write $w$ instead of $w_{{\ensuremath{{\ensuremath{\mbox{\textbf{{G}}}}}}}}$ if the meaning is clear from the context.  In the sequel, we shall frequently mention trees and forests.  We always assume that any tree has a selected node, which we call a [root]{} of the tree.  Given a tree ${\ensuremath{{\ensuremath{\mbox{\textbf{{T}}}}}}}= (T,E)$, we can partition $T$ according to the distance of the vertices from the root. 

The [Gaifman graph]{} (see [@Gai82]) associated with a structure ${\ensuremath{\mbox{\textbf{{A}}}}}$ is the weighted undirected multi-graph ${\ensuremath{\Bbb{G}}}({\ensuremath{\mbox{\textbf{{A}}}}}) =
(G,E)$ such that:

1.   $G = A$. 

2.   The multi-set $E$ is defined as follows: for each $x,y \in G$, we put an $R(t)$-labeled edge $xy$ in $E$ with weight $r$ (the arity of $R$) iff $x$ and $y$ appear in a tuple $R(t)$ in ${\ensuremath{\mathcal{D}}}({\ensuremath{\mbox{\textbf{{A}}}}})$. \[Notice that the multiplicity of $xy$ in $E$ depends on the number of tuples in ${\ensuremath{\mathcal{D}}}({\ensuremath{\mbox{\textbf{{A}}}}})$ that contain both $x$ and $y$ as their arguments.\]

Note also that the subgraph of ${\ensuremath{\Bbb{G}}}({\ensuremath{\mbox{\textbf{{A}}}}})$ induced by the set of all elements of ${\ensuremath{\mbox{\textbf{{A}}}}}$ in a tuple $t$ is the complete graph $K_r$, and so an $L$-labelled edge is adjacent to an edge $e \in E$ iff all $L$-labelled edges are adjacent (i.e. connected) to the edge $e$. For any $a,b \in A$, we define the [distance]{} $d_{{\ensuremath{\mbox{\textbf{{A}}}}}}(a,b)$ between $a$ and $b$ to be their distance in ${\ensuremath{\Bbb{G}}}({\ensuremath{\mbox{\textbf{{A}}}}})$. Also, extend this distance function to tuples and sets of tuples by interpreting them as sets of elements of ${\ensuremath{\mbox{\textbf{{A}}}}}$ that appear in them.  Any pair of tuples $R(t)$ and $R'(t')$ in ${\ensuremath{\mathcal{D}}}({\ensuremath{\mbox{\textbf{{A}}}}})$ are said to be [connected]{} (in ${\ensuremath{\mbox{\textbf{{A}}}}}$) if in ${\ensuremath{\Bbb{G}}}({\ensuremath{\mbox{\textbf{{A}}}}})$ some (and hence all) $R(t)$-labeled edge is adjacent to some (and hence all) $R'(t')$-labeled edge. 

Unary formulas
--------------

A [unary formula]{} is an arbitrary FO formula *without equality* such that each of its relation symbols has arity one.  Let $\sigma$ be a vocabulary whose relation symbols are of arity one.  We shall use ${\ensuremath{\text{UFO}}}(\sigma)$ to denote the set of all unary formulas without equality over $\sigma$. Also, we define ${\ensuremath{\text{UFO}}}= \cup_{\sigma} {\ensuremath{\text{UFO}}}(\sigma)$. The following lemma will be useful for proving expressiveness results in Section \[sec:expressive\]. 

For every unary sentence, there exists an equivalent one of quantifier rank 1.  \[lm:unaryform\]

By a straightforward manipulation.  See the proof of lemma 21.12 in [@BBJ2002].  \[Their proof actually gives more than the result they claim.  In fact, their construction converts an arbitrary unary sentence into one with one unary variable and of quantifier rank 1.\]

Ehrenfeucht-Fraïsse Games
-------------------------

We shall need a limited form of Ehrenfeucht-Fraïsse games; for a general account, the reader may consult [@Libkin2004].  The games are played by two players, Spoiler and Duplicator, on two $\sigma$-structures ${\ensuremath{\mbox{\textbf{{A}}}}}$ and ${\ensuremath{\mbox{\textbf{{B}}}}}$. The goal of Spoiler is to show that the structures are different, while Duplicator aims to show that they are the same.  The game consists of a single round.  Spoiler chooses a structure (say, ${\ensuremath{\mbox{\textbf{{A}}}}}$) and an element $a$ in it, after which Duplicator has to respond by choosing an element $b$ in the other structure ${\ensuremath{\mbox{\textbf{{B}}}}}$. Duplicator wins the game iff the substructure of ${\ensuremath{\mbox{\textbf{{A}}}}}$ induced by $\{a\}$ is isomorphic to the substructure of ${\ensuremath{\mbox{\textbf{{B}}}}}$ induced by $\{b\}$. Duplicator has a winning strategy iff Duplicator has a winning move, regardless of how Spoiler behaves. 

Duplicator has a winning strategy on ${\ensuremath{\mbox{\textbf{{A}}}}}$ and ${\ensuremath{\mbox{\textbf{{B}}}}}$ iff ${\ensuremath{\mbox{\textbf{{A}}}}}$ and ${\ensuremath{\mbox{\textbf{{B}}}}}$ agree on first-order formulas over $\sigma$ of quantifier rank 1. 

Other Notation
--------------

Regarding other notation we shall use throughout the rest of the paper: we shall use $a,b$ for constants, $x,y,z$ for variables, $u$ for free tuples, $U,V$ for views, ${\ensuremath{\mathcal{U}}},
{\ensuremath{\mathcal{V}}}$ for sets of views, $\sigma$ for vocabularies, $R_1, R_2,\ldots$ for relation symbols, ${\ensuremath{\mbox{\textbf{{A}}}}}, {\ensuremath{\mbox{\textbf{{B}}}}},\ldots$ for structures and $A,B$ for their respective universes.  If ${\ensuremath{\mathcal{D}}}$ is a database (a set of tuples), we use $adom({\ensuremath{\mathcal{D}}})$ to denote the set of constants in ${\ensuremath{\mathcal{D}}}$. Finally, given a $a \in adom({\ensuremath{\mathcal{D}}})$ and a “new” constant $b \notin {\ensuremath{\mathcal{D}}}$, we define ${\ensuremath{\mathcal{D}}}[b/a]$ to be the database that is obtained from ${\ensuremath{\mathcal{D}}}$ by replacing every occurrence of $a$ by $b$. The notation ${\ensuremath{\mathcal{D}}}[b_1/a_1,\ldots,b_n/a_n]$ is defined in the same way. 

Definition of First Order Unary-conjunctive-view Logic {#sec:ucvdef}
======================================================

Let $\sigma$ be an arbitrary vocabulary, and ${\ensuremath{\mathcal{V}}}$ be a finite set of (unary conjunctive) views over $\sigma$, which we refer to as a [$\sigma$-view set]{}.  We now inductively define the set ${\ensuremath{\text{UCV}}}(\sigma,{\ensuremath{\mathcal{V}}})$ of [first order unary-conjunctive-view (UCV) queries/formulas over the vocabulary $\sigma$ and a $\sigma$-view set ${\ensuremath{\mathcal{V}}}$]{}:

1.   if $V \in {\ensuremath{\mathcal{V}}}$, then $V(x) \in {\ensuremath{\text{UCV}}}(\sigma,{\ensuremath{\mathcal{V}}})$; and

2.   if $\phi, \psi \in {\ensuremath{\text{UCV}}}(\sigma,{\ensuremath{\mathcal{V}}})$, then the formulas $\neg \phi, \phi \wedge \psi$ and $\exists x\phi$ belong to ${\ensuremath{\text{UCV}}}(\sigma,{\ensuremath{\mathcal{V}}})$.

The smallest set of so-constructed formulas defines the set ${\ensuremath{\text{UCV}}}(\sigma,{\ensuremath{\mathcal{V}}})$. We denote the set of all UCV formulas over the vocabulary $\sigma$ by ${\ensuremath{\text{UCV}}}(\sigma)$, i.e. ${\ensuremath{\text{UCV}}}(\sigma) {\ensuremath{\overset{\mbox{\tiny def}}{=}}}\bigcup_{{\ensuremath{\mathcal{V}}}} {\ensuremath{\text{UCV}}}(\sigma,{\ensuremath{\mathcal{V}}})$ where ${\ensuremath{\mathcal{V}}}$ may be any $\sigma$-view set.  Further, the set of all UCV queries is denoted by ${\ensuremath{\text{UCV}}}$, i.e. ${\ensuremath{\text{UCV}}}{\ensuremath{\overset{\mbox{\tiny def}}{=}}}\bigcup_{\sigma} {\ensuremath{\text{UCV}}}(\sigma)$, where $\sigma$ is any vocabulary.  As usual, we use the shorthands $\phi \vee \psi$, $\phi {\ensuremath{\rightarrow}}\psi$, $\phi {\ensuremath{\leftrightarrow}}\psi$, and $\forall x\phi$ for (respectively) $\neg (\neg \phi \wedge \neg \psi), \neg \phi \vee \psi,
(\phi {\ensuremath{\rightarrow}}\psi) \wedge (\psi {\ensuremath{\rightarrow}}\phi)$, and $\neg \exists x \neg \phi$. Thus, the UCV language is closed under boolean combinations and first-order quantifications.  As an example, consider the UCV formula $$q_1 = \exists x( V(x) \wedge \neg V'(x) )$$ where $V$ and $V'$ are defined as $$\begin{aligned}
    V(x) & {\ensuremath{\leftarrow}}& E(x,y) \\
    V'(x) & {\ensuremath{\leftarrow}}& E(x,y), E(y,z) \\\end{aligned}$$ This formula asserts that there exists a vertex from which there is an outgoing arc, but no outgoing directed walk of length 2. 

Let us make a few remarks on the expressive power of the logic ${\ensuremath{\text{UCV}}}$ with respect to other logics.  It is easy to see that the UCV language strictly subsumes [$\text{UFO}$]{}$\;$ (the Löwenheim class without equality [@lowenheim; @BGG97]), as UCV queries can be defined over *any* relational vocabularies (i.e. including ones that include $k$-ary relation symbols with $k >
1$).  It is also easy to see that allowing any general existential positive formula (i.e. of the form $\exists\overline{x}\phi(\overline{x})$ where $\phi$ is a quantifier-free formula with no negation) with one free variable, does not increase the expressive power of the logic.  Indeed, the quantifier-free subformula $\phi$ can be rewritten in disjunctive normal form without introducing negation, after which we may distribute the existential quantifier across the disjunctions and consequently transform entire formula to a disjunction of conjunctive queries with one or zero free variables.  Each such conjunctive query can then be treated as a view. 

There are two ways in which we can interpret a UCV formula.  The standard way is to think of a UCV query as an FO formula over the underlying vocabulary.  Take the afore-mentioned query $q_2$ as an example.  We can interpret this query as the formula $$\exists x( \exists y,z(E(x,y) \wedge E(y,z)) \wedge \neg \exists y(E(x,y) )$$ over the graph vocabulary.  The non-standard way is to regard a UCV query $\phi$ as a unary formula over the view set.  For example, we can think of $q_2$ as a unary formula over the vocabulary $\sigma' = \langle V,V' \rangle$. Now, if $\phi \in {\ensuremath{\text{UCV}}}(\sigma,{\ensuremath{\mathcal{V}}})$, then we denote by $\phi^{{\ensuremath{\mathcal{V}}}}$ the unary formula over ${\ensuremath{\mathcal{V}}}$ corresponding to $\phi$ in the non-standard interpretation of UCV queries.  However, for notational convenience, we shall write $\phi$ instead of $\phi^{{\ensuremath{\mathcal{V}}}}$ when the meaning is clear from the context.  Given a vocabulary $\sigma$ and a $\sigma$-view set ${\ensuremath{\mathcal{V}}} = \{V_1,\ldots,V_n\}$, we may define the function $\Lambda: STRUCT(\sigma) {\ensuremath{\rightarrow}}STRUCT({\ensuremath{\mathcal{V}}})$ such that for any ${\ensuremath{\mbox{\textbf{I}}}}\in STRUCT(\sigma)$ $$\Lambda({\ensuremath{\mbox{\textbf{I}}}}) {\ensuremath{\overset{\mbox{\tiny def}}{=}}}\langle I; V_1^{\Lambda({\ensuremath{\mbox{\textbf{I}}}})}, \ldots,
                    V_n^{\Lambda({\ensuremath{\mbox{\textbf{I}}}})} \rangle$$ where $V_i^{\Lambda({\ensuremath{\mbox{\textbf{I}}}})} {\ensuremath{\overset{\mbox{\tiny def}}{=}}}V_i({\ensuremath{\mbox{\textbf{I}}}})$. For example, let $\sigma = \langle E \rangle$ and ${\ensuremath{\mathcal{V}}} = \{V,V'\}$ be as above, and let $${\ensuremath{\mbox{\textbf{I}}}}= \langle \{1,2,3,4\}; E^{{\ensuremath{\mbox{\textbf{I}}}}} = \{(1,2),(2,3),(3,4)\} \rangle.$$ Then, we have $${\ensuremath{\mbox{\textbf{J}}}}{\ensuremath{\overset{\mbox{\tiny def}}{=}}}\Lambda({\ensuremath{\mbox{\textbf{I}}}}) = \langle \{1,2,3,4\}, V^{{\ensuremath{\mbox{\textbf{J}}}}} = \{1,2,3\},
                V'^{{\ensuremath{\mbox{\textbf{J}}}}} = \{1,2\} \rangle.$$ In the following, we shall reserve the symbol $\Lambda$ to denote this special function.  In addition, if ${\ensuremath{\mbox{\textbf{J}}}}\in STRUCT({\ensuremath{\mathcal{V}}})$ and there exists a structure ${\ensuremath{\mbox{\textbf{I}}}}\in STRUCT(\sigma)$ such that $\Lambda({\ensuremath{\mbox{\textbf{I}}}}) =
{\ensuremath{\mbox{\textbf{J}}}}$, we say that the structure ${\ensuremath{\mbox{\textbf{J}}}}$ is [realizable]{} with respect to the vocabulary $\sigma$ and the view set ${\ensuremath{\mathcal{V}}}$, or that ${\ensuremath{\mbox{\textbf{I}}}}$ [realizes]{} ${\ensuremath{\mbox{\textbf{J}}}}$. We shall omit mention of $\sigma$ and ${\ensuremath{\mathcal{V}}}$ if they are understood by context. 

A number of remarks about the notion of realizability are in order.  First, some unary structures are *not* realizable with respect to a given view set ${\ensuremath{\mathcal{V}}}$. For example, the query $q_2$ has infinitely many models if treated as a unary formula, but none of these models are realizable, since $V' \subseteq V$. Second, if $\phi \in {\ensuremath{\text{UCV}}}(\sigma,{\ensuremath{\mathcal{V}}})$ has a model ${\ensuremath{\mbox{\textbf{I}}}}$, then the structure $\Lambda({\ensuremath{\mbox{\textbf{I}}}})$ over ${\ensuremath{\mathcal{V}}}$ is a model for $\phi^{{\ensuremath{\mathcal{V}}}}$. In other words, if a UCV query is satisfiable, then it is also satisfiable if treated as a unary formula.  Conversely, it is also clearly true that a UCV query is satisfiable, if it is satisfiable when treated as a unary formula and that at least one of its models is realizable.  More precisely, if $\Lambda({\ensuremath{\mbox{\textbf{I}}}})$ is a model for $\phi^{{\ensuremath{\mathcal{V}}}}$, then ${\ensuremath{\mbox{\textbf{I}}}}$ is a model for $\phi$. So, combining these, we have $I \models \phi$ iff $\Lambda(I) \models \phi^{{\ensuremath{\mathcal{V}}}}$. So, we immediately have the following lemma:

Suppose ${\ensuremath{\mbox{\textbf{{A}}}}}, {\ensuremath{\mbox{\textbf{{B}}}}} \in STRUCT(\sigma)$ and $\phi \in {\ensuremath{\text{UCV}}}(\sigma,{\ensuremath{\mathcal{V}}})$. Then, for $\Lambda: STRUCT(\sigma) {\ensuremath{\rightarrow}}STRUCT({\ensuremath{\mathcal{V}}})$ defined above, the following statements are equivalent:

1.   ${\ensuremath{\mbox{\textbf{{A}}}}} \models \phi$ iff ${\ensuremath{\mbox{\textbf{{B}}}}} \models \phi$,

2.   $\Lambda({\ensuremath{\mbox{\textbf{{A}}}}}) \models \phi^{\Lambda}$ iff $\Lambda({\ensuremath{\mbox{\textbf{{B}}}}}) \models
            \phi^{\Lambda}$.

\[lem:realize\]

This lemma is useful when combined with Ehrenfeucht-Fraïsse games.  For example, suppose that we are given a model ${\ensuremath{\mbox{\textbf{{A}}}}}$ for $\phi$, and we construct a “nicer” structure ${\ensuremath{\mbox{\textbf{{B}}}}}$ that, we wish, satisfies $\phi$. If we can prove that the second statement in the lemma (which is often easier to establish as views have arity one), we might deduce that ${\ensuremath{\mbox{\textbf{{B}}}}} \models \phi$.

Decidability of UCV Queries {#sec:decid}
===========================

In this section, we prove our main result that satisfiability is decidable for ${\ensuremath{\text{UCV}}}$ formulas.  Our main theorem stipulates that ${\ensuremath{\text{UCV}}}$ has the bounded model property. 

\[th:fin\_s\] Let $\phi$ be a formula in ${\ensuremath{\text{UCV}}}$. Suppose, further, that $\phi$ contains precisely the views in the view set ${\ensuremath{\mathcal{V}}}$, and relation symbols in the vocabulary $\sigma$, with $m$ being the maximum length of the views in ${\ensuremath{\mathcal{V}}}$, and $p = |\sigma|$. If $\phi$ is satisfiable, then it has a model using at most $2^{2^{q(p,m)}}$ elements, for some fixed polynomial $q$ in $p$ and $m$.

Before we prove this theorem, we first derive some corollaries.  Simple algebraic manipulations yield the following corollary. 

Continuing from Theorem \[th:fin\_s\], if $n$ is the size of (the parse tree of) a satisfiable formula $\phi$, then $\phi$ has a model of size $2^{2^{g(n)}}$ for some fixed polynomial $g$ in $n$. \[th:fin\_s2\]

Corollary \[th:fin\_s2\] immediately leads to the decidability of satisfiability for ${\ensuremath{\text{UCV}}}$. We can in fact derive a tighter bound. 

Satisfiability for the ${\ensuremath{\text{UCV}}}$ class of formulas is in 2-NEXPTIME.  \[th:timecomp\]

This theorem follows immediately from the following proposition and corollary \[th:fin\_s2\]. 

Let $s$ be a non-decreasing function with $s(n) \geq n$. Then, the problem of determining whether an FO sentence has a model of size at most $s(n)$, where $n$ is the size of the input formula, can be decided nondeterministically in $2^{O(n \log(s(n)))}$ steps.  \[prop:timecomp\]

We may use any reasonable encoding ${\ensuremath{\text{code}}}({\ensuremath{\mbox{\textbf{{A}}}}})$ of a finite structure ${\ensuremath{\mbox{\textbf{{A}}}}}$ in bits (e.g. see [@Libkin2004 Chapter 6]).  The size of the encoding, denoted $|{\ensuremath{\mbox{\textbf{{A}}}}}|$, is polynomial in $|A|$. We first guess a structure ${\ensuremath{\mbox{\textbf{{A}}}}}$ of size at most $s(n)$. Let $s' = |A|$. Since the size $|{\ensuremath{\mbox{\textbf{{A}}}}}|$ of the encoding of ${\ensuremath{\mbox{\textbf{{A}}}}}$ is polynomial in $s'$, the guessing procedure takes $O(s^k(n))$ time steps for some constant $k$. We, then, use the usual procedure for evaluating whether ${\ensuremath{\mbox{\textbf{{A}}}}} \models \phi$. This can be done in $O(n \times |{\ensuremath{\mbox{\textbf{{A}}}}}|^n)$ steps (e.g. see [@Libkin2004 Proposition 6.6]).  Simple algebraic manipulations give the sought after upper bound. 

Observe that a lower bound for satisfiability of ${\ensuremath{\text{UCV}}}$ formulas follows immediately from the NEXPTIME completeness for satisfiability of [$\text{UFO}$]{}$\;$ formulas given in [@BGG97]

Satisfiability for the ${\ensuremath{\text{UCV}}}$ class of formulas is NEXPTIME hard. 

What remains now is to prove theorem \[th:fin\_s\]. 

Let $\phi, m, p$ be as stated in theorem \[th:fin\_s\].  We begin by first enumerating all possible views over $\sigma$ of length at most $m$. As we shall see later in the proof of Subproperty \[subp:prune\], doing so will help facilitate the correctness of our construction of a finite model, since enumerating all such views effectively allows us to determine all possible ways the model may be “seen” by views, or parts of views.  Let ${\ensuremath{\mathcal{U}}} =
\{V_1,\ldots,V_N\}$ be the set of all non-equivalent views obtained.  By elementary counting, one may easily verify that $N \leq m(mp)^m$. Indeed, each view is composed of its head and its body, whose length is bounded by $m$. The body is a set of conjuncts that we may fix in some order.  There are at most $m$ variables that the head can take.  Each position in the body is a variable ($m$ choices) that is part of a relation $R$ ($p$ choices).  The upper bound is then immediate. 

Let ${\ensuremath{\mbox{\textbf{I}}}}_0$ be a (possibly infinite) model for $\phi$. \[If it is infinite, by the Löwenheim-Skolem theorem, we may assume that it is countable.\] Without loss of generality, we may assume that there exists a “universe” relation $U$ in ${\ensuremath{\mbox{\textbf{I}}}}_0$ which contains each constant in $adom({\ensuremath{\mbox{\textbf{I}}}}_0)$. Otherwise, if $U' \notin \sigma$ is a unary relation symbol, the $(\sigma \cup \{U'\})$-structure obtained by adding to ${\ensuremath{\mbox{\textbf{I}}}}_0$ the relation $U'$, which is to be interpreted as $I_0$, is also a model for $\phi$.

Let us now define $2^N$ formulas $C_0,\ldots,C_{2^{N}-1}$ of the form $$C_i(x) {\ensuremath{\overset{\mbox{\tiny def}}{=}}}(\neg) V_1(x) \wedge \ldots \wedge (\neg) V_N(x),$$ where the conjunct $V_j(x)$ is negated iff the $j$th bit of the binary representation of $i$ is 0.  For each ${\ensuremath{\mbox{\textbf{{A}}}}} \in STRUCT(\sigma)$, these formulas induce an equivalence relation on $A$ with each set $C_i({\ensuremath{\mbox{\textbf{{A}}}}})$ being an equivalence class.  When ${\ensuremath{\mbox{\textbf{{A}}}}}$ is clear, we refer to the equivalence class $C_i({\ensuremath{\mbox{\textbf{{A}}}}})$ simply as $C_i$. In addition, the existence of the universe relation $U$ in ${\ensuremath{\mbox{\textbf{I}}}}_0$ implies that the all-negative equivalence class $C_0$ is empty. 

We next describe a sequence of five satisfaction-preserving procedures for deriving a finite model from ${\ensuremath{\mbox{\textbf{I}}}}_0$. This sequence is best described diagrammatically: $${\ensuremath{\mbox{\textbf{I}}}}_0 \stackrel{\text{\tt makeJF}}{{\ensuremath{\longrightarrow}}}
    {\ensuremath{\mbox{\textbf{I}}}}_1 \stackrel{\text{\tt rename1}}{{\ensuremath{\longrightarrow}}}
    {\ensuremath{\mbox{\textbf{I}}}}_2 \stackrel{\text{\tt rename2}}{{\ensuremath{\longrightarrow}}}
    {\ensuremath{\mbox{\textbf{I}}}}_3 \stackrel{\text{\tt copy}}{{\ensuremath{\longrightarrow}}}
    {\ensuremath{\mbox{\textbf{I}}}}_4 \stackrel{\text{\tt prune}}{{\ensuremath{\longrightarrow}}}
    {\ensuremath{\mbox{\textbf{I}}}}_5.$$ The $i$th procedure above takes a structure ${\ensuremath{\mbox{\textbf{I}}}}_i$ as input, and outputs another structure ${\ensuremath{\mbox{\textbf{I}}}}_{i+1}$. The structure ${\ensuremath{\mbox{\textbf{I}}}}_5$ is guaranteed to be finite (and indeed bounded).  That each procedure preserves satisfiability immediately follows by subproperties \[subp:makeJHS\], \[subp:rename\], \[subp:maxim\], \[subp:copy\], and \[subp:prune\].  While reading the description of the procedures below, it is instructive to keep in mind that the property that $C_i({\ensuremath{\mbox{\textbf{I}}}}_j) = \emptyset$ iff $C_i({\ensuremath{\mbox{\textbf{I}}}}_{j+1}) = \emptyset$ is sufficient for showing that the $j$th procedure preserves satisfiability (see lemma \[lm:equiv\]). 

Roughly speaking, the procedure `makeJF` transforms the initially given structure ${\ensuremath{\mbox{\textbf{I}}}}_0$ into another structure that has a forest-like graphical representation, called a “justification forest”.  Each subsequent procedure works only on justification forests.  In the sequel, we shall use ${\ensuremath{\mathcal{H}}}_i$ to denote our graphical representation of ${\ensuremath{\mbox{\textbf{I}}}}_i$ ($i \in \{1,\ldots,5\}$). 

*The procedure `makeJF`*

We define the structure ${\ensuremath{\mbox{\textbf{I}}}}_1$ by first defining a sequence ${\ensuremath{\mbox{\textbf{I}}}}_1^0, {\ensuremath{\mbox{\textbf{I}}}}_1^1, \ldots$ of structures such that ${\ensuremath{\mbox{\textbf{I}}}}_1^k$ is a substructure of ${\ensuremath{\mbox{\textbf{I}}}}_1^{k+1}$, and then setting ${\ensuremath{\mbox{\textbf{I}}}}_1 =
\bigcup_{k=0}^{\infty} {\ensuremath{\mbox{\textbf{I}}}}_1^k$. \[Note: we take the normal union, not *disjoint union*.\] We first deal with the base case of ${\ensuremath{\mbox{\textbf{I}}}}_1^0$. For each non-empty equivalence class $C_i({\ensuremath{\mbox{\textbf{I}}}}_0)$, we choose a witnessing constant $a_i \in C_i({\ensuremath{\mbox{\textbf{I}}}}_0)$. We define $I_1^0$ as the collection of all such $a_i$s.  All relations in ${\ensuremath{\mbox{\textbf{I}}}}_1^0$ are empty.  Each $a_i$ is said to be [unjustified]{} in ${\ensuremath{\mbox{\textbf{I}}}}_1^0$, meaning that the model is missing tuples that can witness the truth of $a_i$ being a member of some equivalence class.  We now describe how to define ${\ensuremath{\mbox{\textbf{I}}}}_1^{k+1}$ from ${\ensuremath{\mbox{\textbf{I}}}}_1^{k}$. For each $a \in I_1^k$, if $a \in C_i({\ensuremath{\mbox{\textbf{I}}}}_0)$ for some $i$, it is the case that $a \in V_j({\ensuremath{\mbox{\textbf{I}}}}_0)$ iff ${\ensuremath{\text{bit}_{j}(i)}} = 1$ for $1 \leq
j \leq N$. For such $a$, we may take a minimal witnessing substructure ${\ensuremath{\mbox{\textbf{{S}}}}}_a$ of ${\ensuremath{\mbox{\textbf{I}}}}_0$ such that $a \in
V_j({\ensuremath{\mbox{\textbf{{S}}}}}_a)$ iff ${\ensuremath{\text{bit}_{j}(i)}} = 1$. As each constant in $adom({\ensuremath{\mbox{\textbf{{S}}}}}_a)$ appears in at least one relation in ${\ensuremath{\mbox{\textbf{{S}}}}}_a$, we shall often think of these witnessing structures as databases (i.e. sets of tuples), and refer to them as [justification sets]{}.  We define the structure ${\ensuremath{\mbox{\textbf{I}}}}_1^{k+1}$ to be the union of ${\ensuremath{\mbox{\textbf{I}}}}_1^k$ and all the witnessing structures ${\ensuremath{\mbox{\textbf{{S}}}}}_a$ such that $a$ is unjustified in ${\ensuremath{\mbox{\textbf{I}}}}_1^k$. The elements in $I_1^k$ become *justified* in ${\ensuremath{\mbox{\textbf{I}}}}_1^{k+1}$. The elements in $I_1^{k+1}-I_1^k$ are then said to be [unjustified]{} in ${\ensuremath{\mbox{\textbf{I}}}}_1^{k+1}$. Observe that the structure ${\ensuremath{\mbox{\textbf{I}}}}_1^{K+1}$ does not unjustify any elements that were justified in ${\ensuremath{\mbox{\textbf{I}}}}_1^{k}$, since there is no negation in the view definitions.  Finally, the structure ${\ensuremath{\mbox{\textbf{I}}}}_1$ is defined as the union of all ${\ensuremath{\mbox{\textbf{I}}}}_1^k$s.  Observe that each element in $I_1$ appears in at least one relation in ${\ensuremath{\mbox{\textbf{I}}}}_1$.

The structure ${\ensuremath{\mbox{\textbf{I}}}}_1$ has an intuitive graphical representation, which we denote by ${\ensuremath{\mathcal{H}}}_1$. The graph ${\ensuremath{\mathcal{H}}}_1$ is simply a labeled forest in which each tree $T_i$ (for some $0 \leq i \leq 2^N-1$) corresponds to exactly one witnessing constant $a_i$ for each non-empty $C_i$. We define $T_i$ as follows: the root of $T_i$ is labeled by ${\ensuremath{\mbox{\textbf{{S}}}}}_{a_i} \times C_i$; and for each $j=0,1,\ldots$, any ${\ensuremath{\mbox{\textbf{{S}}}}}_b \times
C_k$-labeled node $v$ at level $j$ (for some justification set ${\ensuremath{\mbox{\textbf{{S}}}}}_b$ and equivalence class formula $C_k$), and any constant $c$ in $adom({\ensuremath{\mbox{\textbf{{S}}}}}_b)$ that is distinct from $b$, define a new ${\ensuremath{\mbox{\textbf{{S}}}}}_c \times C_{k'}$-labeled node to be a child of $v$, for the unique $k'$ such that $c \in C_{k'}({\ensuremath{\mbox{\textbf{I}}}}_0)$. In the following, when the meaning is clear, we shall often refer to an $({\ensuremath{\mbox{\textbf{{S}}}}}_a \times C_k)$-labeled node simply as a ${\ensuremath{\mbox{\textbf{{S}}}}}_a$-labeled node.  Also, observe the similarity of the construction of ${\ensuremath{\mathcal{H}}}_1$ and that of ${\ensuremath{\mbox{\textbf{I}}}}_1$. In fact, the union of all ${\ensuremath{\mbox{\textbf{{S}}}}}_a$, for which there is an ${\ensuremath{\mbox{\textbf{{S}}}}}_a$-labeled node in ${\ensuremath{\mathcal{H}}}_1$, is precisely ${\ensuremath{\mbox{\textbf{I}}}}_1$. Observe also that each tree $T_i$ may be infinite.  For obvious reasons, we shall refer to $T_i$ as a [justification tree]{} (of $a_i$), and to ${\ensuremath{\mathcal{H}}}_1$ as [justification forest]{}.  In the following, for any justification tree $T$ and any justification forest ${\ensuremath{\mathcal{H}}}$, their [corresponding structures]{} (or [databases]{}), denoted by ${\ensuremath{\mathcal{D}}}(T)$ and ${\ensuremath{\mathcal{D}}}({\ensuremath{\mathcal{H}}})$ respectively, are defined to be the union of all ${\ensuremath{\mbox{\textbf{{S}}}}}_a$, such that there is an ${\ensuremath{\mbox{\textbf{{S}}}}}_a$-labeled node in, respectively, $T$ and ${\ensuremath{\mathcal{H}}}$. Furthermore, we shall use $adom(T)$ and $adom({\ensuremath{\mathcal{H}}})$ to denote $adom({\ensuremath{\mathcal{D}}}(T))$ and $adom({\ensuremath{\mathcal{D}}}({\ensuremath{\mathcal{H}}}))$, respectively.  The elements in the set $adom(T)$ and $adom(T)$ and $adom({\ensuremath{\mathcal{H}}})$ are referred to as, respectively, constants in $T$ and constants in ${\ensuremath{\mathcal{H}}}$.

We now illustrate this procedure by a small example.  Define the UCV formula $$\phi = \forall x( V_1(x) \wedge \neg V_2(x) ),$$ where the views are $$\begin{aligned}
    V_1(x) & {\ensuremath{\leftarrow}}& E(x,y) \\
    V_2(x) & {\ensuremath{\leftarrow}}& E(x,x).\end{aligned}$$ Here, we have ${\ensuremath{\mathcal{V}}} = \{V_1,V_2\}$, $\sigma = \langle E \rangle$, and $m = 2$. Suppose that $${\ensuremath{\mbox{\textbf{I}}}}_0 = \langle \mathbb{N}, E = \{(0,1),(1,2),(2,3),(3,4),\ldots\} \rangle$$ is a path extending indefinitely to the right.  Then, we have ${\ensuremath{\mbox{\textbf{I}}}}_0 \models \phi$. Enumerating all non-equivalent views over $\sigma$ of length at most $m$, we have ${\ensuremath{\mathcal{U}}} = \{V_1,V_2,V_3\}$ where $$V_3(x) {\ensuremath{\leftarrow}}E(y,x).$$ Now, there are exactly two non-empty equivalence classes: $$\begin{aligned}
    C_{100} & = & \{0\} \\
    C_{101} & = & \{1,2,\ldots\}.\end{aligned}$$ Then, we have ${\ensuremath{\mbox{\textbf{{S}}}}}_0 = \{E(0,1)\}$ and ${\ensuremath{\mbox{\textbf{{S}}}}}_i = \{E(i-1,i),E(i,i+1)\}$ for $i > 0$. Following the above procedure, we obtain the trees $T_{100}$ and $T_{101}$ as depicted in figure \[fig:H1\].  Note that ${\ensuremath{\mathcal{H}}}_1$ is the disjoint union of $T_{100}$ and $T_{101}$.

*The procedure `rename1`*

*Proviso: in subsequent procedures (including the present one), we shall not change the second entries (i.e. $C_i$) of each node label (i.e. of the form ${\ensuremath{\mbox{\textbf{{S}}}}}_a\times C_i$) and frequently omit mention of them.* 

The aim of this procedure is to ensure that there are no two justification trees $T$ and $T'$ with $adom(T) \cap adom(T') \neq \emptyset$. It essentially performs renaming of constants in $adom(T)$, for each tree $T$ in ${\ensuremath{\mathcal{H}}}_1$. This step will later help us guarantee the correctness of the last step that is used to produce the final model ${\ensuremath{\mbox{\textbf{I}}}}_5$, which relies on a kind of “tree disjointness” property.  More formally, we define ${\ensuremath{\mbox{\textbf{I}}}}_2$ to be the disjoint union[^4] of ${\ensuremath{\mathcal{D}}}(T)$ over all trees $T$ in ${\ensuremath{\mathcal{H}}}_1$. The justification forest ${\ensuremath{\mathcal{H}}}_2$ corresponding to ${\ensuremath{\mbox{\textbf{I}}}}_2$ can be obtained from ${\ensuremath{\mathcal{H}}}_1$ by renaming constants of the tuples in each tree $T$ in ${\ensuremath{\mathcal{H}}}_1$ accordingly.  Let us continue with our previous example of ${\ensuremath{\mathcal{H}}}_1$. The graph ${\ensuremath{\mathcal{H}}}_2$ in this case will be precisely identical to ${\ensuremath{\mathcal{H}}}_1$, except that in $T_{101}$ we use the label, say, ${\ensuremath{\mbox{\textbf{{S}}}}}_{0'} = \{E(0',1')\}$ (resp.  ${\ensuremath{\mbox{\textbf{{S}}}}}_{i'} =
\{E((i-1)',i'),E(i',(i+1)')\}$ for $i > 0$) instead of ${\ensuremath{\mbox{\textbf{{S}}}}}_0$ (resp.  ${\ensuremath{\mbox{\textbf{{S}}}}}_i$ for $i > 0$). 

*The procedure `rename2`*

The aim of this procedure is to transform the model in such a way that each constant $a$ can appear only at two consecutive levels, say $j$ and $j+1$, within each tree.  It appears at level $j$ as part of an $S_b$-labeled node $v$, for some constant $b \neq a$, and at level $j+1$ as part of an $S_a$-labeled node that is a child of $v$. Further, the procedure ensures that any given constant occurs in at most one node’s label at each level in a tree.  Again, this will step will later help us guarantee the correctness of the step that is used to produce the final model ${\ensuremath{\mbox{\textbf{I}}}}_5$, which relies on the existence of a kind of internal “disjointness” property within trees. 

Let us fix a sibling ordering for the nodes within each tree $T_i$ in ${\ensuremath{\mathcal{H}}}_2$. Define a set $U$ of constants disjoint from $I_2$ as follows: $$U = \{ a_{j,l} : \text{$j, l \in \mathbb{N}$ and $a \in I_2$} \}.$$ For $a,b \in I_2$, we require that $a_{j,l} \neq b_{j',l'}$ whenever either $j \neq j'$, or $l \neq l'$, or $a \neq b$. For each tree $T_i$ and for each $j = 1,2,\ldots$, choose the $l$th node $v$ with respect to the fixed sibling ordering (say, ${\ensuremath{\mbox{\textbf{{S}}}}}_a$-labeled) at level $j$ in $T_i$. Let $v$’s children be $v_1,\ldots,v_k$ (labeled by, respectively, ${\ensuremath{\mbox{\textbf{{S}}}}}_{b^1},\ldots,{\ensuremath{\mbox{\textbf{{S}}}}}_{b^k}$ with $b^h \neq a$).  Now do the following: change $v$ to ${\ensuremath{\mbox{\textbf{{S}}}}}_a[b^1_{j,l},\ldots,b^k_{j,l}/b^1,\ldots,b^k]$; and change $v_h$, where $1 \leq h \leq k$, to ${\ensuremath{\mbox{\textbf{{S}}}}}_{b^h_{j,l}} {\ensuremath{\overset{\mbox{\tiny def}}{=}}}{\ensuremath{\mbox{\textbf{{S}}}}}_{b^h}[b^h_{j,l}/b^h]$. Observe that there are two stages in this procedure where each non-root node at level $j$, say ${\ensuremath{\mbox{\textbf{{S}}}}}_a$-labeled, undergoes relabeling: first when we are at level $j-1$ (the constant $a$ is renamed by $a_{j,k}$ for some $k$), and second when we are at level $j$ (constants other than $a_{j,k}$ are renamed for what is now ${\ensuremath{\mbox{\textbf{{S}}}}}_{a_{j,k}}$ ).  The output of this procedure on ${\ensuremath{\mathcal{H}}}_2$ is denoted by ${\ensuremath{\mathcal{H}}}_3$, whose corresponding structure we denote by ${\ensuremath{\mbox{\textbf{I}}}}_3$.

Continuing with our previous example.  The root node $u_1$ of $T_{100}$ in ${\ensuremath{\mathcal{H}}}_2$ is ${\ensuremath{\mbox{\textbf{{S}}}}}_0=\{E(0,1)\}$, its child $u_2$ (sibling zero at level 1) is ${\ensuremath{\mbox{\textbf{{S}}}}}_1=\{E(0,1),E(1,2)\}$ and in turn the children of that child are $u_3={\ensuremath{\mbox{\textbf{{S}}}}}_0=\{E(0,1)\}$ (sibling 0 at level 2) and $u_4={\ensuremath{\mbox{\textbf{{S}}}}}_2=\{E(1,2),E(2,3)\}$ (sibling 1 at level 2).  Under the `rename2` procedure, node $u_1$ is unchanged, since it is at level zero.  Node $u_2$ is changed to ${\ensuremath{\mbox{\textbf{{S}}}}}_1=\{E(0_{1,0},1),E(1,2_{1,0})\}$ Node $u_3$ is changed to ${\ensuremath{\mbox{\textbf{{S}}}}}_{0_{1,0}}=\{E(0_{1,0},1_{2,0})\}$ and $u_4$ is changed to ${\ensuremath{\mbox{\textbf{{S}}}}}_{2_{1,0}}=\{E(1_{2,1},2_{1,0}),E(2_{1,0},3_{2,1})\}$.

*The procedure `copy`*

This procedure makes a number of isomorphic copies of the model ${\ensuremath{\mathcal{H}}}_3$ and then unions them together.  Duplicating the model in this way facilitates the construction of a bounded model by the `prune` procedure, that will be described shortly.  Let $\delta$ be the total number of constants that appear in some tuples from a node label at level $h := cm$ in ${\ensuremath{\mathcal{H}}}_3$, for some fixed $c \in \mathbb{N}$, independent from $\phi$, whose value will later become clear in the proofs that follow.  By virtue of procedure `makeJF`, we are guaranteed that each node in ${\ensuremath{\mathcal{H}}}_3$ can have at most $N \times m$ children, where $N \times m$ represents an upper bound on the number of constants each justification set might contain.  Since there are at most $2^N$ trees in ${\ensuremath{\mathcal{H}}}_3$, by elementary counting, we see that $\delta \leq 2^N \times
(N \times m)^h$. Now, letting $g := cm$, make $\Delta := \delta^{g}$ (isomorphic) copies of ${\ensuremath{\mathcal{H}}}_3$, each with a disjoint set of constants.  That is, the node labeling of each new copy of ${\ensuremath{\mathcal{H}}}_3$ is isomorphic to that of ${\ensuremath{\mathcal{H}}}_3$, except that is uses disjoint set of constants.  Let us call them the copies ${\ensuremath{\mathcal{B}}}_1,
\ldots, {\ensuremath{\mathcal{B}}}_{\Delta}$ (the original copy of ${\ensuremath{\mathcal{H}}}_3$ is included).  So, we have $B_i \cap B_j = \emptyset$, for $i \neq j$. For each tree $T_i$ in ${\ensuremath{\mathcal{H}}}_3$, we denote by $T_i^k$ the isomorphic copy of $T_i$ in ${\ensuremath{\mathcal{B}}}_k$. Now, let $${\ensuremath{\mathcal{H}}}_4 = {\ensuremath{\mathcal{B}}}_1 \cup \ldots \cup {\ensuremath{\mathcal{B}}}_{\Delta}.$$ The structure corresponding to ${\ensuremath{\mathcal{H}}}_4$ is denoted by ${\ensuremath{\mbox{\textbf{I}}}}_4$. In the sequel, each node at level $h$ in ${\ensuremath{\mathcal{B}}}_k$ is said to be a [(potential) leaf]{} of ${\ensuremath{\mathcal{B}}}_k$.

*The procedure `prune`*

The purpose of this procedure is to transform ${\ensuremath{\mathcal{H}}}_4$ into a finite model.  Intuitively, this is achieved by “pruning” all trees at level $h$ and then rejustifying the resulting unjustified constants by “linking” them to a justification being used in some other part of the model.  This is the most complex step in the entire sequences of procedures, and care will be needed later to prove to ensure that satisfiability is not violated when constants are being rejustified. 

We begin first by describing the connections that we wish to construct between the different parts of the model.  Roughly speaking, the model we intend to construct somewhat resembles a $\delta$-regular graph, whose nodes are the copies ${\ensuremath{\mathcal{B}}}_1 \cup \ldots \cup {\ensuremath{\mathcal{B}}}_{\Delta}$ made earlier, and where edges between copies indicate that one copy is being used to make a new justification for a node at level $h$ in another copy. 

Firstly though, we state a proposition from extremal graph theory (see [@Bol04 Theorem 1.4’ Chapter III]\] for proof) that can be used to guarantee the existence of the kind of $\delta$-regular graph we intend to construct. 

Fix two positive integers $\delta, g$ and take an integer $\Delta$ with $$\Delta \geq \frac{(\delta - 1)^{g-1} - 1}{\delta - 2}.$$ Then, there exists a $\delta$-regular graph of size $\Delta$ with girth at least $g$.

Using $\delta,g$ and $\Delta$ as defined in the `copy` procedure, this proposition implies that there exists a $\delta$-regular graph ${\ensuremath{\mbox{\textbf{{G}}}}}$ with vertices $\{{\ensuremath{\mathcal{B}}}_1, \ldots,{\ensuremath{\mathcal{B}}}_{\Delta}\}$ and with girth at least $g$. Let us now treat ${\ensuremath{\mbox{\textbf{{G}}}}}$ as a directed graph, where each edge in ${\ensuremath{\mbox{\textbf{{G}}}}}$ is regarded as two bidirectional arcs. 

Observe that, for each vertex ${\ensuremath{\mathcal{B}}}_k$, there is a bijection $out_k$ from the set of leafs (nodes at height $h$) of ${\ensuremath{\mathcal{B}}}_k$ to the set of arcs going out from ${\ensuremath{\mathcal{B}}}_k$ in ${\ensuremath{\mbox{\textbf{{G}}}}}$. We next take each leaf of ${\ensuremath{\mathcal{B}}}_k$ in turn.  For a leaf $v$ (say, ${\ensuremath{\mbox{\textbf{{S}}}}}_b$-labeled), suppose that $out_k(v) = ({\ensuremath{\mathcal{B}}}_k,{\ensuremath{\mathcal{B}}}_{k'})$. Choose $i$ such that $b \in C_i({\ensuremath{\mbox{\textbf{I}}}}_4)$. If the root of $T_i^{k'}$ is ${\ensuremath{\mbox{\textbf{{S}}}}}_c$-labeled, for some $c \in I_4$, then we delete all descendants of $v$ in $T_i^k$ and change $v$ to ${\ensuremath{\mbox{\textbf{{S}}}}}_c[b/c]$. In this way, we “prune” each of the trees in ${\ensuremath{\mathcal{H}}}_4$, and link each leaf node to the root node of another tree for the purpose of justification.  We denote by ${\ensuremath{\mathcal{H}}}_5$ the resulting collection of interlinked models, whose corresponding structure is denoted by ${\ensuremath{\mbox{\textbf{I}}}}_5$. ${\ensuremath{\mathcal{H}}}_5$ can be thought of as a collection of interlinked forests, where each forest corresponds to one of the copies $\{{\ensuremath{\mathcal{B}}}_1, \ldots,{\ensuremath{\mathcal{B}}}_{\Delta}\}$ and each forest is a collection of trees. 

Observe now that each “tree” in ${\ensuremath{\mathcal{H}}}_5$ is of height $h$. Since there are at most $\Delta \times 2^N$ trees in ${\ensuremath{\mathcal{H}}}_5$, each of which has at most $(N \times m)^{h+1}$ constants, we see that $$\begin{aligned}
    I_5 & \leq & (\Delta \times 2^N) \times (N \times m)^{h+1} \\
        & \leq & ((2^N \times (Nm)^{cm})^{cm} \times 2^N) \times
        (N\times m)^{cm+1}\end{aligned}$$ It is easy to calculate now that $I_5 \leq 2^{2^{q(p,m)}}$ for some polynomial $q$ in $p$ and $m$. We have thus managed to construct a bounded model ${\ensuremath{\mbox{\textbf{I}}}}_5$ which satisfies the original ${\ensuremath{\text{UCV}}}$ formula $\phi$.

We now prove the correctness of our construction for theorem \[th:fin\_s\].  The proof is divided into a series of subproperties that assert the correctness of each procedure in our construction.  First, we prove a simple lemma. 

Let ${\ensuremath{\mathcal{V}}}$ be a set of (unary) views over a vocabulary $\sigma$. Suppose ${\ensuremath{\mbox{\textbf{I}}}}, {\ensuremath{\mbox{\textbf{J}}}}$ are $\sigma$-structures such that $C({\ensuremath{\mbox{\textbf{I}}}})$ is non-empty iff $C({\ensuremath{\mbox{\textbf{J}}}})$ is non-empty for each equivalence class formula $C$ constructed with respect to ${\ensuremath{\mathcal{V}}}$. Then, ${\ensuremath{\mbox{\textbf{I}}}}$ and ${\ensuremath{\mbox{\textbf{J}}}}$ agree on ${\ensuremath{\text{UCV}}}(\sigma,{\ensuremath{\mathcal{V}}})$. \[lm:equiv\]

By standard Ehrenfeucht-Fraïsse argument, we see that $\Lambda({\ensuremath{\mbox{\textbf{I}}}})$ and $\Lambda({\ensuremath{\mbox{\textbf{J}}}})$ agree on ${\ensuremath{\text{UFO}}}({\ensuremath{\mathcal{V}}})$. Then, by lemma \[lem:realize\], we have that ${\ensuremath{\mbox{\textbf{I}}}}$ and ${\ensuremath{\mbox{\textbf{J}}}}$ agree on ${\ensuremath{\text{UCV}}}(\sigma,{\ensuremath{\mathcal{V}}})$.

1.   For each node $v$ (say, $({\ensuremath{\mbox{\textbf{{S}}}}}_a \times C_i)$-labeled) of ${\ensuremath{\mathcal{H}}}_1$, $a \in C_i({\ensuremath{\mbox{\textbf{I}}}}_1)$ with witnessing structure ${\ensuremath{\mbox{\textbf{{S}}}}}_a$.

2.   If ${\ensuremath{\mbox{\textbf{I}}}}_0 \models \phi$, then ${\ensuremath{\mbox{\textbf{I}}}}_1 \models \phi$.

\[subp:makeJHS\]

First, note that ${\ensuremath{\mbox{\textbf{I}}}}_1 \subseteq {\ensuremath{\mbox{\textbf{I}}}}_0$. Since conjunctive queries are monotonic, we have $V({\ensuremath{\mbox{\textbf{I}}}}_1) \subseteq V({\ensuremath{\mbox{\textbf{I}}}}_0)$ for each view $V \in {\ensuremath{\mathcal{U}}}$. So, we have that $a \in V({\ensuremath{\mbox{\textbf{I}}}}_1)$ implies that $a \in
V({\ensuremath{\mbox{\textbf{I}}}}_0)$. In addition, for each constant $a \in I_1$, if $a \in V({\ensuremath{\mbox{\textbf{I}}}}_0)$, then $a \in V({\ensuremath{\mbox{\textbf{I}}}}_1)$, which is witnessed at some ${\ensuremath{\mbox{\textbf{{S}}}}}_a$-labeled node.  In turn, this implies that for $a \in I_1$, it is the case that $a \in C({\ensuremath{\mbox{\textbf{I}}}}_1)$ iff $a \in C({\ensuremath{\mbox{\textbf{I}}}}_0)$. This proves the first statement.  Also, by construction, if $C_i({\ensuremath{\mbox{\textbf{I}}}}_0)$ is non-empty, where $i \in
\{0,\ldots,2^N-1\}$, we know that one of its members belongs to ${\ensuremath{\mbox{\textbf{I}}}}_1$, witnessed at the root of $T_i$. Therefore, we also have that $C({\ensuremath{\mbox{\textbf{I}}}}_0)$ is non-empty iff $C({\ensuremath{\mbox{\textbf{I}}}}_1)$ is non-empty.  In view of lemma \[lm:equiv\], we conclude the second statement. 

At this stage, it is worth noting that, once ${\ensuremath{\mathcal{H}}}_1$ has been constructed, the subsequent procedures might modify the label $({\ensuremath{\mbox{\textbf{{S}}}}}_a\times C_i)$ — its name (e.g. from ${\ensuremath{\mbox{\textbf{{S}}}}}_a\times C_i$ to ${\ensuremath{\mbox{\textbf{{S}}}}}_{a'} \times C_i$ for some new constant $a'$) as well as its contents (e.g. replacing each occurrence of a tuple $R(a,a)$ by $R(a',a')$ for some new constant $a'$).  Despite this, we wish to highlight that one invariant is preserved by each of these procedures that have been described:

Suppose ${\ensuremath{\mathcal{H}}}$ is a justification forest of a structure ${\ensuremath{\mbox{\textbf{{I}}}}}$, and $v$ a $({\ensuremath{\mbox{\textbf{{S}}}}}_a\times C_i)$-labeled node of ${\ensuremath{\mathcal{H}}}$. Then, we have $a \in C_i({\ensuremath{\mbox{\textbf{{I}}}}})$ with witnessing structure ${\ensuremath{\mbox{\textbf{{S}}}}}_a$. \[inv:JS\]

Subproperty \[subp:makeJHS\] shows that this is satisfied by ${\ensuremath{\mathcal{H}}}_1$. In fact, that this invariant is preserved by the later procedures will be almost immediate from the proof of correctness of the procedure.  Hence, we leave it to the reader to verify. 

If ${\ensuremath{\mbox{\textbf{I}}}}_1 \models \phi$, then ${\ensuremath{\mbox{\textbf{I}}}}_2 \models \phi$. \[subp:rename\]

In this procedure, we perform constant renaming for each tree $T_i$ in ${\ensuremath{\mathcal{H}}}_1$. For the purpose of this proof, let us denote the tree so obtained by $T_i'$. Such a renaming induces a bijection $f_i: adom(T_i){\ensuremath{\rightarrow}}adom(T_i')$. Extend $f_i$ to tuples, structures, and trees in the obvious way.  Observe that the structures corresponding to the trees $f_i(T_i)$ and $T_i$ are isomorphic.  Now, in view of lemma \[lem:rename\], it is easy to check that for each tree $T_i$ in ${\ensuremath{\mathcal{H}}}_1$ and a constant $a$ in the structure corresponding to $T_i$, $a \in C_j({\ensuremath{\mbox{\textbf{I}}}}_1)$ iff $f_i(a) \in C_j({\ensuremath{\mbox{\textbf{I}}}}_2)$. By virtue of by lemma \[lm:equiv\], we conclude our proof. 

Suppose that $a$ is a constant in the structure corresponding to $T_i$ of ${\ensuremath{\mathcal{H}}}_1$. Then, $a \in V({\ensuremath{\mbox{\textbf{I}}}}_1)$ iff $f_i(a) \in V({\ensuremath{\mbox{\textbf{I}}}}_2)$. \[lem:rename\]

(${\ensuremath{\Rightarrow}}$) By subproperty \[subp:makeJHS\], it is the case that $a \in
V({\ensuremath{\mbox{\textbf{{S}}}}}_a)$. Since $f_i$ is a bijection, it is also true that $f_i(a) \in V(f_i({\ensuremath{\mbox{\textbf{{S}}}}}_a))$. (${\ensuremath{\Leftarrow}}$) Let ${\ensuremath{\mbox{\textbf{{M}}}}}$ be a minimal set of tuples in ${\ensuremath{\mbox{\textbf{I}}}}_2$ such that $f_i(a) \in
V({\ensuremath{\mbox{\textbf{{M}}}}})$. Observe that there is a one-to-one function mapping the set of conjuncts in $V$ to ${\ensuremath{\mbox{\textbf{{M}}}}}$. For each tree $T_j$ in ${\ensuremath{\mathcal{H}}}_2$, let ${\ensuremath{\mbox{\textbf{{M}}}}}_j$ denote the members of ${\ensuremath{\mbox{\textbf{{M}}}}}$ that can be found in $T_j$. Note that $adom({\ensuremath{\mbox{\textbf{{M}}}}}_j) \cap adom({\ensuremath{\mbox{\textbf{{M}}}}}_{j'}) = \emptyset$ for $j
\neq j'$. Now, let ${\ensuremath{\mbox{\textbf{{M}}}}}' = \bigcup_j f_j^{-1}({\ensuremath{\mbox{\textbf{{M}}}}}_j)$. It is not hard to see that $a \in V({\ensuremath{\mbox{\textbf{{M}}}}}')$. Since ${\ensuremath{\mbox{\textbf{{M}}}}}' \subseteq {\ensuremath{\mbox{\textbf{I}}}}_1$, we have $a \in V({\ensuremath{\mbox{\textbf{I}}}}_1)$.

If ${\ensuremath{\mbox{\textbf{I}}}}_2 \models \phi$, then ${\ensuremath{\mbox{\textbf{I}}}}_3 \models \phi$. \[subp:maxim\]

Define the function $\eta:I_3 {\ensuremath{\rightarrow}}I_2$ such that $\eta(a_{j,k}) = a$. Note that $\eta$ is onto.  Extend $\eta$ to tuples, and sets of tuples in the obvious way.  In view of lemma \[lm:equiv\], it is sufficient to show that, for each $a \in I_3$ and $i \in
\{0,\ldots,2^N-1\}$, $a \in C_i({\ensuremath{\mbox{\textbf{I}}}}_3)$ iff $\eta(a) \in C_i({\ensuremath{\mbox{\textbf{I}}}}_2)$. In turn, it is enough to show that, $a \in V({\ensuremath{\mbox{\textbf{I}}}}_3)$ iff $\eta(a) \in
V({\ensuremath{\mbox{\textbf{I}}}}_2)$.

(${\ensuremath{\Rightarrow}}$) Take a minimal set ${\ensuremath{\mbox{\textbf{{M}}}}}$ of tuples in ${\ensuremath{\mbox{\textbf{I}}}}_3$ such that $a \in V({\ensuremath{\mbox{\textbf{{M}}}}})$. Then, we have $\eta(a) \in V(\eta({\ensuremath{\mbox{\textbf{{M}}}}}))$. Since $\eta({\ensuremath{\mbox{\textbf{{M}}}}}) \subseteq {\ensuremath{\mbox{\textbf{I}}}}_2$, we have $\eta(a) \in V({\ensuremath{\mbox{\textbf{I}}}}_2)$.

(${\ensuremath{\Leftarrow}}$) Since invariant \[inv:JS\] holds for ${\ensuremath{\mathcal{H}}}_2$, the fact that $\eta(a) \in V({\ensuremath{\mbox{\textbf{I}}}}_2)$ is witnessed by $S_{\eta(a)} \in {\ensuremath{\mathcal{H}}}_2$. Since $S_a$ and $S_{\eta(a)}$ are isomorphic justification sets, we have that $a \in V({\ensuremath{\mbox{\textbf{I}}}}_3)$ is justified by $S_a \in {\ensuremath{\mathcal{H}}}_3$.

1.   For each node $v$ (say, $({\ensuremath{\mbox{\textbf{{S}}}}}_a \times C_i)$-labeled) of ${\ensuremath{\mathcal{H}}}_4$, $a \in C_i({\ensuremath{\mbox{\textbf{I}}}}_4)$ with witnessing structure ${\ensuremath{\mbox{\textbf{{S}}}}}_a$.

2.   If ${\ensuremath{\mbox{\textbf{I}}}}_3 \models \phi$, then ${\ensuremath{\mbox{\textbf{I}}}}_4 \models \phi$.

\[subp:copy\]

Similar to the proof of subproperty \[subp:rename\]. 

If ${\ensuremath{\mbox{\textbf{I}}}}_4 \models \phi$, then ${\ensuremath{\mbox{\textbf{I}}}}_5 \models \phi$. \[subp:prune\]

Recall that there are $N_l {\ensuremath{\overset{\mbox{\tiny def}}{=}}}\delta \times \Delta$ leafs in ${\ensuremath{\mathcal{H}}}_4$. Let us order these nodes as $v_1,\ldots,v_{N_l}$. Suppose also that $v_i$ is labeled by ${\ensuremath{\mbox{\textbf{{S}}}}}_{b_i}$ for some $b_i \in I_4$. By virtue of `rename2`, we see that $b_i \neq b_j$ whenever $i \neq j$. Next, we may think of the procedure `prune` as consisting of $N_l$ steps, where at step $i$, the node $v_i$ has all its descendants removed (pruned) and $v_i$ is changed to ${\ensuremath{\mbox{\textbf{{S}}}}}_{b_i}' {\ensuremath{\overset{\mbox{\tiny def}}{=}}}{\ensuremath{\mbox{\textbf{{S}}}}}_{c_i}[b_i/c_i]$ for some $c_i \in I_4$. Letting ${\ensuremath{\mathcal{K}}}_0 {\ensuremath{\overset{\mbox{\tiny def}}{=}}}{\ensuremath{\mathcal{H}}}_4$, we denote by ${\ensuremath{\mathcal{K}}}_i$ ($i = 1,\ldots,N_l$) the resulting model after executing $i$ steps on ${\ensuremath{\mathcal{K}}}_0$. The structure corresponding to ${\ensuremath{\mathcal{K}}}_i$ is denoted by ${\ensuremath{\mbox{\textbf{J}}}}_i$.

We wish to prove by induction on $0 \leq i < N_l$ that

(I)

:   For each $a \in J_{i+1}$ and $V \in {\ensuremath{\mathcal{U}}}$, $a \in V({\ensuremath{\mbox{\textbf{J}}}}_{i+1})$ iff $a \in V({\ensuremath{\mbox{\textbf{J}}}}_i)$.

(II)

:   Invariant \[inv:JS\] holds for ${\ensuremath{\mbox{\textbf{J}}}}_{i+1}$.

(III)

:   For each $a \in J_{i+1}$, we have $a \in C_i({\ensuremath{\mbox{\textbf{J}}}}_{i+1})$ iff $a \in C_i({\ensuremath{\mbox{\textbf{J}}}}_i)$.

Note that $J_{i+1} \subseteq J_i$. So, by lemma \[lm:equiv\] and the fact that invariant \[inv:JS\] holds for the initial case ${\ensuremath{\mbox{\textbf{{J}}}}}_0$ (from proofs of previous subproperties), statement (III) will imply what we wish to prove.  It is easy to see that statement (III) is a direct consequence of statement (I).  It is also easy to show that statement (I) implies statement (II).  This follows since firstly, at step $i+1$, we replace the content of ${\ensuremath{\mbox{\textbf{{S}}}}}_{b_i}$ by that of ${\ensuremath{\mbox{\textbf{{S}}}}}_{c_i}$, except for substituting $b_i$ for $c_i$. Second, the elements $b_i$ and $c_i$ belong to the same equivalence class in ${\ensuremath{\mbox{\textbf{J}}}}_i$, and invariant \[inv:JS\] holds for ${\ensuremath{\mbox{\textbf{J}}}}_i$ by induction.  Therefore, it remains only to prove statement (I). 

Let us now fix $i < N_l$, $a \in J_{i+1}$, and $V \in {\ensuremath{\mathcal{U}}}$. It is simple to prove that $a \in V({\ensuremath{\mbox{\textbf{J}}}}_i)$ implies $a \in V({\ensuremath{\mbox{\textbf{J}}}}_{i+1})$. This is witnessed by tuples in the ${\ensuremath{\mbox{\textbf{{S}}}}}_a$-labeled (or ${\ensuremath{\mbox{\textbf{{S}}}}}_{b_i}'$-labeled if $a = b_i$) node in ${\ensuremath{\mathcal{K}}}_{i+1}$, which exists by construction. 

Conversely, we take a minimal set ${\ensuremath{\mbox{\textbf{{M}}}}}$ of tuples in ${\ensuremath{\mbox{\textbf{J}}}}_{i+1}$ with $a \in V({\ensuremath{\mbox{\textbf{J}}}}_{i+1})$, witnessed by the valuation $\nu$. Our aim is to find a set ${\ensuremath{\mbox{\textbf{{M}}}}}'$ of tuples in ${\ensuremath{\mbox{\textbf{J}}}}_i$ with $a \in V({\ensuremath{\mbox{\textbf{{M}}}}}')$. Let ${\ensuremath{\mbox{\textbf{{M}}}}}_{b_i} {\ensuremath{\overset{\mbox{\tiny def}}{=}}}{\ensuremath{\mbox{\textbf{{M}}}}} -
{\ensuremath{\mathcal{D}}}({\ensuremath{\mbox{\textbf{J}}}}_i)$. Intuitively, ${\ensuremath{\mbox{\textbf{{M}}}}}_{b_i}$ contains the set of *new* tuples.  These are tuples which did not exist in the structure ${\ensuremath{\mbox{\textbf{J}}}}_i$ and have been created specifically to justify the node whose descendants (justifications) have just been pruned.  By construction, we have ${\ensuremath{\mbox{\textbf{{M}}}}}_{b_i} \subseteq
{\ensuremath{\mbox{\textbf{{S}}}}}_{b_i}'$, which implies that $adom({\ensuremath{\mbox{\textbf{{M}}}}}_{b_i}) \subseteq
adom({\ensuremath{\mbox{\textbf{{S}}}}}_{b_i}')$. Observe also that $b_i \in adom(t)$ for each tuple $t$ in ${\ensuremath{\mbox{\textbf{{M}}}}}_{b_i}$; otherwise, $t$ would be a tuple in ${\ensuremath{\mbox{\textbf{{S}}}}}_{c_i} \subseteq {\ensuremath{\mbox{\textbf{J}}}}_i$ (i.e. it would not be a new tuple).  Define $${\ensuremath{\mbox{\textbf{{L}}}}} := \{ t \in {\ensuremath{\mbox{\textbf{{M}}}}} - {\ensuremath{\mbox{\textbf{{M}}}}}_{b_i} : \text{$t$ is connected to
            some $t' \in {\ensuremath{\mbox{\textbf{{M}}}}}_{b_i}$ in ${\ensuremath{\mbox{\textbf{{M}}}}}$} \}.$$ ${\ensuremath{\mbox{\textbf{{L}}}}}$ consists of tuples that are connected to new tuples.  Also, let ${\ensuremath{\mbox{\textbf{{L}}}}}' {\ensuremath{\overset{\mbox{\tiny def}}{=}}}{\ensuremath{\mbox{\textbf{{M}}}}} - {\ensuremath{\mbox{\textbf{{M}}}}}_{b_i} - {\ensuremath{\mbox{\textbf{{L}}}}}$, i.e., the set of all tuples of ${\ensuremath{\mbox{\textbf{{M}}}}}$ that are *not* connected to any (new) tuples in ${\ensuremath{\mbox{\textbf{{M}}}}}_{b_i}$. Note that ${\ensuremath{\mbox{\textbf{{L}}}}} \cup {\ensuremath{\mbox{\textbf{{L}}}}}' \subseteq {\ensuremath{\mbox{\textbf{J}}}}_i$, and that the sets ${\ensuremath{\mbox{\textbf{{M}}}}}_{b_i}$, ${\ensuremath{\mbox{\textbf{{L}}}}}$, and ${\ensuremath{\mbox{\textbf{{L}}}}}'$ form a partition on ${\ensuremath{\mbox{\textbf{{M}}}}}$. Also, by definition, we have $adom({\ensuremath{\mbox{\textbf{{L}}}}}') \cap adom({\ensuremath{\mbox{\textbf{{M}}}}}_{b_i}
\cup {\ensuremath{\mbox{\textbf{{L}}}}}) = \emptyset$. In the following, we define ${\ensuremath{\mbox{\textbf{{M}}}}}_{c_i} {\ensuremath{\overset{\mbox{\tiny def}}{=}}}{\ensuremath{\mbox{\textbf{{M}}}}}_{b_i}[c_i/b_i]$. Note that ${\ensuremath{\mbox{\textbf{{M}}}}}_{c_i} \subseteq {\ensuremath{\mbox{\textbf{{S}}}}}_{c_i}
\subseteq {\ensuremath{\mbox{\textbf{J}}}}_i$.

Before we proceed further, it is helpful to see how we partition ${\ensuremath{\mbox{\textbf{{M}}}}}$ on a simple example.  Suppose that the view $V$ is defined as $$V(x_0) {\ensuremath{\leftarrow}}E(x_0,x_1),E(x_1,x_2),R(x_3,x_4),R(x_4,x_5).$$ Furthermore, suppose that we take the valuation $\nu$ defined as $\nu(x_i) = i$. In this case, ${\ensuremath{\mbox{\textbf{{M}}}}}$ can be described diagrammatically as follows $$V(0) {\ensuremath{\leftarrow}}E(0,1),E(1,2),R(3,4),R(4,5).$$ Assume now that the only tuple in ${\ensuremath{\mbox{\textbf{{M}}}}}$ that doesn’t belong to ${\ensuremath{\mathcal{D}}}({\ensuremath{\mbox{\textbf{J}}}}_i)$ is $E(0,1)$. Then, we have ${\ensuremath{\mbox{\textbf{{M}}}}}_{b_i} = \{E(0,1)\}$. It is easy to show that ${\ensuremath{\mbox{\textbf{{L}}}}} = \{E(1,2)\}$ and ${\ensuremath{\mbox{\textbf{{L}}}}}' =
\{R(3,4),R(4,5)\}$.

We next state a result regarding ${\ensuremath{\mbox{\textbf{{L}}}}}$ that will shortly be needed.  It clarifies the nature of a partition that exists for ${\ensuremath{\mbox{\textbf{{L}}}}}$ and the relationships which hold between the elements of the partition. 

We can find tuple-sets ${\ensuremath{\mbox{\textbf{{A}}}}}, {\ensuremath{\mbox{\textbf{{B}}}}} \subseteq {\ensuremath{\mbox{\textbf{{L}}}}}$ such that:

1.   ${\ensuremath{\mbox{\textbf{{A}}}}} \cap {\ensuremath{\mbox{\textbf{{B}}}}} = \emptyset$,

2.   ${\ensuremath{\mbox{\textbf{{A}}}}} \cup {\ensuremath{\mbox{\textbf{{B}}}}} = {\ensuremath{\mbox{\textbf{{L}}}}}$,

3.   $adom({\ensuremath{\mbox{\textbf{{A}}}}}) \cap adom({\ensuremath{\mbox{\textbf{{B}}}}}) = \emptyset$,

4.   $b_i \notin adom({\ensuremath{\mbox{\textbf{{B}}}}})$, and

5.   $adom({\ensuremath{\mbox{\textbf{{M}}}}}_{b_i}) \cap adom({\ensuremath{\mbox{\textbf{{A}}}}}) \subseteq \{b_i\}$.

\[prop:part\]

The proof of this proposition can be found at the end of this section.  We now shall construct ${\ensuremath{\mbox{\textbf{{M}}}}}' \subseteq {\ensuremath{\mathcal{D}}}({\ensuremath{\mbox{\textbf{J}}}}_i)$ such that $a \in V({\ensuremath{\mbox{\textbf{{M}}}}}')$. First, we put ${\ensuremath{\mbox{\textbf{{L}}}}}'$ in ${\ensuremath{\mbox{\textbf{{M}}}}}'$. This does not affect our choice of tuple-sets that replace ${\ensuremath{\mbox{\textbf{{M}}}}}_{b_i}$, ${\ensuremath{\mbox{\textbf{{A}}}}}$, and ${\ensuremath{\mbox{\textbf{{B}}}}}$ as $adom({\ensuremath{\mbox{\textbf{{L}}}}}') \cap adom({\ensuremath{\mbox{\textbf{{M}}}}}_{b_i} \cup {\ensuremath{\mbox{\textbf{{L}}}}}) = \emptyset$ (i.e. the set of free tuples instantiated by ${\ensuremath{\mbox{\textbf{{L}}}}}'$ and the set of free tuples instantiated by ${\ensuremath{\mbox{\textbf{{M}}}}}_{b_i} \cup {\ensuremath{\mbox{\textbf{{L}}}}}$ share no common variables), as we have noted earlier.  There are two cases to consider:

case 1

:   $a = b_i$. Let $F$ be the set of all free tuples in the body of $V$ such that $\{ \nu(u) : u \in F \} =
                {\ensuremath{\mbox{\textbf{{M}}}}}_{b_i} \cup {\ensuremath{\mbox{\textbf{{B}}}}}$. Suppose $X$ is the set of all variables in $V$. Let $\{y_1,\ldots,y_r\} \subseteq X$ be the set of variables in $F$ such that $\nu(y_j) = b_i$. With $y$ as a new variable, let $F' := F[y/y_1,\ldots,y_r]$. Define the new view $V'(y)$ whose conjuncts are exactly $F'$: $$V'(y) {\ensuremath{\leftarrow}}\bigwedge F'$$ Trivially, we have $b_i \in V'({\ensuremath{\mbox{\textbf{{M}}}}}_{b_i} \cup {\ensuremath{\mbox{\textbf{{B}}}}})$. Then, as $b_i \notin adom({\ensuremath{\mbox{\textbf{{B}}}}})$ by proposition \[prop:part\], we have $c_i \in V'({\ensuremath{\mbox{\textbf{{M}}}}}_{c_i} \cup
            {\ensuremath{\mbox{\textbf{{B}}}}})$. Note that ${\ensuremath{\mbox{\textbf{{M}}}}}_{c_i} \cup {\ensuremath{\mbox{\textbf{{B}}}}} \subseteq
            {\ensuremath{\mathcal{D}}}({\ensuremath{\mbox{\textbf{J}}}}_i)$ and $V' \in {\ensuremath{\mathcal{U}}}$ since $length(V') \leq m$. So, since by induction $b_i$ and $c_i$ belong to the same equivalence class in ${\ensuremath{\mbox{\textbf{J}}}}_i$, there exist tuple-sets ${\ensuremath{\mbox{\textbf{{P}}}}}_{b_i}$ and ${\ensuremath{\mbox{\textbf{{B}}}}}'$ with ${\ensuremath{\mbox{\textbf{{P}}}}}_{b_i} \cup {\ensuremath{\mbox{\textbf{{B}}}}}'
            \subseteq {\ensuremath{\mbox{\textbf{J}}}}_i$ such that $b_i \in V'({\ensuremath{\mbox{\textbf{{P}}}}}_{b_i} \cup {\ensuremath{\mbox{\textbf{{B}}}}}')$. \[${\ensuremath{\mbox{\textbf{{P}}}}}_{b_i}$ and ${\ensuremath{\mbox{\textbf{{B}}}}}'$, respectively, replace the role of ${\ensuremath{\mbox{\textbf{{M}}}}}_{c_i}$ and ${\ensuremath{\mbox{\textbf{{B}}}}}$.\] Observe now that $a \notin
            adom({\ensuremath{\mbox{\textbf{{B}}}}})$ as $a = b_i$. Since $adom({\ensuremath{\mbox{\textbf{{M}}}}}_{b_i})
            \cap adom({\ensuremath{\mbox{\textbf{{A}}}}}) \subseteq
            \{b_i\}$ and $adom({\ensuremath{\mbox{\textbf{{A}}}}}) \cap adom({\ensuremath{\mbox{\textbf{{B}}}}}) = \emptyset$ from proposition \[prop:part\], it is easy to verify that $$a \in V({\ensuremath{\mbox{\textbf{{P}}}}}_{b_i} \cup {\ensuremath{\mbox{\textbf{{A}}}}} \cup {\ensuremath{\mbox{\textbf{{B}}}}}' \cup {\ensuremath{\mbox{\textbf{{L}}}}}').$$

case 2

:   $a \neq b_i$. This is divided into two further cases:

    (a)

    :   $b_i \in adom(A)$. This is divided into two further cases:

        (i)

        :   $a \in adom(A)$. In this case, note that $a \notin adom({\ensuremath{\mbox{\textbf{{M}}}}}_{b_i})$ (using Proposition \[prop:part\](5)) and $a \notin adom({\ensuremath{\mbox{\textbf{{B}}}}}$) (using Proposition \[prop:part\](3)).  We can then continue in the same fashion as in the case 1. 

        (ii)

        :   $a \notin adom(A)$. Let $F$ be the set of all free tuples in the body of $V$ such that $\{ \nu(u) : u \in F \} =
                    {\ensuremath{\mbox{\textbf{{A}}}}}$. Let $\{y_1,\ldots,y_r\} \subseteq X$ be the set of variables in $F$ such that $\nu(y_j) = b_i$. Let $y$ be a new variable (i.e. $y \notin X$) and $F' := F[y/y_1,\ldots, y_r]$, i.e., we replace each occurrence of the variables $y_1, \ldots, y_r$ in $F$ by $y$. Then, let $V'(y)$ be the view whose conjuncts are exactly $F'$: $$V'(y) {\ensuremath{\leftarrow}}\bigwedge F'.$$ Then, $V' \in {\ensuremath{\mathcal{U}}}$ and $b_i \in V'({\ensuremath{\mbox{\textbf{{A}}}}})$. Since ${\ensuremath{\mbox{\textbf{{A}}}}} \subseteq {\ensuremath{\mathcal{D}}}({\ensuremath{\mbox{\textbf{J}}}}_i)$ and because $b_i$ and $c_i$ belong to the same equivalence class in ${\ensuremath{\mbox{\textbf{J}}}}_i$ (by the induction hypothesis), there exists a set ${\ensuremath{\mbox{\textbf{{A}}}}}' \subseteq {\ensuremath{\mathcal{D}}}({\ensuremath{\mbox{\textbf{J}}}}_i)$ such that $c_i \in V'({\ensuremath{\mbox{\textbf{{A}}}}}')$. Since $adom({\ensuremath{\mbox{\textbf{{M}}}}}_{b_i}) \cap
                    adom({\ensuremath{\mbox{\textbf{{A}}}}}) \subseteq \{b_i\}$ and $adom({\ensuremath{\mbox{\textbf{{A}}}}}) \cap adom({\ensuremath{\mbox{\textbf{{B}}}}}) = \emptyset$ from proposition \[prop:part\], it is easy to check that $a \in V'({\ensuremath{\mbox{\textbf{{M}}}}}_{c_i} \cup {\ensuremath{\mbox{\textbf{{A}}}}}' \cup {\ensuremath{\mbox{\textbf{{B}}}}} \cup {\ensuremath{\mbox{\textbf{{L}}}}}')$.

    (b)

    :   $b_i \notin adom(A)$. Let ${\ensuremath{\mbox{\textbf{{M}}}}}_{c_i} {\ensuremath{\overset{\mbox{\tiny def}}{=}}}{\ensuremath{\mbox{\textbf{{M}}}}}_{b_i}[c_i/b_i]$. By construction, we see that ${\ensuremath{\mbox{\textbf{{M}}}}}_{c_i} \subseteq {\ensuremath{\mbox{\textbf{{S}}}}}_{c_i} \subseteq {\ensuremath{\mathcal{D}}}({\ensuremath{\mbox{\textbf{J}}}}_i)$. By proposition \[prop:part\] (items 4 and 5), it is the case that $$a \in V({\ensuremath{\mbox{\textbf{{M}}}}}_{c_i} \cup {\ensuremath{\mbox{\textbf{{A}}}}} \cup {\ensuremath{\mbox{\textbf{{B}}}}} \cup {\ensuremath{\mbox{\textbf{{L}}}}}').$$

In any case, we have $a \in V({\ensuremath{\mbox{\textbf{J}}}}_i)$. This completes the proof. 

It remains to prove proposition \[prop:part\]. 

The present situation is depicted in figure \[fig:part\]. 

This is a snapshot of the moment just before we apply step $i+1$. Step $i$ of `prune` procedure simply prunes the subtree rooted at the ${\ensuremath{\mbox{\textbf{{S}}}}}_{b_i}$-labeled node $v$, and links (rejustifies) $v$ using the ${\ensuremath{\mbox{\textbf{{S}}}}}_{c_i}$-labeled node $w$, where $b_i$ and $c_i$ belong to the same equivalence class in ${\ensuremath{\mbox{\textbf{{J}}}}}_i$. It is important to note that some cousin[^5] $w_3$ of $v$ might also be linked to a root $w_6$ of another tree, which in turn might be linked to a leaf node $w_2$ of another tree, which in turn might have a cousin $w_1$ that satisfies the same property as $w_3$ and so on.  Furthermore, the node $w$ might have also been linked to some other leaf $w_4$ that has a cousin $w_5$ that is connected to a root of some other tree, and so on.  Note that it is impossible for two leafs of a tree to be linked to the same root node of a tree by construction.  Hence, the three trees in the middle (i.e. where $v,w$, and $w_6$ are located) are necessarily distinct.  The leftmost and rightmost tree might be the same tree depending on the value of the girth $g$ that we defined earlier. 

Let us now define $$\begin{aligned}
    {\ensuremath{\mbox{\textbf{{A}}}}} & {\ensuremath{\overset{\mbox{\tiny def}}{=}}}& \{ t \in {\ensuremath{\mbox{\textbf{{L}}}}} : d_{{\ensuremath{\Bbb{G}}}({\ensuremath{\mbox{\textbf{{J}}}}}_i)}(t,b_i)
                    \leq m \} \\
    {\ensuremath{\mbox{\textbf{{B}}}}} & {\ensuremath{\overset{\mbox{\tiny def}}{=}}}& \{ t \in {\ensuremath{\mbox{\textbf{{L}}}}} : d_{{\ensuremath{\Bbb{G}}}({\ensuremath{\mbox{\textbf{{J}}}}}_i)}(t,{\ensuremath{\mbox{\textbf{{S}}}}}_{c_i})
                    \leq m \}.\end{aligned}$$ Intuitively, the set ${\ensuremath{\mbox{\textbf{{A}}}}}$ contains tuples up to distance $m$ from the label ${\ensuremath{\mbox{\textbf{{S}}}}}_{b_i}$ of node $v$ in ${\ensuremath{\mbox{\textbf{J}}}}_i$, while the set ${\ensuremath{\mbox{\textbf{{B}}}}}$ contains tuples up to distance $m$ from the label ${\ensuremath{\mbox{\textbf{{S}}}}}_{c_i}$ of $w$ in ${\ensuremath{\mbox{\textbf{J}}}}_i$. Note that this is distance in the structure ${\ensuremath{\mbox{\textbf{J}}}}_i$, not ${\ensuremath{\mbox{\textbf{J}}}}_{i+1}$. It is immediate that we have property (2) ${\ensuremath{\mbox{\textbf{{A}}}}} \cup {\ensuremath{\mbox{\textbf{{B}}}}} = {\ensuremath{\mbox{\textbf{{L}}}}}$, as the length of the view $V$ is at most $m$ and that $adom({\ensuremath{\mbox{\textbf{{M}}}}}_{b_i}) \subseteq \{b_i\} \cup adom({\ensuremath{\mbox{\textbf{{S}}}}}_{c_i})$. So, it is sufficient to show that properties 3 and 5 are satisfied, as they obviously imply properties 1 and 4.  Note that our construction has ensured that:

1.   Two nodes in any given tree in ${\ensuremath{\mathcal{K}}}_i$ that are at least distance two apart cannot share a constant. 

2.   Two trees $T$ and $T'$ in ${\ensuremath{\mathcal{K}}}_i$ cannot share a constant except on: (i) a unique leaf of $T$ and the root of $T'$, as is the case for $v$ and $w$ in Figure \[fig:part\] or alternatively (ii) a unique leaf of $T$ and a unique leaf of $T'$. This case can happen when both leafs are connected to the root of a different tree $T''$, as is the situation for $w_2$ and $w_3$ in Figure \[fig:part\]. 

Therefore, for some sufficiently large constant $c' \in \mathbb{N}$, two nodes $v'$ and $v''$ in ${\ensuremath{\mathcal{K}}}_i$ of distance $c' m$ cannot have two elements of ${\ensuremath{\mbox{\textbf{{J}}}}}_i$ that are of distance $\leq m$ in ${\ensuremath{\Bbb{G}}}({\ensuremath{\mbox{\textbf{{J}}}}}_i)$. \[In fact, a careful analysis will show that $c' = 1$ is sufficient.\] Therefore, the locations of the constants in ${\ensuremath{\mbox{\textbf{{A}}}}}$ (resp.  ${\ensuremath{\mbox{\textbf{{B}}}}}$) cannot be “very far away” from the tuple $v$ (resp.  $w$).  In fact, if we set $c \geq c'$ (recall that $g = cm$) and consider the path $P$ between a tuple $t \in {\ensuremath{\mbox{\textbf{{A}}}}}$ and the constant $b_i$ (which belongs to $v$ and its parent), it cannot connect a root and a leaf of the same tree (i.e. through the body of the tree).  So, either it is completely contained in the tree of which $v$ is a leaf, or it has to alternate alternate between leafs and root several times, and then end in some tree.  In figure \[fig:part\], we may pick the following example $$v {\ensuremath{\rightarrow}}^* w_3 {\ensuremath{\rightarrow}}w_6 {\ensuremath{\rightarrow}}w_2 {\ensuremath{\rightarrow}}^* w_1 {\ensuremath{\rightarrow}}\ldots,$$ where we use the notation ${\ensuremath{\rightarrow}}^*$ to mean “path in the same tree”.  The same analysis can be applied to determine the locations of the tuples of ${\ensuremath{\mbox{\textbf{{B}}}}}$. Therefore, in order the ensure that properties 3 and 5 are satisfied, we just need to ensure that the height of each tree and the girth of ${\ensuremath{\mathcal{K}}}_i$ be large enough, which can be done by taking a sufficiently large $c$. When the girth (as ensured in the `copy` and `prune` procedures) is sufficiently large, we can be sure that no paths of length $\leq m$ exist between $v$ and $w$ in ${\ensuremath{\mathcal{K}}}_i$ \[In fact, a careful but tedious analysis shows that $c = 1$ is sufficient.\]

Theorem \[th:fin\_s\] also holds for infinite models, since even if the initial justification hierarchies are infinite, the proof method used is unchanged.  We thus also obtain finite controllability (every satisfiable formula is finitely satisfiable) for ${\ensuremath{\text{UCV}}}$.

The ${\ensuremath{\text{UCV}}}$ class of formulas is finitely controllable. 

Extending the View Definitions {#extend}
==============================

The previous section showed that the first order language using unary conjunctive view definitions is decidable.  A natural way to increase the power of the language is to make view bodies more expressive (but retain unary arity for the views).  We say earlier that allowing unary views to use disjunction in their definition does not actually increase expressiveness of the UCV language and hence this case is decidable.  Unfortunately, as we will show, employing other ways of extending the views results in satisfiability becoming undecidable. 

The first extension we consider is allowing inequality in the views, e.g.,

$V(x) \leftarrow R(x,y), S(x,x), x \neq y$

Call the first order language over such views the [*first order unary conjunctive$^{\neq}$ view language*]{}.  In fact, this language allows us to check whether a two counter machine computation is valid and terminates, which thus leads to the following result:

\[viewineq\] Satisfiability is undecidable for the first order unary conjunctive$^{\neq}$ view query language. 

The proof is by a reduction from the halting problem of two counter machines (2CM’s) starting with zero in the counters.  Given any description of a 2CM and its computation, we can show how to a) encode this description in database relations and b) define queries to check this description.  We construct a query which is satisfiable iff the 2CM halts.  The basic idea of the simulation is similar to one in [@LMSS92], but with the major difference that [*cycles are allowed*]{} in the successor relation, though there must be at least one good chain. 

A two-counter machine is a deterministic finite state machine with two non-negative counters.  The machine can test whether a particular counter is empty or non-empty.  The transition function has the form $$\delta: \; S \; \times \; \{=,>\} \; \times \; \{=,>\} \; \rightarrow \;
S \; \times \; \{pop,push\} \; \times \; \{pop,push\}$$ For example, the statement $\delta(4,=,>) \; = \; (2,push,pop)$ means that if we are in state 4 with counter 1 equal to 0 and counter 2 greater than 0, then go to state 2 and add one to counter 1 and subtract one from counter 2. 

The computation of the machine is stored in the relation $config(t,s,c_1,c_2)$, where $t$ is the time, $s$ is the state and $c_1$ and $c_2$ are values of the counters.  The states of the machine can be described by integers $0,1 \ldots
,h$ where 0 is the initial state and $h$ the halting (accepting) state.  The first configuration of the machine is $config(0,0,0,0)$ and thereafter, for each move, the time is increased by one and the state and counter values changed in correspondence with the transition function. 

We will use some relations to encode the computation of 2CMs starting with zero in the counters.  These are:

-   $S_0,\ldots,S_h$: each contains a constant which represents that particular state. 

-   $succ$: the successor relation.  We will make sure it contains one chain starting from $zero$ and ending at $last$ (but it may in addition contain unrelated cycles). 

-   $config$: contains computation of the 2CM. 

-   $zero$: contains the first constant in the chain in $succ$. This constant is also used as the number zero. 

-   $last$: contains the last constant in the chain in $succ$.

Note that we sometimes blur the distinction between unary relations and unary views, since a view $V$ can simulate a unary relation $U$ if it is defined by $V(x) \leftarrow U(x)$.\
The unary and nullary views (the latter can be eliminated using quantified unary views) are:

-   $halt$: true if the machine halts. 

-   $bad$: true if the database doesn’t correctly describe the computation of the 2CM. 

-   $dsucc$: contains all constants in $succ$.

-   $dT$: contains all time stamps in $config$.

-   $dP$: contains all constants in $succ$ with predecessors. 

-   $dCol_1, dCol_2$: are projections of the first and second columns of $succ$.

When defining the views, we also state some formulas (such as $hasPred$) over the views which will be used to form our first order sentence over the views. 

-   The “domain” views (those starting with the letter $d$) are easy to define, e.g.

    $dP(x) \leftarrow succ(z,x)$\
    $dCol_1(x) \leftarrow succ(x,y)$\
    $dCol_2(x) \leftarrow succ(y,x)$

-   $hasPred$ says “each nonzero constant in $succ$ has a predecessor:”

    $hasPred:$ $\forall x (dsucc(x) \Rightarrow (zero(x) \vee \ dP(x)))$

-   $sameDom$ says “the constants used in $succ$ and the timestamps in $config$ are the same set”:

    $sameDom:$ $\forall x (dsucc(x) \Rightarrow  dT(x)) \wedge
    \forall y (dT(y) \Rightarrow dsucc(y)))$

-   $goodzero$ says “the zero occurs in $succ$”:

    $goodzero:$ $\forall x (zero(x) \Rightarrow dsucc(x))$

-   $nempty$ : each of the domains and unary base relations is not empty

    $nempty:$ $\exists x (dsucc(x))$

-   Check that each constant in $succ$ has at most one successor and at most one predecessor and that it has no cycles of length 1. 

    $bad \leftarrow succ(x,y), succ(x,z), y \neq z$\
    $bad \leftarrow succ(y,x), succ(z,x), y \neq z$\
    $bad \leftarrow succ(x,x)$

    Note that the first two of these rules could be enforced by database style functional dependencies $x \rightarrow y$ and $y \rightarrow x$ on $succ$.

-   Check that every constant in the chain in succ which isn’t the last one must have a successor

    $hassuccnext:$ $\forall y (dCol_2(y) \Rightarrow (last(y) \vee dCol_1(y))$

-   Check that the last constant has no successor and zero (the first constant) has no predecessor. 

    $bad \leftarrow last(x), succ(x,y)$\
    $bad \leftarrow zero(x), succ(y,x)$

-   Check that every constant eligible to be in last and zero must be so. 

    $eligiblezero:$ $\forall y (dCol_1(y) \Rightarrow (dCol_2(y) \vee zero(y))$\
    $eligiblelast:$ $\forall y(dCol_2(y) \Rightarrow (dCol_1(y) \vee last(y)))$

-   Each $S_i$ and $zero$ and $last$ contain $\leq$ 1 element. 

    $bad \leftarrow S_i(x), S_i(y), x \neq y$\
    $bad \leftarrow zero(x), zero(y), x \neq y$\
    $bad \leftarrow last(x), last(y), x \neq y$

-   Check that $S_i,S_j
    ,last, zero$ are disjoint ($0 \leq i < j \leq h$):

    $bad \leftarrow zero(x), last(x)$\
    $bad \leftarrow S_i(x), S_j(x)$\
    $bad \leftarrow zero(x), S_i(x)$\
    $bad \leftarrow last(x), S_i(x)$

-   Check that the timestamp is the key for $config$. There are three rules, one for the state and two for the two counters; the one for the state is:

    $bad \leftarrow config(t,s,c_1,c_2),$$config(t,s',c'_1,c'_2), s \neq s'$

-   Check the configuration of the 2CM at time zero.  $config$ must have a tuple at $(0,0,0,0)$ and there must not be any tuples in config with a zero state and non zero times or counters. 

    $V_{z_s}(s)\!\leftarrow\!zero(t),\!config(t,s,x,y)$\
    $V_{z_{c_1}}(c)\!\leftarrow\!zero(t),\!config(t,x,c,y)$\
    $V_{z_{c_2}}(c)\!\leftarrow\!zero(t),\!config(t,x,y,c)$\
    $V_{y_s}(t)\!\leftarrow\!zero(s),\!config(t,s,x,y)$\
    $V_{y_{c_1}}(c_1)\!\leftarrow\!zero(s),\!config(t,s,c_1,x)$\
    $V_{y_{c_2}}(c_2)\!\leftarrow\!zero(s),\!config(t,s,x,c_2)$\
    $goodconfigzero:$ $\forall x (V_{z_s}(x) \Rightarrow S_0(x) \wedge $\
    `   `$(V_{z_{c_1}}(x) \vee V_{z_{c_2}}(x)
    \vee V_{y_s}(x) \vee V_{y_{c_1}}(x)
    \vee V_{y_{c_2}}(x)) \Rightarrow zero(x))$

-   For each tuple in $config$ at time $t$ which isn’t the halt state, there must also be a tuple at time $t+1$ in $config$.

    $V_1(t) \leftarrow config(t,s,c_1,c_2), S_h(s)$\
    $V_2(t) \leftarrow succ(t,t2), config(t2,s',c_1',c_2')$\
    $hasconfignext:$ $\forall t ((dt(t) \wedge \neg V_1(t)) \Rightarrow V_2(t))$

-   Check that the transitions of the 2CM are followed.  For each transition $\delta(j,>,=) = (k,pop,push)$, we include three rules, one for checking the state, one for checking the first counter and one for checking the second counter.  For the transition in question we have for checking the state

    $V_{\delta}(t') \leftarrow  config(t,s,c_1,c_2),
    succ(t,t'), S_j(s),succ(x,c_1),
    zero(c_2)$\
    $V_{\delta_s}(s) \leftarrow V_{\delta}(t), config(t,s,c_1,c_2)$\
    $goodstate_{\delta}:$ $\forall s (V_{\delta_s}(s) \Leftrightarrow S_k(s))$

    and for the first counter, we (i) find all the times where the transition is definitely correct for the first counter $$\begin{array}{@{}r@{~}l}
    Q_{1_\delta}(t') & \leftarrow  config(t,s,c_1,c_2),\\
    & \; \; \; succ(t,t'), S_j(s),succ(x,c_1),\\
    & \; \; \;  zero(c_2),succ(c_1'',c_1),config(t',s',c_1'',c_2') \mbox{\Large}
      \end{array}$$ (ii) find all the times where the transition may or may not be correct for the first counter $$Q_{2_\delta}(t') \leftarrow  config(t,s,c_1,c_2),
    succ(t,t'), S_j(s),succ(x,c_1),
    zero(c_2)
    $$ and make sure $Q_{1_\delta}$ and $Q_{2_\delta}$ are the same

    $goodtrans_{\delta_{c_1}}:$ $\forall t (Q_{1_{\delta}}(t) \Leftrightarrow Q_{2_{\delta}}(t))$

    Rules for second counter are similar. 

    For transitions $\delta_1, \delta_2, \ldots , \delta_k$, the combination can be expressed thus:

    $goodstate:$ $goodstate_{\delta_1} \wedge goodstate_{\delta_2}
    \wedge \ldots \wedge goodstate_{\delta_k}$\
    $goodtrans_{c_1}:$ $goodtrans_{\delta_{1_{c_1}}} \wedge goodtrans_{\delta_{2_{c_1}}}
    \wedge \ldots \wedge goodtrans_{\delta_{k_{c_1}}}$\
    $goodtrans_{c_2}:$ $goodtrans_{\delta_{1_{c_2}}} \wedge goodtrans_{\delta_{2_{c_2}}}
    \wedge \ldots \wedge goodtrans_{\delta_{k_{c_2}}}$

-   Check that halting state is in $config$.

    $hlt(t) \leftarrow config(t,s,c_1,c_2), S_h(s)$\
    $halt:$ $\exists x hlt(x)$

Given these views, we claim that satisfiability is undecidable for the query $\psi = \neg bad \wedge hasPred \wedge sameDom \wedge halt
\wedge goodzero \wedge goodconfigzero \wedge \wedge nempty \wedge hassuccnext
\wedge eligiblezero \wedge eligiblelast \wedge
 goodstate \wedge goodtrans_{c_1} \wedge goodtrans_{c_2} \wedge hasconfignext$

The second extension we consider is to allow “safe” negation in the conjunctive views, e.g.

$V(x) \leftarrow R(x,y), R(y,z), \neg R(x,z)$

Call the first order language over such views the [*first order unary conjunctive$^{\neg}$ view language*]{}.  It is also undecidable, by a result in [@BDR98]. 

[@BDR98] Satisfiability is undecidable for the first order unary conjunctive$^{\neg}$ view query language. 

A third possibility for increasing the expressiveness of views would be to keep the body as a pure conjunctive query, but allow views to have [*binary*]{} arity, [*e.g.*]{}

$V(x,y) \leftarrow R(x,y)$

This doesn’t yield a decidable language either, since this language has the same expressiveness as first order logic over binary relations, which is known to be undecidable [@BGG97]. 

Satisfiability is undecidable for the first order binary conjunctive view language. 

A fourth possibility is to use unary conjunctive views, but allow recursive view definitions.  e.g.

$V(x) \leftarrow edge(x,y)$\
$V(x) \leftarrow V(x) \wedge edge(y,x)$

Call this the first order unary conjunctive$^{rec}$ language.  This language is undecidable also. 

Satisfiability is undecidable for the first order unary conjunctive$^{rec}$ view language. 

(sketch): The proof of theorem \[viewineq\] can be adapted by removing inequality and instead using recursion to ensure there exists a connected chain in $succ$. It then becomes more complicated, but the main property needed is that $zero$ is connected to $last$ via the constants in $succ$. This can be expressed by

$conn\_zero(x) \leftarrow zero(x)$\
$conn\_zero(x) \leftarrow conn\_zero(y), succ(y,x)$\
$\exists x (last(x) \wedge conn\_zero(x))$

Applications {#sec:app}
============

Reasoning Over Ontologies
-------------------------

A currently active area of research is that of reasoning over ontologies (see e.g. [@DBLP:conf/iccs/Horrocks05]).  The aim here is to use decidable query languages used for accessing and reasoning about information and structure for the Semantic Web.  In particular, ontologies provide vocabularies which can define relationships or associations between various concepts (classes) and also properties that link different classes together.  Description logics are a key tool for reasoning over schemas and ontologies and to this end, a considerable number of different description logics have been developed.  To illustrate some reasoning over a simple ontology, we adopt an example from [@horr03], describing people, countries and some relationships.  This example can be encoded in a description logic such as $SHIQ$ and also in the UCV query language.  We show how to accomplish the latter. 

-   Define classes such as $Country, Person, Student$ and $Canadian$. These are just unary views defined over unary relations, e.g. $Country(x) \leftarrow country(x)$. Observe that we can blur the distinction between unary views and unary relations and use them interchangeably. 

-   State that $student$ is a subclass of $Person$. $$\forall x Student(x) \Rightarrow Person(x)$$

-   State that $Canada$ and $England$ are both instances of the class $Country$. To accomplish this in the UCV language, we could define $Canada$ and $England$ as unary views and ensure that they are contained in the $Country$ relation and are disjoint with all other classes/instances. 

-   Declare $Nationality$ as a property relating the classes $Person$ (its domain) and $Country$ (its range).  In the UCV language, we could model this as a binary relation $Nationality(x,y)$ and impose constraints on its domain and range.  e.g.

    $dom\_Nationality(x) \leftarrow Nationality(x,y)$\
    $range\_Nationality(y) \leftarrow Nationality(x,y)$\
    $\forall x (dom\_Nationality(x) \Rightarrow Person(x))$\
    $\forall x (range\_Nationality(x) \Rightarrow Country(x))$\

-   State that $Country$ and $Person$ are disjoint classes.  $\forall x (Country(x) \Rightarrow \neg Person(x))$.

-   Assert that the class $Stateless$ is defined precisely as those members of the class $Person$ that have no values for the property $Nationality$.

    $has\_Nationality(x) \leftarrow Nationality(x,y)$\
    $Stateless (x) \Leftrightarrow Person(x) \wedge \neg has\_Nationality(x)$\

The above types of statements are reasonably simple to express.  In order to achieve more expressiveness, property chaining and property composition have been identified as important reasoning features.  To this end, integration of rule-based KR and DL-based KR is an active area of research.  The UCV query language has the advantage of being able to express certain types of property chaining, which would not be expressible in the description logic SHIQ, which is not able to accomplish chaining [@horr03].  For example

-   An uncle is precisely a parent’s brother. 

    $uncle_1(z) \leftarrow parent(x,y), brother(x,z)$\
    $uncle_2(z) \leftarrow parent(x,y), brother(z,x)$\
    $uncle(z) \Leftrightarrow uncle_1(z) \vee uncle_2(z)$\

We consequently believe the UCV query language has some intriguing potential to be used as a reasoning component for ontologies, possibly to supplement description logics for some specialized applications.  We leave this as an open area for future investigation. 

Containment and Equivalence
---------------------------

We now briefly examine the application of our results to query containment.  Theorem \[th:fin\_s\] implies we can test whether $Q_1(x) \subseteq Q_2(x)$ under the constraints $C_1 \wedge C_2 \ldots \wedge C_n$ where $Q_1, Q_2, C_1, \ldots, C_n$ are all first order unary conjunctive view queries in 2-NEXPTIME.  This just amounts to testing whether the sentence $\exists x (Q_1(x) \wedge \neg Q_2(x))  \wedge
C_1 \wedge \ldots \wedge C_n$ is unsatisfiable.  Equivalence of $Q_1(x)$ and $Q_2(x)$ can be tested with containment tests in both directions. 

Of course, we can also show that testing the containment $Q_1 \subseteq Q_2$ is undecidable if $Q_1$ and $Q_2$ are first order unary conjunctive view$^{\neq}$ queries, first order unary conjunctive view$^{\neg}$ queries and first order unary conjunctive$^{rec}$ view queries. 

Containment of queries with negation was first considered in [@SY80].  There it was essentially shown that the problem is decidable for queries which do not apply projection to subexpressions with difference.  Such a language is disjoint from ours, since it cannot express a sentence such as $ \exists y V_4(y) \wedge
\neg\exists x (V_1(x) \wedge
\neg V_2(x))$ where $V_1$ and $V_2$ are views defined over several variables. 

Inclusion Dependencies
----------------------

Unary inclusion dependencies were identified as useful in [@CKV90].  They take the form $R[x] \subseteq S[y]$. If we allow $R$ and $S$ above to be unary conjunctive view queries, we could obtain [*unary conjunctive view containment dependencies*]{}.  Observe that the unary views are actually unary projections of the join of one or more relations. 

We can also define a special type of dependency called a [*proper*]{} first order unary conjunctive inclusion dependency, having the form $Q_1(x) \subset Q_2(x)$, where $Q_1$ and $Q_2$ are first order unary conjunctive view queries with one free variable.  If $\{d_1, \ldots, d_k\}$ is a set of such dependencies, then it is straightforward to test whether they imply another dependency $d_x$, by testing the satisfiability of an appropriate first order unary conjunctive view query. 

\[implication\] Implication for the class of unary conjunctive view containment dependencies with subset and proper subset operators is i) decidable in 2-NEXPTIME and ii) finitely controllable. 

The results from [@CKV90] show that implication is decidable in polynomial time, but not finitely controllable, for either of the combinations i) functional dependencies plus unary inclusion dependencies, ii) full implication dependencies plus unary inclusion dependencies.  In contrast, the stated complexity in the above theorem is much higher, due to the increased expressiveness of the dependencies, yet interestingly the class is finitely controllable. 

We might also consider unary conjunctive$^{\neq}$ containment dependencies.  The tests in the proof of theorem \[viewineq\] for the 2CM can be written in the form $Q_1(x) \subseteq Q_2(x)$, with the exception of the non-emptiness constraints, which must use the proper subset operator.  Interestingly also, we can see from the proof of theorem \[viewineq\], that adding the ability to express functional dependencies would also result in undecidability.  We can summarise these observations in the following theorem and its corollary. 

Implication is undecidable for unary conjunctive$^{\neq}$ (or conjunctive$^{\neg}$) view containment dependencies with the subset and the proper subset operators. 

Implication is undecidable for the combination of unary conjunctive view containment dependencies plus functional dependencies. 

 Active Rule Termination
------------------------

The languages in this paper have their origins in [@BDR98], where active database rule languages based on views were studied.  The decidability result for first order unary conjunctive views can be used to positively answer an open question raised in [@BDR98], which essentially asked whether termination is decidable for active database rules expressed using unary conjunctive views. 

Expressive Power of the UCV Language {#sec:expressive}
====================================

As we have seen in the previous sections, the logic ${\ensuremath{\text{UCV}}}$ is quite suitable to reason about hereditary information such as “$x$ is a grandchild of $y$” over family trees.  This is due to the fact that ${\ensuremath{\text{UCV}}}$ can express the existence of a directed walk of length $k$ in the graph, for any fixed positive integer $k$. Therefore, it is natural to also ask what is inexpressible in the logic.  In this section, we describe a game-theoretic technique for proving inexpressibility results for ${\ensuremath{\text{UCV}}}$. First, we show an easy adaptation of [Ehrenfeucht-Fraïssé]{}$\;$ games for proving that a boolean query is inexpressible in ${\ensuremath{\text{UCV}}}(\sigma,{\ensuremath{\mathcal{V}}})$ for a signature $\sigma$ and a finite view set ${\ensuremath{\mathcal{V}}}$ over $\sigma$. Second, we extend this result for proving that a boolean query is inexpressible in ${\ensuremath{\text{UCV}}}(\sigma)$. An inexpressibility result of the second kind is clearly more interesting, as it is independent of our choice of the view set ${\ensuremath{\mathcal{V}}}$ over $\sigma$. Moreover, such a result places an ultimate limit of what can be expressed by UCV queries.  Although it can be adapted to any class ${\ensuremath{\mathcal{C}}}$ of structures, we shall only state our theorem for proving inexpressibility results in ${\ensuremath{\text{UCV}}}$ *over all finite structures*.  For this section only, we shall use $STRUCT(\sigma)$ to denote the set of all *finite* $\sigma$-structures. 

Our first goal is quite easy to achieve.  Recall that each view set ${\ensuremath{\mathcal{V}}}$ over $\sigma$ induces a mapping $\Lambda: STRUCT(\sigma) {\ensuremath{\rightarrow}}STRUCT({\ensuremath{\mathcal{V}}})$ as defined in section \[sec:prelim\]. 

Let ${\ensuremath{\mbox{\textbf{{A}}}}}, {\ensuremath{\mbox{\textbf{{B}}}}} \in STRUCT(\sigma)$. Define the function $\Lambda:
STRUCT(\sigma) {\ensuremath{\rightarrow}}STRUCT({\ensuremath{\mathcal{V}}})$. Then, the following statements are equivalent:

1.   ${\ensuremath{\mbox{\textbf{{A}}}}}$ and ${\ensuremath{\mbox{\textbf{{B}}}}}$ agree on ${\ensuremath{\text{UCV}}}(\sigma,{\ensuremath{\mathcal{V}}})$.

2.   $\Lambda({\ensuremath{\mbox{\textbf{{A}}}}}) \equiv_1^{{\ensuremath{\text{UFO}}}({\ensuremath{\mathcal{V}}})} \Lambda({\ensuremath{\mbox{\textbf{{B}}}}})$ (i.e. they agree on ${\ensuremath{\text{UFO}}}({\ensuremath{\mathcal{V}}})$ formulas of quantifier rank 1. 

Immediate from lemma \[lm:unaryform\], and lemma \[lem:realize\]. 

So, to prove that a boolean query ${\ensuremath{\mathcal{Q}}}$ is not expressible in ${\ensuremath{\text{UCV}}}(\sigma,{\ensuremath{\mathcal{V}}})$, it suffices to find two $\sigma$-structures such that $\Lambda({\ensuremath{\mbox{\textbf{{A}}}}}) \equiv_1^{{\ensuremath{\text{UFO}}}({\ensuremath{\mathcal{V}}})} \Lambda({\ensuremath{\mbox{\textbf{{B}}}}})$, but ${\ensuremath{\mbox{\textbf{{A}}}}}$ and ${\ensuremath{\mbox{\textbf{{B}}}}}$ do not agree on ${\ensuremath{\mathcal{Q}}}$. In turn, to show that $\Lambda({\ensuremath{\mbox{\textbf{{A}}}}}) \equiv_1^{{\ensuremath{\text{UFO}}}({\ensuremath{\mathcal{V}}})} \Lambda({\ensuremath{\mbox{\textbf{{B}}}}})$, we can use Ehrenfeucht-Fraïsse games. 

We now turn to the second task.  Let us begin by stating an obvious corollary of the preceding theorem. 

Let ${\ensuremath{\mbox{\textbf{{A}}}}}, {\ensuremath{\mbox{\textbf{{B}}}}} \in STRUCT(\sigma)$. For any view set ${\ensuremath{\mathcal{V}}}$, define the function $\Lambda^{{\ensuremath{\mathcal{V}}}}: STRUCT(\sigma) {\ensuremath{\rightarrow}}STRUCT({\ensuremath{\mathcal{V}}})$. Then, the following statements are equivalent:

1.   ${\ensuremath{\mbox{\textbf{{A}}}}}$ and ${\ensuremath{\mbox{\textbf{{B}}}}}$ agree on ${\ensuremath{\text{UCV}}}(\sigma)$.

2.   For any view set ${\ensuremath{\mathcal{V}}}$ over $\sigma$, we have $\Lambda^{{\ensuremath{\mathcal{V}}}}({\ensuremath{\mbox{\textbf{{A}}}}}) \equiv_1^{{\ensuremath{\text{UFO}}}({\ensuremath{\mathcal{V}}})} \Lambda^{{\ensuremath{\mathcal{V}}}}({\ensuremath{\mbox{\textbf{{B}}}}})$

\[cor:inexpr1\]

This corollary is not of immediate use.  Namely, checking the second statement is a daunting task, as there are infinitely many possible view sets ${\ensuremath{\mathcal{V}}}$ over $\sigma$. Instead, we shall propose a sufficient condition for this, which employs the easy direction of the well-known homomorphism preservation theorem (see [@Hodg97]). 

A formula $\phi$ over a vocabulary $\sigma$ is said to be [preserved under homomorphisms]{}, if for any ${\ensuremath{\mbox{\textbf{{A}}}}}, {\ensuremath{\mbox{\textbf{{B}}}}} \in
    STRUCT(\sigma)$ the following statement holds: whenever ${\ensuremath{\mbox{\textbf{{a}}}}} {\ensuremath{\overset{\mbox{\tiny def}}{=}}}(a_1,\ldots,a_m) \in
    \phi({\ensuremath{\mbox{\textbf{{A}}}}})$ and $h$ is a homomorphism from ${\ensuremath{\mbox{\textbf{{A}}}}}$ to ${\ensuremath{\mbox{\textbf{{B}}}}}$, it is the case that $h({\ensuremath{\mbox{\textbf{{a}}}}}) {\ensuremath{\overset{\mbox{\tiny def}}{=}}}(h(a_1),\ldots,h(a_m)) \in
    \phi({\ensuremath{\mbox{\textbf{{B}}}}})$.

Conjunctive queries are preserved under homomorphisms.  \[lm:homom\]

Let ${\ensuremath{\mbox{\textbf{{A}}}}}, {\ensuremath{\mbox{\textbf{{B}}}}} \in STRUCT(\sigma)$. To prove that $\Lambda({\ensuremath{\mbox{\textbf{{A}}}}}) \equiv_1^{{\ensuremath{\text{UFO}}}({\ensuremath{\mathcal{V}}})} \Lambda({\ensuremath{\mbox{\textbf{{B}}}}})$ for all $\sigma$-view sets ${\ensuremath{\mathcal{V}}}$, it is sufficient to show that

1.   For every $a \in A$, there exists a homomorphism $h$ from ${\ensuremath{\mbox{\textbf{{A}}}}}$ to ${\ensuremath{\mbox{\textbf{{B}}}}}$ and a homomorphism $g$ from ${\ensuremath{\mbox{\textbf{{B}}}}}$ to ${\ensuremath{\mbox{\textbf{{A}}}}}$ such that $g(h(a)) = a$.

2.   For every $b \in B$, there exists a homomorphism $h$ from ${\ensuremath{\mbox{\textbf{{A}}}}}$ to ${\ensuremath{\mbox{\textbf{{B}}}}}$ and a homomorphism $g$ from ${\ensuremath{\mbox{\textbf{{B}}}}}$ to ${\ensuremath{\mbox{\textbf{{A}}}}}$ such that $h(g(b)) = b$.

\[thm:homom\]

Take an arbitrary $\sigma$-view set ${\ensuremath{\mathcal{V}}}$. We use Ehrenfeucht-Fraïsse game argument.  Suppose Spoiler places a pebble on an element $a$ of $\Lambda({\ensuremath{\mbox{\textbf{{A}}}}})$, whose domain is $A$.  Then, the first assumption tells us that there exist homomorphisms $h: A {\ensuremath{\rightarrow}}B$ and $g: B {\ensuremath{\rightarrow}}A$ such that $g(h(a)) = a$. Duplicator may respond by placing the other pebble from the same pair on the element $h(a)$ of $\Lambda({\ensuremath{\mbox{\textbf{{B}}}}})$. To show this, we need to prove that $a \mapsto h(a)$ defines an isomorphism between the substructures of $\Lambda({\ensuremath{\mbox{\textbf{{A}}}}})$ and $\Lambda({\ensuremath{\mbox{\textbf{{B}}}}})$ induced by, respectively, the sets $\{a\}$ and $\{h(a)\}$. Let $V \in {\ensuremath{\mathcal{V}}}$. It is enough to show that $a \in V({\ensuremath{\mbox{\textbf{{A}}}}})$ iff $h(a) \in V({\ensuremath{\mbox{\textbf{{B}}}}})$. If $a \in V({\ensuremath{\mbox{\textbf{{A}}}}})$, then we have $h(a) \in V({\ensuremath{\mbox{\textbf{{B}}}}})$ by lemma \[lm:homom\].  Similarly, if $h(a) \in V({\ensuremath{\mbox{\textbf{{B}}}}})$, theorem \[lm:homom\] implies that $a = g(h(a)) \in V({\ensuremath{\mbox{\textbf{{A}}}}})$.

For the case where Spoiler plays an element of ${\ensuremath{\mbox{\textbf{{B}}}}}$, we can use the same argument with the aid of the second assumption above.  In either case, we have $\Lambda({\ensuremath{\mbox{\textbf{{A}}}}}) \equiv_1 \Lambda({\ensuremath{\mbox{\textbf{{B}}}}})$.

This theorem allows us to give easy inexpressibility proofs for a variety of first-order queries.  We now give three easy inexpressibility proofs for first-order queries over directed graphs (i.e. structures with one binary relation $E$). 

We show that the formula $SYM \equiv \forall x,y(E(x,y) {\ensuremath{\leftrightarrow}}E(y,x))$ accepting graphs with symmetric $E$ is not expressible in ${\ensuremath{\text{UCV}}}(\sigma)$. To do this, consider the graphs ${\ensuremath{\mbox{\textbf{{A}}}}}$ and ${\ensuremath{\mbox{\textbf{{B}}}}}$ defined as follows

Obviously, the graph $E^{{\ensuremath{\mbox{\textbf{{A}}}}}}$ is symmetric, while $E^{{\ensuremath{\mbox{\textbf{{B}}}}}}$ is not.  Consider the functions $h_1,h_2: A {\ensuremath{\rightarrow}}B$ and $g: B {\ensuremath{\rightarrow}}A$ defined as

-   $h_1(a) = h_1(c) = a$ and $h_1(b) = h_1(d) = b$,

-   $h_2(a) = h_2(c) = c$ and $h_2(b) = h_2(d) = d$, and

-   for $i \in B$, $g(i) = i$.

It is easy to verify that $h_1$ and $h_2$ are homomorphisms from ${\ensuremath{\mbox{\textbf{{A}}}}}$ to ${\ensuremath{\mbox{\textbf{{B}}}}}$, whereas $g$ a homomorphism from ${\ensuremath{\mbox{\textbf{{B}}}}}$ to ${\ensuremath{\mbox{\textbf{{A}}}}}$. Now, for $x \in \{a,b\}$, we have $g(h_1(x)) = x$ and $h_1(g(x)) = x$. For $x \in \{c,d\}$, we have $g(h_2(x)) = x$ and $h_2(g(x)) = x$. So, by theorem \[thm:homom\] and corollary \[cor:inexpr1\], we conclude that $SYM$ is not expressible in ${\ensuremath{\text{UCV}}}(\sigma)$ over all finite directed graphs. 

We now show that the transitivity query $$TRANS \equiv \forall x,y,z( E(x,y) \wedge E(y,z) {\ensuremath{\rightarrow}}E(x,z) )$$ is not expressible in ${\ensuremath{\text{UCV}}}(\sigma)$. To do this, consider the graphs ${\ensuremath{\mbox{\textbf{{A}}}}}$ and ${\ensuremath{\mbox{\textbf{{B}}}}}$ defined as

It is obvious that ${\ensuremath{\mbox{\textbf{{A}}}}} \models TRANS$, and it is not the case that ${\ensuremath{\mbox{\textbf{{B}}}}} \models TRANS$. Consider the homomorphisms $h_1, h_2$ from ${\ensuremath{\mbox{\textbf{{A}}}}}$ to ${\ensuremath{\mbox{\textbf{{B}}}}}$, and the homomorphism $g$ from ${\ensuremath{\mbox{\textbf{{B}}}}}$ to ${\ensuremath{\mbox{\textbf{{A}}}}}$ defined as

-   for $i \in A$, $h_1(i) = i$;

-   for $i \in A$, $h_2(i) = i+3$; and

-   for $i \in B$, $g(i) = i \bmod{3}$.

Then, for $i \in A$, we have $g(h_1(i)) = i$. Conversely, suppose that $i \in B$. If $i = 0,1,2$, then $h_1(g(i)) = i$. Similarly, if $i = 3,4,5$, then $h_2(g(i)) = i$. So, by theorem \[thm:homom\] and corollary \[cor:inexpr1\], transitivity is not expressible in ${\ensuremath{\text{UCV}}}(\sigma)$ over finite directed graphs. 

The query $\forall x,y E(x,y)$ is also not expressible in ${\ensuremath{\text{UCV}}}(\sigma)$. It is easy to apply theorem \[thm:homom\] and corollary \[cor:inexpr1\] on the following graphs to verify this fact. 

Related Work {#sec:related}
============

Satisfiability of first order logic has been thoroughly investigated in the context of the classical decision problem [@BGG97].  The main thrust there has been determining for which quantifier prefixes first order languages are decidable.  We are not aware of any result of this type which could be used to demonstrate decidability of the first order unary conjunctive view language.  Instead, our result is best classified as a new decidable class generalising the traditional decidable unary first-order language (the Löwenheim class [@lowenheim]).  Use of the Löwenheim class itself for reasoning about schemas is described in [@Th96], where applications towards checking intersection and disjointness of object oriented classes are given. 

As observed earlier, description logics are important logics for expressing constraints on desired models.  In [@CDL98], the query containment problem is studied in the context of the description logic ${\cal DLR}_{reg}$. There are certain similarities between this and the first order (unary) view languages we have studied in this paper.  The key difference appears to be that although ${\cal DLR}_{reg}$ can be used to define view constraints, these constraints cannot express unary conjunctive views (since assertions do not allow arbitrary projection).  Furthermore, ${\cal DLR}_{reg}$ can express functional dependencies on a single attribute, a feature which would make the UCV language undecidable (see proof of theorem \[viewineq\]).  There is a result in [@CDL98], however, showing undecidability for a fragment of ${\cal DLR}_{reg}$ with inequality, which could be adapted to give an alternative proof of theorem \[viewineq\] (although inequality is used there in a slightly more powerful way). 

Another interesting family of decidable logics are guarded logics.  The Guarded Fragment [@guarded98] and the Loosely Guarded Fragment [@bentham97] are both logics that have the finite model property [@DBLP:journals/sLogica/Hodkinson02].  The philosophy of UCV is somewhat similar to these guarded logics, since the decidability of UCV also arises from certain restrictions on quantifier use.  In terms of expressiveness though, guarded logics seem distinct from UCV formulas, not being able to express cyclic views, such as $\exists x (V(x))$, where $V(x) \leftarrow R(x,y), R(y,z), R(z,z'), R(z',x)$.

Another area of work that deals with complexity of views is the view consistency problem, with results given in [@AD98].  This involves determining whether there exists an underlying database instance that realises a [*specific*]{} (bounded) view instance .  The problem we have focused on in this paper is slightly more complicated; testing satisfiability of a first order view query asks the question whether there exists an ([*unbounded*]{}) view instance that makes the query true.  This explains how satisfiability can be undecidable for first order unary conjunctive$^{\neq}$ view queries, but view consistency for non recursive datalog$^{\neq}$ views is in $NP$. Monadic views have been recently examined in [@DBLP:conf/icdt/NashSV07], where they were shown to exhibit nice properties in the context of answering and rewriting conjunctive queries using only a set of views.  This is an interesting counterpoint to the result of this paper, which demonstrate how monadic views can form the basis of a decidable fragment of first order logic. 

Summary and Further work {#sec:summary}
========================

In this paper, we have introduced a new decidable language based on the use of unary conjunctive views embedded within first order logic.  This is a powerful generalisation of the well known fragment of first order logic using only unary relations (the Löwenheim class).  We also showed that our new class is maximal, in the sense that increasing the expressivity of views is not possible without undecidability resulting.  Table 1 provides a summary of our decidability results.  Note that the Unary Conjunctive$^{\cup}$ View language corresponds to the extension of ${\ensuremath{\text{UCV}}}$ by allowing disjunction in the view definition.  We feel that the decidable case we have identified, is sufficiently natural and interesting to be of practical, as well as theoretical interest. 

[Table 1:\
Summary of Decidability Results for First Order View Languages]{}\

  Unary Conjunctive View            Decidable
  --------------------------------- ----------------------
  Unary Conjunctive$^{\cup}$ View   Decidable
  Unary Conjunctive$^{\neq}$ View   Undecidable
  Unary Conjunctive$^{rec}$ View    Undecidable
  Unary Conjunctive$^{\neg}$ View   Undecidable [@BDR98]
  Binary Conjunctive View           Undecidable

\[summary-table\]

An interesting open problem for future work is to investigate the decidability of an extension to the first order unary conjunctive view language, when equality is allowed to be used outside of the unary views (i.e. included in the first order part).  An example formula in this new language is\
$$\forall X,Y (V_1(X) \wedge V_2(Y) \Rightarrow X \neq Y)$$

We conjecture this extended language is decidable, but do not currently have a proof. 

For other future work, we believe it would be worthwhile to investigate relationships with description logics and also examine alternative ways of introducing negation into the UCV language.  One possibility might be to allow views of arity zero to specify description logic like constraints, such as $R_1(x,y)
\subseteq R_2(x,y)$.

Finally, there is still an exponential gap between the upper bound complexity of 2-NEXPTIME and lower bound complexity of NEXPTIME-hardness that we derived.  The primary reason for this exponential blow-up is the enumeration of all subviews of the views that are present in the formula, which we need for the proof. 

We thank Sanming Zhou for pointing out useful references on extremal graph theory.  We are grateful to Leonid Libkin for his comments on a draft of this paper. 

[^1]: A preliminary version of this paper appeared in [@DBLP:conf/icdt/BaileyD99]

[^2]: More generally, views may be any existential formulas with one free variable, since this can be rewritten into a disjunction of conjunctive formulas with one free variable. 

[^3]: Although it is common in mathematical logic to use the term “constants” to mean the interpretation of constant symbols in the structure, no confusion shall arise in this article, as we assume the absence of constant symbols in the vocabulary.  Our results, nevertheless, easily extend to vocabularies with constant symbols. 

[^4]: The disjoint union of two $\sigma$-structures ${\ensuremath{\mbox{\textbf{{A}}}}}$ and ${\ensuremath{\mbox{\textbf{{B}}}}}$ with $A \cap B = \emptyset$ is the structure with universe $A \cup B$ and relation $R$ interpreted as $R^{{\ensuremath{\mbox{\textbf{{A}}}}}}\cup R^{{\ensuremath{\mbox{\textbf{{B}}}}}}$. If $A \cap B \neq \emptyset$, one can simply force disjointness by renaming constants. 

[^5]: node of the same tree and level
