Tractability Frontier of Data Complexity in Team Semantics
Arnaud Durand\thanks{Institut de Math\'ematiques de Jussieu - Paris Rive Gauche
CNRS UMR 7586 - Universit\'e Paris Diderot
France. durand@math.univ-paris-diderot.fr
Arnaud Durand \institute{IMJ-PRG
CNRS UMR 7586
Universit\'e Paris-Diderot
France
We study the data complexity of model-checking for logics with team semantics. For dependence and independence logic, we completely characterize the tractability/intractability frontier of data complexity of both quantifier-free and quantified formulas. For inclusion logic formulas, we reduce the model-checking problem to the satisfiability problem of so-called Dual-Horn propositional formulas. Via this reduction, we give an alternative proof for the recent result showing that the data complexity of inclusion logic is in PTIME.
dependence_independence.tex

\section{Dependence and independence logics}%
%In the rest of this article, due to lack of space,  the full proofs of selected results can only be found in the Appendix.
%Due to lack of space,  the full proofs of some results can only be found in the Appendix.
In this section we consider the complexity of model-checking for quantifier-free and quantified  formulas of dependence and independence logic. 

\subsection{The case of quantifier-free formulas}
In this section we consider the complexity of model-checking for quantifier-free formulas of dependence and independence logic. For dependence logic the problem has  already been essentially settled in \cite{kontinenj13}.  The following theorems delineate a clear barrier between tractability and intractability for quantifier-free dependence logic formulas.
%known about the data complexity of the model cheking problem for formulas in $\df$. 
\begin{theorem}[\cite{kontinenj13}]\label{JarmoKontinenNL} The model checking problem for formula $\dep(x,y)\vee \dep(z,v)$ is $\nl$-complete. More generally, the model-checking for $\varphi \vee \psi$ where $\varphi$ and $\psi$ are $2$-coherent quantifier-free formulas of $\df$ is always in $\nl$.
\end{theorem}

When  two disjunctions can be used, the model checking problem becomes intractable as shown by the following results.

\begin{theorem}[\cite{kontinenj13}]\label{JarmoKontinenNP}
The model checking problem for formula $\dep(x,y)\vee \dep(z,v) \vee \dep(z,v)$ is $\np$-complete.
\end{theorem}


%We will show below that the formula above is in some sense optimal. We start with the following result which essentially shows that two independence atoms  are not enough to express $\np$-complete problems. 
%\arnaud{The result below will supersede Proposition \ref{2 disjunction Indep} and \ref{2 disjunction Indep bis}}

In order to give a syntactic analogue of  Theorem \ref{JarmoKontinenNL}, we define next the disjunction-width of a formula. % The type of a formula $\varphi$, denoted $\type{\varphi}$, is 1 if $\varphi$ contain at least one "dependence" atom i.e. is not purely first-order . 


\begin{definition} Let $\sigma$ be a relational signature. The disjunction-width of a $\sigma$-formula $\varphi$, denoted $\Disjunctiondepth{\varphi}$, is defined as follows:
\[
\Disjunctiondepth{\varphi}=
\left\{\begin{array}{l}
1  \mbox{ if } \varphi  \mbox{ is } \indep{\tu y}{\tu x }{\tu z} \mbox{ or }  \dep(\tu x, y) \mbox{ or } \tu x\subseteq \tu y\\
0   \mbox{ if } \varphi \mbox{ is } R(\tu x)  \mbox{ or }   \neg R(\tu x),    \mbox{ for } R\in \sg\cup\{=\}\\
\max (\Disjunctiondepth{\varphi_1}, \Disjunctiondepth{\varphi_2}) \mbox{ if } \varphi \mbox{ is } \varphi_1\wedge\varphi_2 \\
\Disjunctiondepth{\varphi_1} + \Disjunctiondepth{\varphi_2} \mbox{ if } \varphi \mbox{ is } \varphi_1\vee\varphi_2 \\
\Disjunctiondepth{\varphi_1}  \mbox{ if } \varphi \mbox{ is } \exists x \varphi_1 \mbox{ or } \forall \varphi_1.
\end{array}\right.
\]
\end{definition}

The next theorem  is a syntactically defined analogue of Theorem  \ref{JarmoKontinenNL}.
\begin{proposition}\label{disjunction depth 2}
The data complexity of  model-checking of quantifier-free $\df$-formulas  $\phi$ with $\Disjunctiondepth{\phi} \leq 2$ is in  $\nl$.
\end{proposition}

\begin{proof} We will first show that a formula  $\phi$ with $\Disjunctiondepth{\phi} =1$ is $2$-coherent.
 This follows by induction using the following facts \cite{kontinenj13}: 
 \begin{itemize}
\item dependence atoms are $2$-coherent, and first-order formulas are $1$-coherent,
\item if $\psi$ is $k$-coherent, then $\psi\vee \phi$ is also $k$-coherent assuming  $\phi$ is first-order,
\item  if   $\psi$ is $k$-coherent and  $\phi$ is $k\le j$-coherent, then  $\psi\wedge \phi$ is $j$-coherent.
\end{itemize}
It is also straightforward to check that the data complexity of a formula  $\phi$ with $\Disjunctiondepth{\phi} =1$ is in Logspace (the formula $\phi$ can be  expressed in FO assuming the team $X$ with domain $\tu x=\Fr(\phi)$ is represented by the $n$-ary relation $X(\tu x)$). We will complete the  proof using induction on $\varphi$ with  
 $\Disjunctiondepth{\phi} = 2$.  Suppose that  $\varphi=\psi\vee \phi$, where  $\Disjunctiondepth{\psi}= \Disjunctiondepth{\phi} = 1$. Then the claim follows by Theorem  \ref{JarmoKontinenNL}. The case $\varphi=\psi\wedge \phi$ is also clear. Suppose finally  that $\varphi=\psi\vee \phi$, where $\phi$ is first-order. Note that by downward closure 
 $$\mA\models_X \varphi \Leftrightarrow  \mA\models_{X'}\psi,$$
where $X'=\{ s\in X \ |\ \mA\not \models_s \phi \}$. Now since $X'$ can be computed in Logspace,  the model-checking problem of $\phi$ can be decided in NL by the induction assumption for $\psi$. %Finally assume that   $\varphi=\psi\vee \phi$, where  $\Disjunctiondepth{\psi}= \Disjunctiondepth{\phi} = 1$. A simple induction shows that the formulas $\psi$ and  $\phi$ 2-coherent using the facts that  
\end{proof}


In this section we examine potential  analogues of Theorems \ref{JarmoKontinenNL} and \ref{JarmoKontinenNP} for  independence logic. It is well-known that the dependence atom $\dep(\tu x,y)$ is logically equivalent to the independence atom $ \indep{y}{\tu x}{y}$. Hence, the following is immediate from Theorem~\ref{JarmoKontinenNP} \cite{kontinenj13}.
%an immediate corollary of Theorem~\ref{JarmoKontinenNP}.

\begin{corollary}\label{3 disjunction relativized independance}
The model checking problem for formula 
\[\indep{y}{x}{y}\vee \indep{v}{z}{v} \vee \indep{v}{z}{v}\]
 is $\np$-complete.
\end{corollary}
For independence logic, the situation is not as clear, in particular  concerning tractability.
 In the following we will exhibit a fragment of independence logic whose data complexity is in $\nl$ and which is in some sense the maximal such fragment.  

\newcommand{\bcindepfo}{\mathsf{BC}(\bot,\fo)}
\newcommand{\CCm}{\mathfrak{C}^{-}}
\newcommand{\CCp}{\mathfrak{C}^{+}}

\begin{definition} The Boolean closure of an independence atom by first-order formulas, 
denoted $\bcindepfo$, is defined as follows:

\begin{itemize} 
\item Any independence atom $\indep{\tu x}{\tu y}{\tu z}$ is in $\bcindepfo$.

\item If $\varphi\in \bcindepfo$, then for any formula $\phi\in \fo$, $\varphi \wedge \phi$ and $\varphi\vee \phi$ are in $\bcindepfo$. 
\end{itemize}
\end{definition}


Let $\varphi\in \bcindepfo$. Up to permutation of disjunction and conjunction, $\varphi$ can be put into the following normalized form:

\[
\varphi\equiv ((\dots ((\indep {\tu x}{\tu z}{\tu y} \wedge \phi_1) \vee \psi_1)\wedge \dots ) \wedge \phi_k) \vee \psi_k
\]

Let $\mA$ be any structure, $\CCp=\bigcap_{i=1}^k \phi_i(\mA)$ and $\CCm=\bigcup_{i=1}^k \psi_i(\mA)$, where, $\phi_i(\mA)$
is the set of assignments $s\colon \Fr(\varphi)\rightarrow A$ such that
$\mA \models_s \phi_i$. We can restate the fundamental property for satisfiability of an independence atom in a team (and a structure) to tackle the case of $\bcindepfo$ formulas. It holds that, for any $\varphi\in\bcindepfo$, any team $X$ and structure $\mA$, $\mA\models_X\varphi$ if and only if: 

\begin{itemize}

	 \item for all $s\in X$: either $s\in [((..(\psi_1\wedge \phi_2) \vee \dots ) \wedge \phi_k) \vee \psi_k](\mA)$ or $s\in\CCp$, $s\not\in\CCm$ and 
 
 
\item  for all $s_1,s_2\in X$ such that $s_1,s_2\in \CCp$, $s_1,s_2\not\in \CCm$, and $s_1(\tu z)=s_2(\tu z)$,  there exists $s_3\in X$ such that: $s_3(\tu z)=s_1(\tu z), s_3(\tu x)=s_1(\tu x) \mbox{ and } s_3(\tu y)=s_2(\tu y)$. 

%\[
%s_3(\tu z)=s_1(\tu z), s_3(\tu x)=s_1(\tu x) \mbox{ and } s_3(\tu y)=s_2(\tu y). 
% \]

\end{itemize}


The first item is true by exhaustive case distinction. The second one comes from the fact that if a tuple $s$ satisfies  $s\in\CCp$ and  $s\not\in\CCm$  then it is forced to be in the sub-team satisfying $\indep{\tu x}{\tu z}{\tu y}$.  

In the rest of the paper, assignments $s_1,s_2$ as in the second item will be said \textit{compatible} for formula $\varphi$ and team $X$ and $s_3$ is called a \textit{witness} of $s_1,s_2$ (for formula $\varphi$).

Since checking whether a tuple $s$ belongs to the query result $\phi(\mA)$ of a first-order formula can be done in logarithmic space, deciding whether $\mA\models_X\varphi$ is in $\logspace$. The following tractability result can be obtained.

\begin{theorem}
The data complexity of the model checking problem for formulas of the form $\varphi_1\vee \varphi_2$  with $\varphi_1,\varphi_2\in \bcindepfo$ is in $\nl$.
\end{theorem}

\input{proofNLfragment.tex}

We will next show that a slight relaxation on the form of the input formula immediately yields intractability 
of model-checking.
\begin{theorem}
The exists a formula $\varphi_1\vee \varphi_2$ such that $\varphi_1\in\bcindepfo$ and $\varphi_2$ is the conjunction of \textit{two} independence atoms whose model-checking problem is $\np$-complete.
\end{theorem}

\input{hardnessIndep.tex}

Hardness result of Proposition~\ref{3 disjunction relativized independance} concerns conditional independence atoms. We prove an analog for the case of pure independence below.
%The following theorem further shows that even unary pure independence atoms suffice to make the model-cheking problem NP-complete.

\begin{theorem}\label{pure3-disjunction}
	The model checking problem 	is $\np$-complete for formula $\phi$ of the form
	$$\phi \equiv \left(x \perp y\right) \vee \left(x \perp y\right) \vee \left(x \perp y\right) \vee x \neq y$$
%	is $\np$-complete.
\end{theorem}


\begin{proof}
	Let $G=(V_G,E_G)$ be a graph, $\mA = V_G $ be a first order structure of the empty signature, and $X$ be the team $X = \{\,(v,v) \,|\, v \in V_G\,\}\cup \{\,(v_1,v_2), (v_2,v_1) \,|\, (v_1,v_2) \in E_G\,\}$ (we  write an assignment $s$ with $s(x)=v_1$ and  $s(y)=v_2$ succinctly as $(v_1,v_2)$).
		 We are going to show that $G$ has a $3$-clique cover if and only if $\mA \models_X \phi$.
	 
%	 $$\begin{array}{|c|c|}
%		\hline
%		\col x & \col y \\
%		\hline
%		v_1 & v_1 \\
%		v_2 & v_2 \\
%		\vdots & \vdots \\
%		v_{|V_G|} & v_{|V_G|} \\
%		\hline
%		v_1 & v_2 \\
%		v_2 & v_1 \\
%		v_2 & v_4 \\
%		v_4 & v_2 \\
%		\vdots & \vdots \\
%		\hline
%	\end{array}$$
	
	 \begin{itemize}
	 \item[$\Rightarrow$] Suppose that $G$ has a $3$-clique cover, i.e., there exists $C_1,C_2,C_3$ three cliques such that $V_G = V_{C_1} \cup V_{C_2} \cup V_{C_3}$. We have to prove  $\mA \models_X \phi$. For $i \in \{\,1,2,3\,\}$, let $$X_i = \{\,(v,v)\,|\, v \in C_i\,\} \cup  \{\,(v_1,v_2), (v_2,v_1)\, |\, v_1,v_2 \in C_i\,\}$$ and $X_4 = X\setminus (X_1\cup X_2 \cup X_3)$.
	 
	 Because it is a vertex cover, every assignment of the form $(v,v)$ is contained in $X_1\cup X_2\cup X_3$ and not in $X_4$, i.e. $\mA \models_{X_4} x \neq y$.
	 
	 Let $i \in \{\,1,2,3\,\}$ and $s,s' \in X_i$ be two assignments. If $s(x,y)=(v,v)$ and $s'(x,y)=(v',v')$, then $v,v' \in C_i$ and there exists two assignments $s_1,s_2$  in $X_i$ such that $s_1(x,y) = (v,v')$ and $s_2(x,y)=(v',v)$ by construction. Similarly if $s(x,y) = (v,v)$ and $s'(x,y) = (v_1,v_2)$, there exists in $X_i$ the assignments $(v,v_2)$ and $(v_1,v)$ (even if $v_1 = v$ or $v_2 = v$). Finally, if $s(x,y)=(v_1,v_2)$ and $s'(x,y)=(v_1',v_2')$, the assignments $(v_1,v_1),(v_2,v_2),(v_1',v_1'),(v_2',v_2')$ are in $X_i$ and so are $(v_1,v_2'),(v_1',v_2)$. The above implies that $\mA \models_{X_i} x \perp y$.
	 
	\item[$\Leftarrow$]  Suppose that $\mA \models_X  \left(x \perp y\right) \vee \left(x \perp y\right) \vee \left(x \perp y\right) \vee x \neq y$, then $X = X_1 \cup X_2 \cup X_3 \cup X_4$ such that $\mA \models_{X_i} x \perp y$ for $i \in \{\,1,2,3\,\}$ and $\mA \models_{X_4} x \neq y$.
	For $i \in \{\,1,2,3\,\}$ let $C_i$ be the graph whose vertices are $\{\, v \,|\,(v,v) \in X_i\,\}$ and edges are 
	\[ \{\, (v_1,v_2)\,|\,(v_1,v_2) \in X_i \text{ and }(v_2,v_1) \in X_i\,\} .\]
	Note that  some $C_i$ can be empty but they form a vertex cover of $G$ as no assignment $(v,v)$ is in $X_4$. If $v,v'\in C_i$ then $(v,v)$ and $(v',v')$ are in $X_i$. By independence, $(v,v')$ and $(v',v)$ are also in $X_i$. Therefore the edge $(v,v')$ is in $C_i$: $C_i$ is a clique. Therefore, $G$ is covered by the three disjoint cliques $C_1' = C_1$, $C_2' = C_2 / C_1$ and $C_3' = C_3 / (C_1 \cup C_2)$. 
	
	%	If we are in strict semantic, the $X_i$ are disjoints, so are the cliques. If we are in lax semantic, $G$ is covered by the disjoint cliques $C_1' = C_1$, $C_2' = C_2 / C_1$ and $C_3' = C_3 / (C_1 \cup C_2)$. In both cases, $G$ has a $3$-clique cover.
	 \end{itemize}
		 
\end{proof}


%The formalisms above can be generalized in two ways: either by allowing existential quantification (with or without a limited form of disjunction), or by allowing more than one disjunction. We will prove that all choices lead to intractability of the model-checking problem.



\subsection{The case of quantified formulas}

In this section we show that  existential quantification even without disjunction makes the model checking problem hard  for both dependence and independence logic. %Let $\AndExistDep$ and  $\AndExistInd$  be the fragments of $\df$ and $\Ind$ using existential quantification and conjunction only. 

\begin{theorem}\label{Exists+wedge} There is a formula $\varphi$ of dependence logic of empty non-logical vocabulary build with $\exists $ and $\wedge$ whose model-checking problem is  $\np$-complete.
 
\end{theorem}

\begin{proof} Define  the formula $\phi$ as follows:
	$$\phi \equiv \exists x\dep\left(x,r_1,r_2,e,m\right)\wedge \dep \left(v_1,v_2,x\right).$$ 
	We will reduce the problem of determining whether a graph $G$ with  $n^2$ vertices is $n$-colorable to the model-checking problem of $\phi$. This graph problem is easily seen to be $\np$-complete.
	


	Let $G$ be a graph with $n^2$ vertices $V_G=\{\alpha_0,\hdots,\alpha_{n^2-1}\}$, $\mA=\{0,\ldots, n-1\}$ a first order structure of the empty signature and $X = \{s_i^j \ |\  i \in \{0,\ldots ,n^2-1\},\  0 \le j\le i \}$ be a team such that :

	\begin{itemize}
		\item $s_i^j(v_1) = \lfloor i/n\rfloor$ and $s_i^j(v_2) = i \mod n$. %for every $j \in \{0,\ldots, i \}$. 
		In other words, $s_i^j(v_1,v_2)$ is the decomposition of $i$ in base $n$.
		\item $s_i^j(r_1) = \lfloor j/n\rfloor $ and $s_i^j(r_2) = j \mod n$. %, for every  $j \in \{0,\ldots, i \}$. 
		In other words, $s_i^j(r_1,r_2)$ is the decomposition of $j$  in base $n$.
		
		\item $s_i^j(m) = 0$ if $i \neq j$ and $s_i^i(m) = 1$.%, for any $j \in [1,i]$.
		\item $s_{i'}^{i}(e) = 1$, if $i'=i$, or if there is an edge between $\alpha_i$ and $\alpha_{i'}$ with $i' > i$. Otherwise $s_{i'}^{i}(e) = 0$.
	\end{itemize}
	
	For example, for $n= 2$ and $E_G = \{(0,1);(1,2);(0,2);(2,3)\}$, we  obtain the following team on the universe $A= \{0,1\}$:
	
	$$\begin{array}{|c|c|c|c|c|c|c|}
	\hline
	x & v_1 & v_2 & r_1 & r_2 & m & e \\
	\hline
	& 0 & 0 & 0 & 0 & 1 & 1 \\
	\hline
	& 0 & 1 & 0 & 0 & 0 & 1 \\
	& 0 & 1 & 0 & 1 & 1 & 1 \\
	\hline
	& 1 & 0 & 0 & 0 & 0 & 1 \\
	& 1 & 0 & 0 & 1 & 0 & 1 \\
	& 1 & 0 & 1 & 0 & 1 & 1 \\
	\hline
	& 1 & 1 & 0 & 0 & 0 & 0 \\
	& 1 & 1 & 0 & 1 & 0 & 0 \\
	& 1 & 1 & 1 & 0 & 0 & 1 \\
	& 1 & 1 & 1 & 1 & 1 & 1 \\
	\hline
	\end{array}$$
	$$G \text{ is } n\text{-colourable iff } \mA\models_X \phi$$
	We are going to demonstrate that $\mA \models_X \phi$ if and only if $G$ is $n$-colourable.
	
	First the left to right implication. Since $\mA\models_X \phi$ there exists  a mapping  $F\colon X\rightarrow \mathcal{P}(A)\setminus \{\emptyset\}$ such that $\mA\models_{X(F/x)} \dep\left(x,r_1,r_2,e,m\right)\wedge \dep \left(v_1,v_2,x\right)$.  By downwards closure, we may assume without loss of generality that $F(s)$ is a singleton for all $s\in X$.
	% Let $X'$ be an extension of $X$ such that $\mA\models_{X'} \dep\left(x,r_1,r_2,e,m\right)\wedge \dep \left(v_1,v_2,x\right)$. 
	%Let $F: X \rightarrow A$ be defined by $F(s_i^j) = s_i^j(x)$.
Since  $\dep(v_1,v_2,x)$ holds,  $F$ induces a mapping  $F'\colon V_G \rightarrow A$, by 
$F'(\alpha_i) = s_i^0(x)$. If there is an edge between $\alpha_i$ and $\alpha_{i'}$, $i' > i$, then $s_{i'}^{i}(e) = 1 = s_i^{i}(e)$. Furthermore, $s_{i'}^{i}(r_1,r_2) = s_{i}^{i}(r_1,r_2)  = i$ but $ s_{i'}^{i}(m) = 0$ and $s_{i}^{i}(m) = 1$ Therefore, because the atom  $\dep (x,r_1,r_2,e,m)$ holds,  we must have $s_{i'}^{i}(x) \neq  s_{i'}^{i}(x)$ (and $F'(\alpha_i) \neq F'(\alpha_{i'})$) if there is an edge between $\alpha_i$ and $\alpha_{i'}$.  Thus $F'$ is a colouring of $G$ with $|A| =  n$ colours.
	
	Let us then consider the right to left implication. Let $c: V_G \rightarrow \{0,\ldots ,n-1\}$ be an $n$ colouring. We extend $X$ to variable $x$ with a new team $X'$ such that $s^j_i(x) = c(\alpha_i)$. The value of $x$ depends only on $i$, which is encoded in $(v_1,v_2)$, i.e., $\mA \models_{X'} \dep(v_1,v_2,x)$.
	
	 Let $s_i^j, s_{i'}^{j'}$ be two assignments of $X'$. Suppose that $s_i^j(r_1,r_2,e) = s_{i'}^{j'}(r_1,r_2,e)$ but $s_i^j(m) \neq s_{i'}^{j'}(m)$. In this case we must check that $s_i^j(x)$ is different from $s_{i'}^{j'}(x)$ (because $\mA \models_{X'} \dep(x,r_1,r_2,e,m)$). Now it holds that $j=j'$ because $s_i^j(r_1,r_2) = s_{i'}^{j'}(r_1,r_2)$. Furthermore, since $s_i^j(m) \neq s_{i'}^{j'}(m)$, either $i=j$ or $i'=j'$. Let us suppose $i=j$. Because $1= s^i_i(e)=  s^j_{i}(e) = s^{j'}_{i'}(e)=s^i_{i'}(e)$, there is an edge between $\alpha_i$ and $\alpha_{i'}$ in $G$. Therefore $c(i) \neq c(i')$ and $s^j_i(x) \neq s^{j'}_{i'}(x)$.
	\end{proof}

%\begin{corollary}
%The model-checking problem for  is $\np$-complete. 
%\end{corollary}
By encoding dependence atoms in terms of conditional independence atoms we get the analogous results for free for independence logic.
\begin{corollary}
There is a formula $\varphi$ of independence logic of empty non-logical vocabulary build with $\exists $ and $\wedge$ whose model-checking problem is  $\np$-complete.
 

\end{corollary}

We end this section by noting that existential quantifiers cannot be replaced by universal quantifiers in the above theorems.

\begin{proposition}\label{forall+wedge} The model-checking problem for formulas of  dependence or independence  logic using only  universal quantification and conjunction is in $\logspace$.
% Let $\varphi$  be a formula of  dependence or independence  logic using only  universal quantification and conjunction. Then the  model-checking problem of $\varphi$  is in L.
\end{proposition}
%\begin{proof}[Sketch] It is easy to show that $\varphi$ can be expressed in FO assuming  the team $X$ with domain $\tu x$ is represented by the $n$-ary relation $X(\tu x)$. 
%\end{proof}

\begin{proof} %By the assumption, $\varphi$ may only contain universal quantifiers and conjunction. 
We first transform $\varphi$ into prenex normal-form exactly as in first-order logic \cite{vaananen07}. We may hence assume that $\varphi $ has the form
\[  \forall x_1\ldots \forall x_n \bigwedge \theta_i (x_1,\ldots, x_n,y_1,\ldots,y_m),        \]
where $\theta _i$ is either a first-order, dependence, or independence atom. Let  $\mA$ be a model,  and  $X$ be a team of $A$ with domain $\{x_1,\ldots,x_n,y_1,\ldots,y_m\} $. As in   \cite{vaananen07}, the formula $\bigwedge \theta_i (x_1,\ldots,x_n,y_1,\ldots,y_m)$ can be expressed by a first-order sentence $\psi$ when the team $X$ is represented by the $n+m$-ary relation $X(\tu x,\tu y)$, that is,
$$ \mA\models _X \bigwedge \theta_i (x_1,\ldots,x_n,y_1,\ldots,y_m) \Leftrightarrow (\mA,X(\tu x,\tu y))\models \psi. $$
Since $X(\tu x,\tu y)$ is a first-order definable extension of  $X(\tu y)$ it is clear that we can construct a FO-sentence $\psi'$ such that 
$$ \mA\models _X  \forall \tu x \bigwedge \theta_i (\tu x,\tu y) \Leftrightarrow (\mA,X(\tu y))\models \psi', $$
holds for all structures $\mA$ and teams $X$ with domain $\{y_1,\ldots,y_m\}$. The claim follows from the fact that the data complexity of FO is in Logspace.
\end{proof}




  
eptcsdata.tex
\providecommand{\firstpage}{73}
\providecommand{\publicationstatus}{J. Esparza, E. Tronci (Eds.): Games, Automata,\\ 
Logics and Formal Verification 2015 (GandALF'15)\\
EPTCS 193, 2015, pp.\ \pageref*{FirstPage}--\pageref{LastPage},
doi:\href{http://dx.doi.org/10.4204/EPTCS.193.6}{10.4204/EPTCS.193.6}}

hardnessIndep.tex
\begin{proof}
Define $\varphi_1\equiv w\neq 1 \wedge x \perp_{t} y$, $\varphi_2\equiv c_1\perp_c c_2 \wedge x \perp_z y $. We will reduce  $3$-SAT to the  model-checking problem  of $\varphi_1\vee\varphi_2$. %The data complexity of the formula:
%\[\phi \equiv \left(w\neq 1 \wedge x \perp_{t} y \right) \vee \left(c_1\perp_c c_2 \wedge x \perp_z y\right)\]
%is NP-complete by a reduction to $3$-SAT.
 Let $\Phi = \bigwedge_{i=1}^n C_i$ be  a $3$-SAT instance. Each $C_i= p_{i_1} \vee p_{i_2} \vee p_{i_3}$ % is a disjunction of $3$ literals
  with  $p_{i_1}, p_{i_2}, p_{i_3} \in \{\, v_1,\hdots, v_m,\neg v_1,\hdots, \neg v_m\,\}$. To this instance we associate a universe $\mA$ and a team $X$ on the variables $w,c,c_1,c_2,z,x,y,t$. The structure $\mA$ is composed of  $m$ new elements $a_1,\hdots,a_m$ and of $\{\, v_1,\hdots, v_m,\neg v_1,\hdots, \neg v_m\,\}\cup\{\,0,1\,\}$. For each clause $C_i$ we add  in $X$ the $6$ assignments displayed on the left below,  and for each variable $v_i$,  we add to $X$ the $2$ assignments on the right:
\[
\begin{array}{lcr}\begin{array}{|c|c|c|c|c|c|c|c|}
\hline
w&c&c_1&c_2&z&x&y&t\\
\hline \hline
0&i&1&1&i_1&p_{i_1}&p_{i_1}&a_{6i+1}\\
0&i&1&1&i_2&p_{i_2}&p_{i_2}&a_{6i+2}\\
0&i&1&1&i_3&p_{i_3}&p_{i_3}&a_{6i+3}\\
\hline
1&i&0&0&0&0&0&a_{6i+4}\\
1&i&1&0&0&0&0&a_{6i+4}\\
1&i&0&1&0&0&0&a_{6i+4}\\
\hline
\end{array}& &
\begin{array}{|c|c|c|c|c|c|c|c|}
\hline
w&c&c_1&c_2&z&x&y&t\\
\hline \hline
0&0&0&0&i&v_i&v_i&a_{6(n+1)+i}\\
0&0&0&0&i&\neg v_i&\neg v_i&a_{6(n+1)+i}\\
\hline
\end{array}
\end{array}\]
We will next show that $\Phi$ is satisfiable if and only if $\mA \models_X \phi$.

\begin{itemize}
	\item[$\Rightarrow$] Suppose there is an assignment  $I:\{\,v_1,\hdots,v_m\,\} \rightarrow \{0,1\}$ that evaluates  $\Phi$ to true, i.e., at least one literal in each clause is evaluated to $1$. We have to split $X$ into two sub-teams $X = Y \cup Z$ such that $\mA \models_Y \left(w\neq 1 \wedge x \perp_{t} y \right)$ and $\mA \models_Z \left(c_1\perp_c c_2 \wedge x \perp_z y\right)$. We must put every assignment $s \in X$ such that $s(w) = 1$ in $Z$. There are exactly three such assignments per clause. We put in $Z$ every assignment $s$ such that $s(x) = v_i$ if $I(v_i) = 1$, and $s(x) = \neg v_i$ if $I(v_i) = 0$. The other assignments are put into $Y$.
	
	For each clause $C_i$, one literal $p_{i_1},p_{i_2},p_{i_3}$ is assigned to $1$ by $I$. Then there is at least one assignment $s(c,c_1,c_2) = (i,1,1)$ in $Z$. In $Z$, the  assignments mapping $c$ to $i$ map $(c,c_1,c_2)$ to $(i,1,1), (i,1,0),(i,0,1)$ or $(i,0,0)$. Thus $\mA \models_Z c_1\perp_c c_2$. 
	
	If $s_1,s_2 \in Z$  are such that $s_1(z)=s_2(z) = i$, then $s_1(x)$ (analogously $s_2(x)$) is $v_{i}$ if $I(v_i) = 1$, $\neg v_i$ otherwise.  Therefore, $s_1(x) = s_2(x) = s_1(y) = s_2(y)$, and hence $\mA \models_Z x \perp_z y$  holds.
	
	As for $Y$, it is immediate that $\mA \models_Y w\neq 1$. The only pair of assignments $s_1,s_2$ in $X$ such that $s_1(t)=s_2(t)$ are $(0,0,0,0,i,v_i,v_i,a_k)$ and $(0,0,0,0,i,\neg v_i,\neg v_i,a_k)$. Only one of them is in $Y$ ($s_1$ if $I(v_i) = 1$, $s_2$ otherwise). Thus $\mA \models_Y x \perp_t y$.
	
	\item[$\Leftarrow$] Suppose then that $X = Y \cup Z$ such that $\mA \models_Y \left(w\neq 1 \wedge x \perp_{t} y \right)$ and $\mA \models_Z \left(c_1\perp_c c_2 \wedge x \perp_z y\right)$. Define an assignment  $I$ of the variables of $\Phi$ by: $I(v_i) = 1$ if $s_i^t:=(0,0,0,0,i,v_i,v_i,a_k)$ is in $Z$, $I(v_i) = 0$ if $s_i^f:=(0,0,0,0,i,\neg v_i,\neg v_i,a_k)$ is in $Z$. Since $\mA \models_Z x \perp_z y$, $s_i^f(z) = s_i^t(z)$ and because there is no $s' \in X$ such that $s'(x) = s_i^f(x), s'(y) = s_i^t(y)$ and $s'(z) = s_i^f(z)$, for each $i$ at most one of $s_i^f$, $s_i^t$ can be in $Z$. Similarly, because $\mA \models_Y x \perp_t y$, only one of them can be in $Y$. Thus $I$ is indeed a function.

Since $\mA \models_Z x\perp_z y$ and there is no assignment in $X$ such that $(x,y)\mapsto(v_i,\neg v_i)$, every pair $s_1,s_2 \in Z$ such that $s_1(z) = s_2(z) =i$ must have the same value of $x$ and $y$. Every assignment representing a clause in $Z$ respects the choice of $I$. Furthermore, since $\mA \models_Z c_1 \perp_c c_2$ and $(w,c,c_1,c_2) \mapsto (1,i,0,0), (1,i,1,0),(1,i,0,1)$ are in $Z$, $(1,i,1,1)$ must be in $Z$, i.e., at least one assignment per clause is in $Z$. By the above we may conclude that $I$ satisfies $\Phi$: at least one literal per clause is evaluate to $1$ by $I$.
\end{itemize}

\end{proof}
inclusion.tex
\section{Inclusion Logic}
 In this section we show that the model-checking problem of inclusion logic formulas can be reduced to the satisfiability problem of \emph{dual-Horn} propositional formulas. A propositional formula $\Phi$ in conjunctive normal form is called dual-Horn if each of its clauses contain at most one negative literal.  
  
For a team $X$, $\tu x= \{x_{i_1},...,x_{i_n}\}\subseteq \dom(X)$, and $s\in X$, we denote by $\restrict{s}{\tu x}$ the restriction of $s$ to the  variables $x_{i_1},...,x_{i_n}$. In this section, $\sg$ denotes a relational signature.

  \begin{proposition}\label{FO inclusion lax}
  There exists an algorithm which, given 
   $\varphi\in\FOinclusion$,  a structure $\mA$ over $\sigma$, and  a team $X$ such that $\var{\varphi}\subseteq \dom(X)$, outputs a propositional formula $\Psi$ in dual-Horn form such that: $\mA \models_X \varphi \iff  \Psi$ is satisfiable.
   %   \[ \mA \models_X \varphi \mbox{ iff } \Psi \mbox{ is satisfiable. } \] 
   Furthermore, when $\varphi$ is fixed, the algorithm runs in logarithmic space in the size of $\mA$ and $X$.
  \end{proposition}
  
  \begin{proof}
  Let $\varphi, \mA, X$ be as above and $r_X=|\dom(X)|$. For any team $X$, we  will consider the set $\mX$ of propositional variables $X[s]$ for $s\in A^{r_X}$.
  % and the valuation $I:\mX\longrightarrow \{0,1\}$ defined by:
%\[ I(X[s])=1 \iff s\in X. \]
Starting from $\varphi$, $\mA$, and $X$ we decompose step by step formula $\varphi$ into subformulas (until reaching its atomic subformulas) and different teams $Y$, $Z$, ... and control the relationships between the different teams by propositional dual-Horn formulas built over the propositional variables issued from $X,Y,Z,...$..
Let $\calS=\{(\varphi,X,r_X)\}$ and $\calC=\{X[s] : s\in X\} \cup \{\neg X[s] : s\not\in X\}$. The propositional formula $\Psi$ is now constructed inductively as follows.
  
  As long as $\calS\neq \emptyset$, we apply the following rule:  Pick $(\varphi,X,r)$ in $\calS$ and apply the following rules.
  
  \begin{itemize}
  	\item If $\varphi$ is  $R(\tu x)$ with $R\in \sg$ then: $\calS:=\calS\backslash \{(\varphi,X,r)\}$  and $\calC:=\calC \cup \{X[s]\rightarrow R(\restrict{s}{\tu x}): \mbox{ for all } s\in A^r \}$.
  	%  \[\calS:=\calS\backslash \{(\varphi,X,r)\} \mbox{ and } \calC:=\calC \cup \{X[s]\rightarrow R(\restrict{s}{\tu x}): \mbox{ for all } s\in A^r \}
%  \]
%  	
%  		\begin{eqnarray*}
%  	&  	\calS:=\calS\backslash \{(\varphi,X,r)\} \mbox{ and }\\
%  	&  	\calC:=\calC \cup \{X[s]\rightarrow R(\restrict{s}{\tu x}): \mbox{ for all } s\in A^r \}
%  	  	\end{eqnarray*}
%  	
%  	\[ \calS:=\calS\backslash \{(\varphi,X,r)\} \mbox{ and }\] 
%  	
%  	\[\calC:=\calC \cup \{X[s]\rightarrow R(\restrict{s}{\tu x}): \mbox{ for all } s\in A^r \}  \]
% \juha{$X[s]\rightarrow R(\restrict{s}{\tu x})$ should be reformulated and also the definition  of $\calC$ above.} 	
% \arnaud{I have reformulated the definition of $\calC$ but maybe $X[s]\rightarrow R(\restrict{s}{\tu x})$ is clearer than $\bigcup_{s(\tu x)\not\in R}\neg X[s]$}
Clearly, it holds that $\mA\models_XR(\tu x)$ iff $ \bigwedge_{s(\tu x)\not\in R}  \neg X[s]$ is satisfiable.
  	
  	
  	\item If $\varphi$ is  $\tu x \subseteq \tu y$ then: $\calS:= \calS\backslash \{(\varphi,X,r)\}$  and  
  	\[\textstyle
  		%\calS:= \calS\backslash \{(\varphi,X,r)\}  \mbox{ and } 
  		\calC:=\calC \cup \{X[s]\rightarrow \bigvee_{s'\in A^r, \restrict{s'}{\tu y}=\restrict{s}{\tu x}} X[s']:
  	 s\in A^r \}. \]
  	 %  	  	 		\begin{eqnarray*}
%  	  	  	&  	\calS:= \calS\backslash \{(\varphi,X,r)\}  \mbox{ and } \\
%  	  	  	&  	 \calC:=\calC \cup \{X[s]\rightarrow \bigvee_{s'\in A^r, \restrict{s'}{\tu y}=\restrict{s}{\tu x}} X[s']: %\mbox{ for all }
%  	  	  	 s\in A^r \} 
%  	  	  	  	\end{eqnarray*}
%  	
%  	\[ \calS:= \calS\backslash \{(\varphi,X,r)\}  \mbox{ and } \calC:=\calC \cup \{X[s]\rightarrow \bigvee_{s'\in A^r, \restrict{s'}{\tu y}=\restrict{s}{\tu x}} X[s']: \mbox{ for all } s\in A^r \}  \]
%  	
  	It holds that $\mA\models_X\tu x \subseteq \tu y$ iff $ \bigwedge_{s\in A^r} (X[s]\rightarrow \bigvee_{s'\in A^r, \restrict{s'}{\tu y}=\restrict{s}{\tu x}} X[s'])$ is satisfiable.
  	  	
  	
  	\item If $\varphi$ is  $\exists x \psi$, then: $\calS := ( \calS \backslash \{(\varphi,X,r)\} ) \cup \{(\psi,Y, r+1)\}$and 
  	\[
  		\textstyle
%  	 	\calS := ( \calS \backslash \{(\varphi,X,r)\} ) \cup \{(\psi,Y, r+1)\}  \mbox{ and } 
  	    	\calC:=\calC \cup \{X[s]\rightarrow \bigvee_{
  	  	  	s'=(s,a),\  a\in A} Y[s']: s\in A^r \}, 
  	  	\]
  	%  	  		\begin{eqnarray*}
%  	  	  	&  	\calS := ( \calS \backslash \{(\varphi,X,r)\} ) \cup \{(\psi,Y, r+1)\}  \mbox{ and } \\
%  	  	  	&  	\calC:=\calC \cup \{X[s]\rightarrow \bigvee_{
%  	  	  	  	%s'\in A^{r+1}, \restrict{s'}{\tu x}=\restrict{s}{\tu x}
%  	  	  	  	s'=(s,a),\  a\in A} Y[s']: s\in A^r \} 
%  	  	  	  	\end{eqnarray*}
  	  	%  	\[ \calS := ( \calS \backslash \{(\varphi,X,r)\} ) \cup \{(\psi,Y, r+1)\} \]
%  	
%  	
%  	\[ \calC:=\calC \cup \{X[s]\rightarrow \bigvee_{
%  	%s'\in A^{r+1}, \restrict{s'}{\tu x}=\restrict{s}{\tu x}
%  	s'=(s,a),\  a\in A} Y[s']: \mbox{ for all } s\in A^r \}   \]
%  	
\noindent where the $Y[s]$, $s\in A^{r+1}$ are new  propositional variables (not used in $\calC$).
If $\mA\models_X\exists x \psi$ then, there exists a function $F\colon X\rightarrow \mathcal{P}(A)\setminus \{\emptyset\}$, such that $\mA\models_{X(F/x)} \psi$. In other words,  $\mA\models_Y\psi$ for some team $Y$ defined by the solutions  of the constraint $\bigwedge_{s\in A^r} X[s]\rightarrow \bigvee_{s'=(s,a),\  a\in A} Y[s']$ (which define a suitable function $F$). Conversely, if $\mA\models_Y\psi$ for a team $Y$ as above defined from $X$, then clearly $\mA\models_X\exists x \psi$.

  	
  	\item If $\varphi$ is   $\forall x \psi$, then: $\calS := ( \calS \backslash \{(\varphi,X,r)\} ) \cup \{(\psi,Y, r+1)\} $ and 
  	  		\[
 \begin{array}{l}
%  \calS := ( \calS \backslash \{(\varphi,X,r)\} ) \cup \{(\psi,Y, r+1)\}   \mbox{ and } \\
  \calC :=  \calC \cup  \{X[s]\rightarrow Y[s']:  s\in A^r, s'\in A^{r+1} \mbox{ s.t. } \restrict{s'}{\tu x}=\restrict{s}{\tu x} \},  
 \end{array}
  	  	\]
  	  	%  	  	\[ \calS := ( \calS \backslash \{(\varphi,X,r)\} ) \cup \{(\psi,Y, r+1)\} \]
%  	  	
%  	
%  	 
%  	  	\[ \calC:=\calC \cup \{X[s]\rightarrow Y[s']: \mbox{ for all } s\in A^r, s'\in A^{r+1} \mbox{ s.t. } \restrict{s'}{\tu x}=\restrict{s}{\tu x} \}   \]
  	  	
  	  	 \noindent where the $Y[s]$, $s\in A^{r+1}$ are new  propositional variables (not used in $\calC$). The conclusion is similar as for the preceding case.
  	  	 
  	\item  If $\varphi$ is   $\psi_1 \wedge \psi_2$ then: $\calS := ( \calS \backslash \{(\varphi,X,r)\} ) \cup \{(\psi_1,X, r), (\psi_2,X, r)\}$
  	and $\calC$ is unchanged. By definition, $\mA\models_X\varphi$ iff $\mA\models_X\psi_1 \wedge \psi_2$.
  	 \item 	If $\varphi$ is   $\psi_1 \vee \psi_2$ then: $\calS := ( \calS \backslash \{(\varphi,X,r)\} ) \cup \{(\psi_1,Y, r), (\psi_2,Z, r)\} $ and
  	 %let $\mY=\{Y[s]: s\in A^{r}\}$, $\mZ=\{Z[s]: s\in A^{r}\}$ and:
  	 	$$\textstyle
  	 % \begin{array}{l}
  	   %\calS := ( \calS \backslash \{(\varphi,X,r)\} ) \cup \{(\psi_1,Y, r), (\psi_2,Z, r)\}   \mbox{ and } \\
  	   \calC :=  \calC \cup 
 \{X[s]\rightarrow Y[s]\vee Z[s]: s\in A^r \}\cup 
 \{Y[s]\rightarrow X[s],  Z[s]\rightarrow X[s]: s\in A^r \} 
  	  %\end{array}
  	   	  	$$
  	   	  	%  	 \[ \calS := ( \calS \backslash \{(\varphi,X,r)\} ) \cup \{(\psi_1,Y, r), (\psi_2,Z, r)\}\]
%  
%  and 
%  
%\[   \calC:=\calC \cup \{X[s]\rightarrow Y[s]\vee Z[s], Y[s]\rightarrow X[s],  Z[s]\rightarrow X[s]: \mbox{ for all } s\in A^r \} 
% \]  
   \noindent where again the $Y[s]$ and $Z[s]$, $s\in A^{r}$ are  new propositional variables  (not used in $\calC$). Here again, $\mA\models_X\varphi$ if and only if $\mA\models_Y\psi_1$ and $\mA\models_Z\psi_2$ for some suitable $Y$ and $Z$ such that $Y\cup Z=X$ which is exactly what is stated by the Boolean constraints.
  \end{itemize}
  
  Observe that each new clause added to $\calC$ during the process is of dual-Horn form, i.e., contains at most one negative literal. Observe also, that applied to some $(\varphi,X,r)$, the algorithm above only adds triples  $\calS$ whose first component is a proper subformula of $\varphi$ and eliminates  $(\varphi,X,r)$. When the formula $\varphi$ is atomic, no new triple is added afterwards.  Hence the algorithm will eventually terminate with $\calS=\emptyset$. 
 Setting $\Psi:= \bigwedge_{C\in\calC} C$, it can easily be proved by induction that: $\mA \models_X \varphi$  iff  $\Psi$ is satisfiable.  
 
  
   %\[ \mA \models_X \varphi \mbox{ iff } \Psi \mbox{ is satisfiable. } \]  


Observe also that each clause in $\calC$ can be constructed from $X$ and $\mA$ by simply running through their elements (using their index) hence  in logarithmic space. 
  \end{proof}
  
 \begin{remark} 
 %Remark that t
 The construction of Proposition~\ref{FO inclusion lax} can  be done in principle for any kind of atom: dependence, independence, exclusion, constancy etc. 
 %But the resulting formula seems to be obviously in Dual-Horn form only in the case of inclusion. 
  To illustrate this remark, one could translate in the above proof a dependence atom of the form $\dep(\tu x,y)$ by (using the notations of the proof):
 
\[\bigwedge_{ \substack{s,s'\in A^r\\ s(\tu x)=s'(\tu x) \wedge s(y)\neq s'(y)}} (\neg X[s]\vee \neg X[s']).\]
 
 The additional clauses are of length two. A similar treatment can be done for independence atoms $\indep{\tu x}{\tu y}{\tu z}$.  In the two cases however, the resulting formula is not in Dual-Horn form anymore and there is no way to do so (unless $\Ptime=\np$).
 \end{remark}
  
  
  Since deciding the satisfiability of a propositional formula in dual-Horn form can be done in polynomial time we obtain the following already known corollary.
  
\begin{corollary}
  The data complexity of $\FOinclusion$  is in $\Ptime$.
  \end{corollary}
  
  %The $\FOinclusion$ logic  is in fact known to be $\Ptime$-complete since it can express alternating graph reachability.
  

introduction.tex

\section{Introduction}

In this article we study the data complexity of model-checking of dependence, independence, and inclusion logic formulas. Independence  and inclusion logic  \cite{gradel10,galliani12} are variants of  dependence logic \cite{vaananen07}  that  extends first-order logic by dependence atoms of the form 
%\begin{equation}\label{}
$\dep(x_1,\ldots,x_n)$
%\end{equation} 
expressing that the value of $x_n$ is functionally determined by the values of the variables $x_1,\ldots, x_{n-1}$. 
%The semantics of dependence logic is defined using sets of assignments rather than a single assignment as in first-order logic.  
In independence and inclusion logic dependence atoms are replaced by independence and inclusion atoms 
$\tu{y}\ \bot_{\tu{x}} \ \tu{z}$ and  $\tu{x}\subseteq \tu{y},$
respectively. The meaning of the independence atom is that, with respect to any fixed value of  $ \tu x$, the variables $\tu y$  are independent of the variables $\tu z$, whereas the  inclusion atom expresses that all the values of $\tu{x}$ appear also as values for $\tu{y}$. 

  
Dependence logic is a new framework for formalizing and studying  various notions of dependence and independence  pervasive in many areas of science.  The novelty of dependence logic is in its \emph{team semantics} in which formulas are interpreted using sets of assignments (with a common finite domain $\{x_1,\ldots ,x_n\}$ of variables) instead of single assignments as in first-order logic.  
 Reflecting this, dependence logic  has higher expressive power than classical logics used for these purposes previously.  Dependence, inclusion, and independence  atoms are intimately connected to the  corresponding functional, inclusion, and multivalued  dependencies studied in  database theory, see, e.g., \cite{DBLP:conf/foiks/HannulaK14}.  Interestingly, independence atoms can also be viewed as a qualitative analogue of the notion of conditional independence in statistics, see \cite{DBLP:journals/networks/GeigerVP90}. Furthermore, a variant of dependence logic is in the heart of  {\em Inquisitive Semantics} which is a novel approach in linguistics that analyzes information exchange through communication, see \cite{DBLP:journals/jphil/CiardelliR11}.
 
 Dependence logic and its variants can be  used to %logically 
 formalize and study dependence and independence notions in various areas. For example, in the foundations of quantum mechanics, there  are a range of notions of independence playing a central role in celebrated No-Go results such as Bell's theorem. Abramsky and V\"a\"an\"anen have recently showed that, under a  relational view on these results,  some of these No-Go results can be logically formalized and  syntactically derived using the axioms of independence and dependence atoms. For another application of team semantics in quantum information theory, see \cite{2014arXiv1409.5537H}. Similarly, in the foundations of social choice theory, there are results such as Arrow's Theorem which  can also be formalized in the team semantics setting.
 %%%%

For the applications it is important to understand the complexity theoretic aspects  of dependence logic and its variants. %Full dependence logic is  equivalent in expressive power with existential second-order logic ($\ESO$) \cite{vaananen07}. 
 During the past few years,  these aspects have been addressed in several studies. We will next briefly discuss some previous work. 
%\begin{itemize}
 The data complexity of inclusion logic  is sensitive to the choice between the two main variants of team semantics: under the so-called  lax semantics it is equivalent to positive greatest fixed point logic ($\PGFP$) and captures $\Ptime$ over finite (ordered) structures \cite{gallhella13}. On the other hand, under the strict semantics, inclusion logic is equivalent to $\ESO$ and hence captures $\np$ \cite{galhankon13}.  The  question whether there is a natural  fragment of dependence logic capturing $\Ptime$  was recently considered in \cite{DBLP:journals/corr/abs-1210-3321} %For $\ESO$  it is known that a so-called Horn fragment $\ESOHORN$ of  $\ESO$ captures 
% $\Ptime$ over  successor structures \cite{DBLP:journals/tcs/Gradel92}. 
and 
 a fragment  $\SDHORN$  satisfying 
 $\SDHORN = \ESOHORN=\Ptime$ over finite successor structures was identified.
 
 In \cite{durand11} the fragment of dependence logic allowing only sentences in which dependence atoms of arity at most $k$ may appear (atoms  $\dep(x_1,\ldots, x_n)$ satisfying $n\le k+1$) was shown to correspond to the $k$-ary fragment  $\ESOfarity{k}$ of ESO in which second-order quantification is restricted to at most $k$-ary functions and relations.  Also,  the fragment $\dforall{k}$ in which at most $k$ variables are allowed to  be universally quantified was related 
 %$$\dforall{k} \le \ESOfvar{k}\le  \dforall{2k},$$
to  a fragment   $\ESOfvar{k}$ of   ESO  consisting of  Skolem normal form sentences with  at most  $k$ universal first-order quantifiers.  % $\ESOfvar{k} =\NTIME_{\RAM}(n^k)$  \cite{grandjean04}.
 Similar results have been obtained  for independence and inclusion logic (for the strict semantics) in \cite{galhankon13,DBLP:journals/corr/HannulaK14}.

 The combined complexity of the model-checking problem of dependence logic, and many of its variants, was recently shown to be NEXPTIME-complete \cite{gradel12}. %Furthermore, for any variant of dependence logic whose atoms are PTIME-computable, the corresponding model checking problem is in NEXPTIME   
 On the other hand, the satisfiability problem for the two variable fragment of dependence logic was shown to be NEXPTIME-complete in \cite{KontinenKLV11}. Recently, this result has been generalized to cover many of the variants of dependence logic \cite{DBLP:journals/corr/KontinenKV14}.


The starting point for the present work are the following results of \cite{kontinenj13} showing that the non-classical interpretation of disjunction in team semantics makes the model-checking of certain quantifier-fee
formulas very complicated.  Define $\phi_1$ and $\phi_2$ as follows:
\begin{enumerate}
\item $\phi_1$ is the formula $\dep(x,y)\vee\dep(u,v)$, and
\item\label{phi2} $\phi_2$ is  the formula $ \dep(x,y)\vee\dep(u,v)\vee \dep(u,v)$.
\end{enumerate}
Surprisingly, the data complexity of the model-checking problem of $\phi_1$ and $\phi_2$   is already  NL-complete and NP-complete, respectively. In  \cite{kontinenj13} it was also shown that  model-checking for $\varphi \vee \psi$ where $\varphi$ and $\psi$ are $2$-\emph{coherent} quantifier-free formulas of $\df$ is always in $\nl$. A formula $\varphi$ is  called $k$-coherent if, for all $\mA$ and $X$,  $\mA\models_X \phi$, if and only if,   
$\mA\models_Y \phi$ for all $Y\subseteq X$ such that $|Y|=k$. Note that the left-to-right implication is always true due to the downwards closure property of dependence logic formulas. The  downwards closure property also implies that, for dependence logic formulas,  the strict and the lax semantics are equivalent. For independence and inclusion logic formulas this is not the case. 

In this article our goal is to give as  complete picture as possible  of the tractability frontier of data complexity of model-checking of formulas of dependence, independence, and inclusion logic under the lax team semantics.  In order to state our results, we define  a new syntactic measure called the disjunction-width $\Disjunctiondepth{\varphi}$  of a formula $\varphi$. Our results show that,  for quantifier-free formulas $\varphi$ of dependence logic, the data complexity of model-checking is in NL if $\Disjunctiondepth{\varphi}\le 2$. Surprisingly, for independence logic the case of quantifier-free formulas turns out to be  more fine grained. We give a complete characterization also in this case and, in particular,  exhibit  a quantifier-free formula  with $\Disjunctiondepth{\varphi}\le 2$ whose data-complexity is NP-complete and a seemingly maximal fragment in $\nl$.
% This result is in a sense a explicit syntactically defined generalisation  of the result of  \cite{kontinenj13}  on $2$-coherent quantifier-free $\df$-formulas mentioned above. 
%We also show that for simple formulas $\phi$ with $\Disjunctiondepth{\varphi}=3$  the problem becomes NP-complete. Note that  since  $\dep(x,y)$ is logically equivalent to $y \bot_x y$,  formula $\phi_2$ in \eqref{phi2} gives rise to an independence logic formula with these properties. 
%The task of  finding a formula with NP-complete model-checking problem  and $\Disjunctiondepth{\varphi}=3$ that does not use \emph{conditional} independence atoms but only so-called \emph{pure} atoms  $y \bot x$ turns out to be more laborious (see Theorem \ref{pure3-disjunction}).
For quantified formulas,  the complexity 
%of model-checking 
is shown to be   NP-complete already with simple formulas constructed in terms of existential quantification and conjunction   in the empty non-logical vocabulary. 

For inclusion logic, we  show that model-checking can be reduced to the satisfiability problem of dual-Horn propositional formulas. While interesting in its own right, this also provides  an alternative proof of the recent result of \cite{gallhella13} showing that the  data complexity of  inclusion logic is in PTIME, and is also analogous  to the classical result of Gr\"adel on certain Horn fragments of second-order logic \cite{DBLP:journals/tcs/Gradel92}. 
%In the last section we show that, under the so-called strict semantics, the tractability frontier of model-checking of  (both quantifier-free and quantified) inclusion logic formulas is analogous to the one shown to hold for dependence and independence logic.

%This article is organized as follows...

notes.tex
\documentclass[submission,copyright,creativecommons]{eptcs}
%\documentclass[runningheads]{llncs}

\providecommand{\event}{Gandalf 2015} % Name of the event you are submitting to
\usepackage{breakurl}             % Not needed if you use pdflatex only.


% \fontencoding{T1}
%  \fontfamily{garamond}
%  \fontseries{m}
%  \fontshape{it}
 % \fontsize{12}{15}
%  \selectfont

%\usepackage[T1]{fontenc}
%\usepackage{mathptmx}

 

\usepackage{color}
\usepackage{pstricks,pst-node,pst-tree,pstricks-add}
\usepackage{multido}
%\usepackage{authblk}

%\usepackage{fullpage}
\usepackage{enumerate}
\usepackage[english]{babel}
\usepackage{amsthm}
\usepackage{amssymb}
\usepackage{amsmath}
\usepackage{amsfonts}
\usepackage[footnote,marginclue]{fixme}

\theoremstyle{plain}
\newtheorem{theorem}{Theorem}
\newtheorem{lemma}[theorem]{Lemma}
\newtheorem{corollary}[theorem]{Corollary}
\newtheorem{proposition}[theorem]{Proposition}
\newtheorem{fact}[theorem]{Fact}
\newtheorem{q}{Question}
\newtheorem*{con}{Conjecture}
\newtheorem*{theoremC}{Open Question}
\newtheorem*{theoremB}{Lyndon Interpolation Theorem}
\theoremstyle{definition}
\newtheorem{rem}[theorem]{Remark}
\newtheorem{definition}[theorem]{Definition}
\newtheorem{example}[theorem]{Example}
\newtheorem{remark}{Remark}
\newtheorem{claim}{Claim}

% Structures
\newcommand{\sg}{\sigma}
\newcommand{\rel}{rel}
\newcommand{\mA}{{\mathfrak A}}
\newcommand{\Dom}{{\rm Dom}}
\newcommand{\dom}{{\rm dom}}
\DeclareMathOperator{\str}{Str}
\DeclareMathOperator{\Mod}{Mod}

%\newcommand{\restrict}[2]{{#1}_{|#2}}
\newcommand{\restrict}[2]{{#1}({#2})}

% % letters
\newcommand{\calC}{{\mathcal C}}
\newcommand{\calS}{{\mathcal S}}
\newcommand{\mX}{{\mathfrak X}}
\newcommand{\mY}{{\mathfrak Y}}
\newcommand{\mZ}{{\mathfrak Z}}


%% Logics
%\newcommand{\FO}{{\rm FO}}
%\newcommand{\FO}{\rm FO\foarg}
%\newcommand{\foarg}[1][]{(#1)}

\newcommand{\FO}[1]{{\rm FO(#1)}}
\newcommand{\conjFOqf}[1]{{\rm \{\wedge\}\!-\!FO({#1})}}
\newcommand{\AndExistForallFO}[1]{{\rm \{\wedge, \exists, \forall\}\!-\!FO({#1})}}
\newcommand{\AndExistFO}[1]{{\rm \{\wedge, \exists\}\!-\!FO({#1})}}
\newcommand{\AndExistForallDep}{{\rm \{\wedge, \exists, \forall\}\!-\!\df}}
\newcommand{\AndExistDep}{{\rm \{\wedge, \exists\}\!-\!\df}}
\newcommand{\AndExistInd}{{\rm \{\wedge, \exists\}\!-\! \Ind}}


\newcommand{\free}[1]{\textsf{free}(#1)}

\newcommand{\MSO}{{\rm MSO}}
\newcommand{\Fr}{{\rm Fr}}
\newcommand{\Var}{{\rm Var}}
\newcommand{\SO}{{\rm SO}}
\newcommand{\ESO}{{\rm ESO}}

%\newcommand{\dep}{=\!\!}
\newcommand*\dep{{=\mkern-1.2mu}} 
\newcommand{\Ind}{\mathcal{I}}
\newcommand{\df}{\rm{D}}
%\newcommand{\dfreg}{\mathcal{D}^{reg}}
\newcommand{\FOinclusion}{{\rm FO(\subseteq)}}

\newcommand{\ESOarity}[1]{{\rm ESO}({#1}\mbox{-ary})}
\newcommand{\ESOfarity}[1]{{\rm ESO}_f({#1}\mbox{-ary})}
\newcommand{\ESOfarityOcc}[1]{{\rm ESO}_f^1({#1}\mbox{-ary})}
\newcommand{\ESOfvar}[1]{{\rm ESO}_f({#1}\forall)}
\newcommand{\ESOfvarOcc}[1]{{\rm ESO}_f^1({#1}\forall)}
\newcommand{\ESOarityvar}[2]{{\rm ESO}({#1}\mbox{-ary},{#2}\forall)}
\newcommand{\ESOfarityvar}[2]{{\rm ESO}_f({#1}\mbox{-ary},{#2}\forall)}

\newcommand{\fo}{{\rm FO}}
%\newcommand{\dforall}[1]{\fo(\dep(\ldots))({#1}\forall)}
\newcommand{\dforall}[1]{{\rm D}({#1}\forall)}
\newcommand{\ddep}[1]{\fo(\dep(\ldots))({#1}\mbox{\rm-dep})}



% Complexity

\newcommand{\RAM}{{\rm RAM}}
\newcommand{\NTIME}{{\rm NTIME}}
\newcommand{\np}{{\rm NP}}
\newcommand{\Ptime}{{\rm PTIME}}
\newcommand{\ph}{{\rm PH}}
\newcommand{\nl}{{\rm NL}}
\newcommand{\logspace}{{\rm Logspace}}
\newcommand{\GFP}{{\rm GFP}}
\newcommand{\LFP}{{\rm LFP}}
\newcommand{\PGFP}{{\rm GFP}^+}


% arnaud
\newcommand{\pr}{\mathrm{Pr}}
\newcommand{\tu}[1]{\overline{#1}}
\newcommand{\calP}{\mathcal{P}}

\newcommand{\indep}[3]{{#1}\ \bot_{#2}\ {#3}}
\newcommand{\var}[1]{\mathsf{#1}}
\newcommand{\col}[1]{\mathbf{#1}}

%Nicolas
\newcommand{\mAsat}[2]{\mA \models_{#1}  #2}
\newcommand{\mAnsat}[2]{\mA \models_{#1}  \neg #2}


% % % % % % % % % % % % % % % % % % % % % % % % %
% % % % % % For commenting the text % % % % % 
\newcommand{\commentmargin}[2]{\marginpar{\tiny{\textbf{#1 : }\textit{#2}}}}
\newcommand{\commenttext}[1]{ \begin{center} {\fbox{\begin{minipage}[h]{0.9
            \linewidth}   {\sf #1} \end{minipage} }} \end{center}} 

\newcommand{\arnaud}[1]{ {\leavevmode\color{green}\commenttext{Arnaud: #1}}}
\newcommand{\juha}[1]{{\color{red}\commenttext{Juha: #1}}}
\newcommand{\jouko}[1]{{\color{blue}\commenttext{Jouko: #1}}}
\newcommand{\nicolas}[1]{{\color{orange}\commenttext{Nicolas: #1}}}

\newcommand{\arnaudmargin}[1]{\commentmargin{\color{green}Ar}{\color{orange}#1}}
\newcommand{\juhamargin}[1]{\commentmargin{\color{red}Ju}{\color{red}#1}}
\newcommand{\joukomargin}[1]{\commentmargin{\color{blue}Jo }{\color{blue}#1}}
\newcommand{\nicolasmargin}[1]{\commentmargin{\color{orange}Ni }{\color{orange}#1}}
% % % % % % % % % % % % % % % % % % % % % % % % %


\newcommand{\makeprob}[3]{
\noindent 
\begin{tabular}{l}
\textsc{#1} \\ 
\hspace{1ex}
\begin{tabular}{lp{11cm}}
{\it Input: }  & {#2} \\
{\it Output: } & {#3} 
\end{tabular}
\end{tabular}\vspace{.7ex}
}
 \newcommand{\pb}[1]{\textsc{#1}}
 
 \newcommand{\type}[1]{\textsf{typ}(#1)}
\newcommand{\Disjunctiondepth}[1]{\textsf{d}_{\vee}(#1)}
\newcommand{\Existsdepth}[1]{\textsf{d}_{\exists}(#1)}
\newcommand{\algoone}{\text{algo}_1}
\newcommand{\algotwo}{\text{algo}_2}
\newcommand{\Falgoone}[2]{\text{Fal}_1\left(#1,#2\right)}
\newcommand{\Falgotwo}[3]{\text{Fal}_2\left(#1,#2,#3\right)}

%%%%Juha added
\newcommand{\ESOHORN}{\SO\exists\textrm{-Horn}}
\newcommand{\SDHORN}{\df^*\textrm{-Horn}}
\newcommand{\indlogic}{\rm{FO} (\bot_{\rm c})}
 

 
 % % % % % % % % % % % % % % % % % % %
%\title{Tractability Frontier of Data Complexity in Team Semantics}
%\author{Arnaud Durand\thanks{Institut de Math\'ematiques de Jussieu - Paris Rive Gauche, CNRS UMR 7586 - Universit\'e Paris Diderot, France. \texttt{durand@math.univ-paris-diderot.fr}} , 
% Juha Kontinen\thanks{Department of Mathematics and Statistics, University of Helsinki, Finland. \texttt{juha.kontinen@helsinki.fi}} ,
% Nicolas de Rugy-Alterre, %\inst{1},
%\and Jouko V\"{a}\"{a}n\"{a}nen}
%\authorrunning{A. Durand, J. Kontinen, N. de Rugy-Alterre
%\and J. V\"{a}\"{a}n\"{a}nen}

%llncs
%\author[1]{Arnaud Durand}
%\author[2]{Juha Kontinen}
%\author[1]{Nicolas de Rugy-Alterre}
%\author[2,3]{Jouko V\"{a}\"{a}n\"{a}nen}
%\affil[1]{Institut de Math\'ematiques de Jussieu - Paris Rive Gauche, CNRS UMR 7586 - Universit\'e Paris Diderot, France%\texttt{durand@math.univ-paris-diderot.fr}
%}
%\affil[2]{Department of Mathematics and Statistics, University of Helsinki, Finland} %\texttt{juha.kontinen@helsinki.fi}
%\affil[3]{Institute for Logic, Language and Computation, University of Amsterdam, The Netherlands}




\title{Tractability Frontier of Data Complexity in Team Semantics}

\author{Arnaud Durand
\institute{IMJ-PRG, CNRS UMR 7586\\ Universit\'e Paris-Diderot, France}
%\email{durand@math.univ-paris-diderot.fr}
\and
Juha Kontinen 
\institute{Department of Mathematics and Statistics\\ University of Helsinki, Finland}
\and Nicolas de Rugy-Altherre
\institute{IMJ-PRG, CNRS UMR 7586\\ Universit\'e Paris-Diderot, France}
\and 
Jouko V\"{a}\"{a}n\"{a}nen
\institute{Department of Mathematics and Statistics\\ University of Helsinki, Finland}
\institute{Institute for Logic, Language and Computation\\ University of Amsterdam, The Netherlands}
}
\def\titlerunning{Tractability Frontier of Data Complexity in Team Semantics}
\def\authorrunning{A. Durand, J. Kontinen, N. de Rugy-Altherre \& J. V\"{a}\"{a}n\"{a}nen}




\begin{document}
\maketitle
%% long abstract
%\begin{abstract} We study the data complexity of model-checking for logics with team semantics. For dependence and independence logic, we formulate our results  using a syntactic measure called disjunction-depth $\Disjunctiondepth{\varphi}$. 
%We show that the data complexity of quantifier-free dependence logic formulas $\varphi$  is in NL if $\Disjunctiondepth{\varphi}\le 2$, while for  simple formulas $\phi$ with $\Disjunctiondepth{\varphi}=3$  the problem is known to be  NP-complete. Surprisingly, for independence logic the case of quantifier-free formulas turns out to be  more subtle. We identify a maximal fragment among formulas with   $\Disjunctiondepth{\varphi}\le 2$ for which data complexity is in NL, and also show that there are formulas  with $\Disjunctiondepth{\varphi}\le 2$ whose data-complexity is NP-complete. We also show that when existential quantifiers are allowed very simple formulas $\varphi$ with just one existential quantifier symbol combined with conjunction   give rise to an NP-complete model-checking problem. For inclusion logic formulas, we reduce the model-checking problem  to the  satisfiability problem of so-called \emph{Dual-Horn} propositional formulas providing an alternative proof of the recent result of \cite{gallhella13} showing that the  data complexity of  inclusion logic is in PTIME. In the last section  we turn to the so-called strict semantics and show that the tractability frontier of the data complexity of model-checking for inclusion logic  under this alternative semantics is analogous to that of dependence and independence logic.
%\end{abstract}
\begin{abstract}We study the data complexity of model-checking for logics with team semantics. For dependence and independence logic, we completely characterize the tractability/intractability frontier  of data complexity of both quantifier-free and quantified formulas. For inclusion logic formulas, we reduce the  model-checking problem to the satisfiability problem of so-called \emph{Dual-Horn} propositional formulas. Via this reduction, we give an alternative proof for the recent result showing that the data complexity of  inclusion logic is in  PTIME. 
\end{abstract}

\input{introduction.tex}
\input{preliminaries.tex}
\input{dependence_independence.tex}
\input{inclusion.tex}
%\input{strict_semantics.tex}
\section{Conclusion}
We have studied the  tractability/intractability frontier  of data complexity of both quantifier-free and quantified  dependence and independence logic formulas. Furthermore, we defined a novel translation of  inclusion logic formulas into dual-Horn propositional formulas, and used it to show that the data-complexity of inclusion logic is in PTIME.
%Although our results give a complete overall picture of the tractability/intractability frontiers studied in this article, some open  questions related to the data-complexity of quantifier-free independence logic formulas remain. 
It is an interesting open question whether the translation of Proposition 16 can be generalized to hold for some interesting extensions of $\FO\subseteq$ by further dependency atoms.

\section*{Acknowledgements}
The authors would like to thank Arne Meier for a number of corrections and useful suggestions. The second author was supported by the Academy of Finland grant 264917.
%
\bibliographystyle{eptcs}
\bibliography{biblio}








\end{document}

preliminaries.tex
\section{Preliminaries}
In this section we briefly discuss the basic definitions and results needed in this article.
 
 
 \begin{definition}
Let $\mA$ be a structure with domain $A$, and $V=\{x_1,\ldots,x_k\}$ be a finite (possibly empty) set  of
variables.
\begin{itemize}
\item A \emph{team} $X$ of $\mA$ with domain $\Dom(X) = V$  is a finite set of assignments $s\colon V\rightarrow A$.
\item For a tuple $\tu x=( x_1,\ldots,x_n)$, where  $x_i\in V$,  $X(\tu x):=\{s(\tu x) : s \in X\}$ is the $n$-ary relation of $A$, where $s(\tu x):=( s(x_1),\ldots,s(x_n))$.
\item For $W\subseteq V$, $X \upharpoonright W$ denotes  the team obtained by restricting all assignments of $X$ to  $W$.
\item  The set of free variables of a formula $\varphi$ is  defined as in first-order logic and is denoted by $\Fr(\phi)$.
\end{itemize}
\end{definition}
We are now ready to define team semantics. As now customary, we will restrict attention to formulas in negation normal form, and use the Lax semantics introduced in \cite{galliani12} that differs slightly from the semantics defined in \cite{vaananen07}.  %We will consider two variants of the semantics called the Strict and
%The original semantics given in \cite{Vaananen:2007} is a combination of these variants (with the lax disjunction and the strict existential quantifier).
%For dependence logic formulas, the two variants of the semantics are easily seen to be equivalent, but for independence and inclusion logic this is not the case.
%We will first define the lax  team semantics for first-order formulas in negation normal form. 
Below  $\mA \models_s \alpha$ refers to the satisfaction in first-order logic, and $s(m/x)$ is the assignment such that $s(m/x)(x)=m$, and   $s(m/x)(y)=s(y)$ for $y\neq x$. The power set of a set $A$ is denoted by $\mathcal{P}(A)$.

\begin{definition}
Let $\mA$ be a structure, $X$ be a team of $A$, and $\varphi$ be a first-order formula such that $\Fr(\varphi)\subseteq \Dom(X)$. %Then $\mA \models_X \phi$, if 
\begin{description}
\item[lit:] For a first-order literal $\alpha$, $\mA \models_X \alpha$ if and only if, for all $s \in X$, $\mA \models_s \alpha$.
\item[$\vee$:]  $\mA \models_X \psi \vee \theta$ if and only if,  there are $Y$ and $Z$ such that $Y \cup Z=X$,  $\mA \models_Y \psi$ and $\mA \models_Z \theta$.
\item[$\wedge$:] $\mA \models_X \psi \wedge \theta$ if and only if, $\mA \models_X \psi$ and $\mA \models_X \theta$.
\item[$\exists$:]  $\mA \models_X \exists x \psi$ if and only if, there exists a function $F : X \rightarrow \mathcal{P}(A)\setminus \{\emptyset\}$ such that $\mA \models_{X(F/x)} \psi$, where $X(F/x) =  \{s(m/x) : s \in X, m \in F(s)\}$.
\item[$\forall$:] $\mA \models_X \forall x \psi$ if and only if, $\mA \models_{X(A/x)} \psi$, where $X(A/x) = \{s(m/x) : s \in X, m \in A\}$.
\end{description}
A sentence $\phi$ is  \emph{true} in $\mA$ (abbreviated $\mA \models \phi$) if $\mA \models_{\{\emptyset\}} \phi$. Sentences $\phi$ and $\phi'$ are  \emph{equivalent}, $\phi \equiv \phi'$, if for all models $\mA$, $\mA \models \phi \Leftrightarrow \mA \models \phi'$.
\end{definition}
%In the \emph{Strict Semantics}, the semantic rule for disjunction is modified by adding the requirement $Y\cap Z = \emptyset$, and  the clause for the existential quantifier  is replaced by 
%\begin{description} 
%\item $\mA \models_X \exists x \psi$ if and only if, there exists a function $H : X \rightarrow A$ such that $\mA \models_{X(H/x)} \psi$, where $X(H/x) = \{s(H(s)/x) : s \in X\}$. \end{description}
%The meaning of first-order formulas is invariant under the choice between the strict and the lax semantics. 
First-order formulas satisfy what is known as the \emph{Flatness} property:
%\begin{theorem}[Flatness]\label{flatness}Let $\mA$ be a structure and $X$ a team of $\mA$. Then for a  first- order formula $\phi$ the following are equivalent: 
%\begin{enumerate}
 $\mA \models_X \phi$, if and only if,  $\mA \models_s \phi$  for all $s \in X$.
Next we will give the semantic clauses for the new dependency atoms:
\begin{definition}
\begin{itemize}
\item Let $\tu x$ be a tuple of variables and let $y$ be another variable. Then $\dep(\tu x, y)$ is a \emph{dependence atom}, with the semantic rule
\begin{description}
\item $\mA \models_X \dep(\tu x, y)$ if and only if for all $s, s' \in X$, if $s(\tu x)=s'(\tu x)$, then $s(y)=s'(y)$;
\end{description}
\item Let $\tu x$, $\tu y$, and $\tu z$ be tuples of variables (not necessarily of the same length). Then $\indep{\tu x}{\tu y}{\tu z}$ is a \emph{conditional independence atom}, with the semantic rule
\begin{description}
\item $\mA \models_X {\tu x}\ \bot_{\tu y}\ {\tu z}$ if and only if for all $s, s' \in X$ such that $s(\tu y)=s'(\tu y)$, there exists a $s'' \in X$ such that $s''(\tu x\tu y \tu z)=s(\tu x\tu y)s'(\tu z)$.
\end{description}
Furthermore, when $\tu z$ is empty, we write ${\tu x}\bot{\tu y}$ as a shorthand for ${\tu x}\bot_{\tu z}  {\tu y}$, and  call it a \emph{pure independence atom};
\item Let $\tu x$ and $\tu y$ be two tuples of variables of the same length. Then $\tu x \subseteq \tu y$ %and $\tu x \mid \tu y$ are 
is an \emph{inclusion atom}, with the semantic rule %and \emph{exclusion} atoms, respectively, with the semantic rules
\begin{description}
\item $\mA \models_X \tu x \subseteq \tu y$ if and only if for all $s\in X$ there exists a $s' \in X$ such that $s'(\tu y)=s(\tu x)$. 
%\item[TS-exc:] $\M \models_X \tu x \mid \tu y$ if and only if $X(\tu x) \cap X(\tu y) = \emptyset$.
\end{description}
\end{itemize}
\end{definition}
%For a  collection $\mathcal C \subseteq \{=\!\!(\ldots), \bot_{\rm c}, \subseteq, \mid\}$ of atoms, we write $\FO(\mathcal C)$ (omitting the set parenthesis of $\mathcal{C}$) for the logic obtained by adding them to the syntax of first-order logic.
The formulas of dependence logic, $\df$, are obtained by extending the syntax of $\fo$ by dependence atoms. The semantics of $\df$-formulas is obtained by extending Definition 2 by the semantic rule defined above for dependence atoms.  Independence logic, $\indlogic$, and inclusion logic, $\FOinclusion$, are defined analogously using independence and inclusion atoms, respectively.
%The fragment of independence logic containing only pure independence atoms in denoted  $\indNRlogic$.  The aforementioned atoms are particular instance of a general notion of \emph{generalised dependence atom} \cite{DBLP:journals/corr/Kuusisto13}. The semantics of a generalised dependence atom $A_Q$ is determined (essentially) by a class  $Q$ of structures and teams over which the atomic formula $A_Q(\tu x_1,\ldots, \tu x_n)$  is satisfied (see \cite{DBLP:journals/corr/Kuusisto13} for details).  

It is easy to see that the flatness property is lost immediately when $\fo$ is extended by any of the above dependency atoms. On the other hand,  it is straightforward to check that all $\df$-formulas satisfy the following  strong \emph{Downwards Closure} property:  if $\mA \models_X \phi$ and   $Y\subseteq X$, then $\mA \models_Y \phi$.
%\begin{proposition}[Downwards closure]
%\label{thm:dc}
%Let  $\phi$ be a $\df$-formula. Then for all structures  $\mA$  and teams  $X$, if $\mA \models_X \phi$ and    $Y\subseteq X$, then $\mA \models_Y \phi$.
%\end{proposition}
Another basic property shared by all of the above logics is called \emph{Locality}:
 $\mA \models_X \phi$, if and only if,    $\mA \models_{X \upharpoonright \Fr(\phi)} \phi$.
%\begin{proposition}[Locality]
%Let  $\phi$ be a formula of any of the logics  $\df$,  $\indlogic$ or $\FOinclusion$. Then, under the lax semantics, for all structures  $\mA$  and teams  $X$:
% $$\mA \models_X \phi \mbox{ iff }    \mA \models_{X \upharpoonright \Fr(\phi)} \phi.$$
%\end{proposition}
%Under the strict semantics locality  holds only for dependence logic formulas (see \cite{galliani12} for details).

In this article we study the  data complexity  of model-checking  of dependence, independence, and inclusion logic formulas. In other words, for a fixed formula $\varphi$ of one of the aforementioned logics, we study the complexity of the following model-checking  problem:  given a model  $\mA$ and a team $X$,  decide whether $\mA\models_X\phi$. 
%Note that when we are working with the lax semantics, we may assume without loss of generality that the  domain of $X$ is exactly $\Fr(\phi)$.

We assume that the reader is familiar with the basics of %computational 
complexity theory. %such as NP-completeness.


proofNLfragment.tex
\begin{proof}
The proof is given by a $\logspace$ reduction to the satisfiability problem of   $2$-CNF formulas which is well-known to be in $\nl$.
Given a structure $\mA$ and a  team $X$ we  construct a $2$-CNF propositional formula $\Phi$ such that:
\begin{equation}\label{indep-translation}
 \mA \models_X \varphi_1\vee \varphi_2 \iff \Phi \mbox{ is satisfiable.} 
\end{equation}

 Recall that if a team $X$ is such that  $\mA \models_X \varphi_1\vee \varphi_2$ then, there exists $Y, Z\subseteq X$ such that $Y\cup Z=X$ and $\mA \models_Y \varphi_1\mbox{ and } \mA \models_Z \varphi_2$.
 % \[  \mA \models_Y \varphi_1\mbox{ and } \mA \models_Z \varphi_2.\]
For each assignment $s\in X$, we introduce two Boolean variables $Y[s]$ and $Z[s]$. Our Boolean formula $\Phi$ will be defined below with these  $2|X|$ variables the set of which is denoted by $\Var(\Phi)$. It will express that the set of assignments must split into $Y$ and $Z$ but also make sure that incompatible assignments do not appear in the same subteam. 
 
For each pair $s_i,s_j$ that are incompatible for $\varphi_1$ on team $X$, one adds the $2$-clause: $\neg Y[s_i] \vee \neg Y[s_j]$. The conjunction of these clauses is denoted by $C_Y$.
Similarly, for each pair $s_i,s_j$ that are incompatible for $\varphi_2$ on team $X$, one adds the clause: $\neg Z[s_i] \vee \neg Z[s_j]$ and call $C_Z$  the conjunction of these clauses.

%\[
%\neg Y[s_i] \vee \neg Y[s_j]. 
%\]
%
%The conjunction of these clauses is denoted by $C_Y$.
%Similarly, for each pair $s_i,s_j$ that are incompatible for $\varphi_2$ on team $X$, one adds: 
%
%\[
%\neg Z[s_i] \vee \neg Z[s_j], 
%\]
%
%\noindent and analogously $C_Z$  denotes the conjunction of these clauses.
Finally, the construction of $\varphi$ is completed by adding the following conjunction:

\[ C\equiv \bigwedge_{s\in X} Y[s] \vee Z[s]. \]

It is not hard to see, due to the remark on compatible pairs, that the  formula $\Phi\equiv C\wedge C_Y\wedge C_Z$ can be built in $\logspace$.
 It remains to show that the equivalence \eqref{indep-translation} holds.
 
Assume that the left-hand side of the equivalence holds. Then, there exists $Y, Z\subseteq X$ such that $Y\cup Z=X$, $\mA \models_Y \varphi_1$ and  $\mA \models_Z \varphi_2$.
%\begin{equation}\label{disjunction} 
%  \mA \models_Y \varphi_1\mbox{ and } \mA \models_Z \varphi_2.
%  \end{equation}
% 
 We construct a propositional assignment $I:\Var (\Phi)\rightarrow \{0,1\}$ as follows. For all $s\in Y$, we set $I(Y[s])=1$ and for all $s\in Z$, we set similarly $I(Z[s])=1$. 
 
 Let us consider a clause  $ \neg Y[s_i] \vee \neg Y[s_j]$ for incompatible $s_i,s_j$. Then, $I(Y[s_i])=0$ or $I(Y[s_j])=0$ must hold. For a contradiction, suppose that $I(Y[s_i])=I(Y[s_j])=1$. Then since $\mA \models_Y \varphi_1$ holds, by construction $s_i$ and $s_j$ must be compatible for $\varphi_1$. Hence we get a contradiction and may conclude that $I$ satisfies $ \neg Y[s_i] \vee \neg Y[s_j]$. The situation is similar for each clause $\neg Z[s_i] \vee \neg Z[s_j]$. Finally since $X=Y\cup Z$, $I$ also satisfies $C$.
 
Let us then assume that  $\Phi$ is satisfiable, and let $I:\Var (\Phi)\rightarrow \{0,1\}$ be a satisfying assignment for $\Phi$. Since $I\models C$, we get that $I(Y[s])=1$ or $I(Z[s])=1$ for all  $s\in X$. Let 
   $$ X_{Y}=\{s : I(Y[s])=1\} \mbox{ and } X_{Z}=\{s : I(Z[s])=1\}.  $$
 Note that $X_Y\cup X_Z=X$.
 % \arnaud{This part of the proof should be checked carefully. I am not sure it is the best way to write it.}
 We will next show how the  sets $X_Y$ and $X_Z$ can be extended to sets $Y$ and $Z$ such that $\mA \models_Y \varphi_1$ and  $\mA \models_Z \varphi_2$.
 Note first that, since $I$ satisfies $\Phi$, for all $s_1,s_2\in X_{Y}$, $\Phi$ cannot have a clause of the form $\neg Y[s_1]\vee \neg Y[s_2]$, and hence $s_1,s_2$ are compatible for $\varphi_1$. Analogously we see that all  $s_1,s_2\in X_{Z}$ are compatible for  $\varphi_2$.
We will define the sets  $Y$ and $Z$ incrementally by first initializing them to  $X_Y$ and $X_Z$, respectively. Note that even if $X_Y\cup X_Z=X$, no decision has been made regarding the membership of   assignments $s$ in $Y$ (resp. $Z$) such that $I(Y[s])=0$ (resp. $I(Z[s])=0$).  Let us first consider $Y$. Until no changes occur,  we consider all pairs $s_1,s_2\in Y$ such that  $s_1(\tu z)= s_2(\tu z)$  and add into $Y$ (if they are not already in) all tuples $s_3\in X$ such that $s_3$ is a witness for the pair $(s_1,s_2)$ regarding property $\varphi_1$. Since by construction $s_1,s_2$ are compatible then at least one such  $s_3$ exists (but may be out of $Y$ till now). We prove below that this strategy is safe.
 %\begin{itemize}
 %\item either $s_1[\tu x_1]\neq s_2[\tu x_1]$. In this case, we simply add $s_1$ and $s_2$ if they are not in already.
  %\item or $s_1[\tu x_1]= s_2[\tu x_1]$. 
% In this case,
 %there exists $s_3,s_4\in X$ such that $\star(s_1,s_2,s_3,s_4)$ is true.
 % \[  s_1[\tu u_1]=s_3[\tu u_1], s_2[\tu v_1]=s_3[\tu v_1] \mbox{ and }  s_2[\tu u_1]=s_4[\tu u_1], s_1[\tu v_1]=s_4[\tu v_1].\]
First of all, it is  easily seen that any pair among $\{s_1,s_2,s_3\}$ is compatible for $\varphi_1$. Therefore, it remains to show that the new assignments $s_3$  are compatible with every other element $s$ added to $Y$ so far. Suppose this is not the case and that there exists $s\in Y\setminus \{s_1,s_2\}$ such that $s_3$ and $s$ are incompatible for $\varphi_1$. In passing one must have $s_3(\tu z)=s(\tu z)$. Since $s_1,s_2$, and $s$ are in $Y$ they are all pairwise compatible. Hence, there exists $t_1$ such that $t_1$ is a witness for the pair $(s_1,s)$.

Then,  $t_1(\tu x)=s_1(x)=s_3(\tu x)$, and  $t_1(\tu y)=s(\tu y)$. %Analogously, $t_2(\tu x)=s(\tu x)$ and $t_2(\tu y)=s_2(\tu y)=s_3(\tu y)$. 
 %But we also know that $s_2(\tu u_1)= s_4(\tu u_1)$ and $s_1(\tu v_1)= s_4(\tu v_1)$. 
 Consequently, $t_1$ is also a witness for $s_3,s$ hence, $s_3$ and $s$ are compatible which is a contradiction. Therefore,  the assignment $s_3$  can be safely added to $Y$. The set  $Z$ is defined analogously. %Note that $Y$ and $Z$ will not be necessarily disjoint.
By the construction, it holds that  $\mA \models_Y \varphi_1$  and  $\mA\models_Z \varphi_2$.
  
 
 %\[  \mA \models_Y \varphi_1  \mbox{ and } \mA\models_Z \varphi_2.\]
  
%\end{itemize}

%  Since the assignment $I$ also satisfy the subformula $C$ then, $X=Y\cup Z$.
  \end{proof}
  
notes.bbl
\begin{thebibliography}{10}
\providecommand{\bibitemdeclare}[2]{}
\providecommand{\surnamestart}{}
\providecommand{\surnameend}{}
\providecommand{\urlprefix}{Available at }
\providecommand{\url}[1]{\texttt{#1}}
\providecommand{\href}[2]{\texttt{#2}}
\providecommand{\urlalt}[2]{\href{#1}{#2}}
\providecommand{\doi}[1]{doi:\urlalt{http://dx.doi.org/#1}{#1}}
\providecommand{\bibinfo}[2]{#2}

\bibitemdeclare{article}{DBLP:journals/jphil/CiardelliR11}
\bibitem{DBLP:journals/jphil/CiardelliR11}
\bibinfo{author}{Ivano \surnamestart Ciardelli\surnameend} \&
  \bibinfo{author}{Floris \surnamestart Roelofsen\surnameend}
  (\bibinfo{year}{2011}): \emph{\bibinfo{title}{Inquisitive Logic}}.
\newblock {\sl \bibinfo{journal}{J. Philosophical Logic}}
  \bibinfo{volume}{40}(\bibinfo{number}{1}), pp. \bibinfo{pages}{55--94},
  \doi{10.1007/s10992-010-9142-6}.

\bibitemdeclare{article}{durand11}
\bibitem{durand11}
\bibinfo{author}{Arnaud \surnamestart Durand\surnameend} \&
  \bibinfo{author}{Juha \surnamestart Kontinen\surnameend}
  (\bibinfo{year}{2012}): \emph{\bibinfo{title}{Hierarchies in dependence
  logic}}.
\newblock {\sl \bibinfo{journal}{ACM Transactions on Computational Logic
  (TOCL)}} \bibinfo{volume}{13}(\bibinfo{number}{4}), p.~\bibinfo{pages}{31},
  \doi{10.1145/2362355.2362359}.

\bibitemdeclare{article}{DBLP:journals/corr/abs-1210-3321}
\bibitem{DBLP:journals/corr/abs-1210-3321}
\bibinfo{author}{Johannes \surnamestart Ebbing\surnameend},
  \bibinfo{author}{Juha \surnamestart Kontinen\surnameend},
  \bibinfo{author}{Julian{-}Steffen \surnamestart M{\"{u}}ller\surnameend} \&
  \bibinfo{author}{Heribert \surnamestart Vollmer\surnameend}
  (\bibinfo{year}{2014}): \emph{\bibinfo{title}{A Fragment of Dependence Logic
  Capturing Polynomial Time}}.
\newblock {\sl \bibinfo{journal}{Logical Methods in Computer Science}}
  \bibinfo{volume}{10}(\bibinfo{number}{3}), \doi{10.2168/LMCS-10(3:3)2014}.

\bibitemdeclare{article}{galliani12}
\bibitem{galliani12}
\bibinfo{author}{Pietro \surnamestart Galliani\surnameend}
  (\bibinfo{year}{2012}): \emph{\bibinfo{title}{Inclusion and exclusion
  dependencies in team semantics: On some logics of imperfect information}}.
\newblock {\sl \bibinfo{journal}{Annals of Pure and Applied Logic}}
  \bibinfo{volume}{163}(\bibinfo{number}{1}), pp. \bibinfo{pages}{68 -- 84},
  \doi{10.1016/j.apal.2011.08.005}.

\bibitemdeclare{inproceedings}{galhankon13}
\bibitem{galhankon13}
\bibinfo{author}{Pietro \surnamestart Galliani\surnameend},
  \bibinfo{author}{Miika \surnamestart Hannula\surnameend} \&
  \bibinfo{author}{Juha \surnamestart Kontinen\surnameend}
  (\bibinfo{year}{2013}): \emph{\bibinfo{title}{{Hierarchies in independence
  logic}}}.
\newblock In \bibinfo{editor}{Simona Ronchi~Della \surnamestart
  Rocca\surnameend}, editor: {\sl \bibinfo{booktitle}{Computer Science Logic
  2013 (CSL 2013)}}, {\sl \bibinfo{series}{Leibniz International Proceedings in
  Informatics (LIPIcs)}}~\bibinfo{volume}{23}, \bibinfo{publisher}{Schloss
  Dagstuhl--Leibniz-Zentrum fuer Informatik}, \bibinfo{address}{Dagstuhl,
  Germany}, pp. \bibinfo{pages}{263--280}, \doi{10.4230/LIPIcs.CSL.2013.263}.
\newblock \urlprefix\url{http://drops.dagstuhl.de/opus/volltexte/2013/4202}.

\bibitemdeclare{inproceedings}{gallhella13}
\bibitem{gallhella13}
\bibinfo{author}{Pietro \surnamestart Galliani\surnameend} \&
  \bibinfo{author}{Lauri \surnamestart Hella\surnameend}
  (\bibinfo{year}{2013}): \emph{\bibinfo{title}{{Inclusion Logic and Fixed
  Point Logic}}}.
\newblock In \bibinfo{editor}{Simona Ronchi~Della \surnamestart
  Rocca\surnameend}, editor: {\sl \bibinfo{booktitle}{Computer Science Logic
  2013 (CSL 2013)}}, {\sl \bibinfo{series}{Leibniz International Proceedings in
  Informatics (LIPIcs)}}~\bibinfo{volume}{23}, \bibinfo{publisher}{Schloss
  Dagstuhl--Leibniz-Zentrum fuer Informatik}, \bibinfo{address}{Dagstuhl,
  Germany}, pp. \bibinfo{pages}{281--295}, \doi{10.4230/LIPIcs.CSL.2013.281}.
\newblock \urlprefix\url{http://drops.dagstuhl.de/opus/volltexte/2013/4203}.

\bibitemdeclare{article}{DBLP:journals/networks/GeigerVP90}
\bibitem{DBLP:journals/networks/GeigerVP90}
\bibinfo{author}{Dan \surnamestart Geiger\surnameend}, \bibinfo{author}{Thomas
  \surnamestart Verma\surnameend} \& \bibinfo{author}{Judea \surnamestart
  Pearl\surnameend} (\bibinfo{year}{1990}): \emph{\bibinfo{title}{Identifying
  independence in bayesian networks}}.
\newblock {\sl \bibinfo{journal}{Networks}}
  \bibinfo{volume}{20}(\bibinfo{number}{5}), pp. \bibinfo{pages}{507--534},
  \doi{10.1002/net.3230200504}.

\bibitemdeclare{article}{DBLP:journals/tcs/Gradel92}
\bibitem{DBLP:journals/tcs/Gradel92}
\bibinfo{author}{Erich \surnamestart Gr{\"{a}}del\surnameend}
  (\bibinfo{year}{1992}): \emph{\bibinfo{title}{Capturing Complexity Classes by
  Fragments of Second-Order Logic}}.
\newblock {\sl \bibinfo{journal}{Theor. Comput. Sci.}}
  \bibinfo{volume}{101}(\bibinfo{number}{1}), pp. \bibinfo{pages}{35--57},
  \doi{10.1016/0304-3975(92)90149-A}.

\bibitemdeclare{article}{gradel12}
\bibitem{gradel12}
\bibinfo{author}{Erich \surnamestart Gr{\"a}del\surnameend}
  (\bibinfo{year}{2013}): \emph{\bibinfo{title}{Model-checking games for logics
  of imperfect information}}.
\newblock {\sl \bibinfo{journal}{Theor. Comput. Sci.}} \bibinfo{volume}{493},
  pp. \bibinfo{pages}{2--14}.
\newblock \urlprefix\url{http://dx.doi.org/10.1016/j.tcs.2012.10.033}.

\bibitemdeclare{article}{gradel10}
\bibitem{gradel10}
\bibinfo{author}{Erich \surnamestart Gr\"adel\surnameend} \&
  \bibinfo{author}{Jouko \surnamestart V\"a\"an\"anen\surnameend}
  (\bibinfo{year}{2013}): \emph{\bibinfo{title}{Dependence and Independence}}.
\newblock {\sl \bibinfo{journal}{Studia Logica}}
  \bibinfo{volume}{101}(\bibinfo{number}{2}), pp. \bibinfo{pages}{399--410},
  \doi{10.1007/s11225-013-9479-2}.

\bibitemdeclare{inproceedings}{DBLP:conf/foiks/HannulaK14}
\bibitem{DBLP:conf/foiks/HannulaK14}
\bibinfo{author}{Miika \surnamestart Hannula\surnameend} \&
  \bibinfo{author}{Juha \surnamestart Kontinen\surnameend}
  (\bibinfo{year}{2014}): \emph{\bibinfo{title}{A Finite Axiomatization of
  Conditional Independence and Inclusion Dependencies}}.
\newblock In \bibinfo{editor}{Christoph \surnamestart Beierle\surnameend} \&
  \bibinfo{editor}{Carlo \surnamestart Meghini\surnameend}, editors: {\sl
  \bibinfo{booktitle}{Foundations of Information and Knowledge Systems - 8th
  International Symposium, FoIKS 2014, Bordeaux, France, March 3-7, 2014.
  Proceedings}}, {\sl \bibinfo{series}{Lecture Notes in Computer Science}}
  \bibinfo{volume}{8367}, \bibinfo{publisher}{Springer}, pp.
  \bibinfo{pages}{211--229}, \doi{10.1007/978-3-319-04939-7\_10}.

\bibitemdeclare{article}{DBLP:journals/corr/HannulaK14}
\bibitem{DBLP:journals/corr/HannulaK14}
\bibinfo{author}{Miika \surnamestart Hannula\surnameend} \&
  \bibinfo{author}{Juha \surnamestart Kontinen\surnameend}
  (\bibinfo{year}{2015}): \emph{\bibinfo{title}{Hierarchies in independence and
  inclusion logic with strict semantics}}.
\newblock {\sl \bibinfo{journal}{J. Log. Comput.}}
  \bibinfo{volume}{25}(\bibinfo{number}{3}), pp. \bibinfo{pages}{879--897},
  \doi{10.1093/logcom/exu057}.

\bibitemdeclare{article}{2014arXiv1409.5537H}
\bibitem{2014arXiv1409.5537H}
\bibinfo{author}{T.~\surnamestart {Hyttinen}\surnameend},
  \bibinfo{author}{G.~\surnamestart {Paolini}\surnameend} \&
  \bibinfo{author}{J.~\surnamestart {V{\"a}{\"a}n{\"a}nen}\surnameend}
  (\bibinfo{year}{2014}): \emph{\bibinfo{title}{{Quantum team logic and Bell's
  Inequalities}}}.
\newblock {\sl \bibinfo{journal}{ArXiv e-prints}},
  \doi{10.1017/S1755020315000192}.

\bibitemdeclare{article}{kontinenj13}
\bibitem{kontinenj13}
\bibinfo{author}{Jarmo \surnamestart Kontinen\surnameend}
  (\bibinfo{year}{2013}): \emph{\bibinfo{title}{Coherence and Computational
  Complexity of Quantifier-free Dependence Logic Formulas}}.
\newblock {\sl \bibinfo{journal}{Studia Logica}}
  \bibinfo{volume}{101}(\bibinfo{number}{2}), pp. \bibinfo{pages}{267--291},
  \doi{10.1007/s11225-013-9481-8}.

\bibitemdeclare{article}{KontinenKLV11}
\bibitem{KontinenKLV11}
\bibinfo{author}{Juha \surnamestart Kontinen\surnameend},
  \bibinfo{author}{Antti \surnamestart Kuusisto\surnameend},
  \bibinfo{author}{Peter \surnamestart Lohmann\surnameend} \&
  \bibinfo{author}{Jonni \surnamestart Virtema\surnameend}
  (\bibinfo{year}{2014}): \emph{\bibinfo{title}{Complexity of two-variable
  dependence logic and IF-logic}}.
\newblock {\sl \bibinfo{journal}{Inf. Comput.}} \bibinfo{volume}{239}, pp.
  \bibinfo{pages}{237--253}, \doi{10.1016/j.ic.2014.08.004}.

\bibitemdeclare{article}{DBLP:journals/corr/KontinenKV14}
\bibitem{DBLP:journals/corr/KontinenKV14}
\bibinfo{author}{Juha \surnamestart Kontinen\surnameend},
  \bibinfo{author}{Antti \surnamestart Kuusisto\surnameend} \&
  \bibinfo{author}{Jonni \surnamestart Virtema\surnameend}
  (\bibinfo{year}{2014}): \emph{\bibinfo{title}{Decidable Fragments of Logics
  Based on Team Semantics}}.
\newblock {\sl \bibinfo{journal}{CoRR}} \bibinfo{volume}{abs/1410.5037}.
\newblock \urlprefix\url{http://arxiv.org/abs/1410.5037}.

\bibitemdeclare{book}{vaananen07}
\bibitem{vaananen07}
\bibinfo{author}{Jouko \surnamestart V\"a\"an\"anen\surnameend}
  (\bibinfo{year}{2007}): \emph{\bibinfo{title}{Dependence Logic}}.
\newblock \bibinfo{publisher}{Cambridge University Press},
  \doi{10.1017/CBO9780511611193}.

\end{thebibliography}
