\appendix

\section{Definitions and Notation}
\label{defs}
We list some relevant notions\footnote{under construction}.

\begin{Def} [Terms as trees] Consider $\la \cN^*, \cdot, \Lambda 
\ra$, the monoid of sequences of natural numbers, called {\em 
positions} with concatenation as the binary operator and the empty 
sequence as the neuter element. Further, we call a set of 
positions $P \subseteq \cN^*$ {\em prefix-closed} iff for all 
$p,q,r \in \cN^*$: $p = q \cdot r \Rightarrow q \in P$. For $p \in P, 
succ(p) =\{q \in P \mid \exists i: q =p \cdot i\}$. A {\em term}  $t$ 
over an signature $\Sigma$ and an set $X$ of variables is  a pair $\la 
P, l_\Sigma \ra$ satisfying the following conditions:
\begin{enumerate}
\item
$P \subseteq \cN^*$ is prefix-closed
\item
$l_\Sigma : P \longrightarrow \Sigma \cup X$
\item 
If $ f \in \Sigma$ and $arity(f)=n >0$, then $l_\Sigma(p) = f$ 
implies that $succ(p) = \{p\cdot 1\mdots p\cdot n \}$.
\end{enumerate}

\end{Def}
\bedef [Contexts] $E[F]$ denotes that the subexpression $F$ inside 
the brackets has at least one occurrence in $E$.
\enef
\bedef
[Linear] A term $u$ is {\em linear} if there is no multiple occurrence 
of the same variable therein. The term $\q t$ is called {\em 
restricted} \wrt $t$ if either there is $x \in t$ such that $\q x$ is 
not linear or 
there are two distinct variables $x_1,x_2 \in t$ such that $\q x_1$ 
and $\q x_1$ share a variable.
\enef
\bedef
[Universal(Existential) closure]
\enef
\bedef [Substitutions]
\enef
\bedef[Ground, Instance, Term Subsumption]
\enef
\begin{Notation} [Tuples and Variables]
We write $\vt$ for a tuple of elements, in this case terms, whose 
length is unimportant:
$\tn$ will be used as an abbreviation of $t_1 \mdots t_n$. Note that 
this notation assumes the properties of finite sets, \ie $\vx$ stands 
both for $x,x\prime$ and $x\prime,x$. Further, $\xn,\ym,\zp$  and 
their vectorized version are intended to stand resp.\ for tuples  
(sets)  of existential, universal and free variables. They are assumed 
to be disjoint: $\wr$ will be used to stand for a tuple of either free 
or existentially quantified variables. $\tm = \sm$ (resp.\ $\tm 
\nq\sm$) will  
stand for 
\[\BAnd^m_{i=1} t_i = s_i  \quad \quad\quad\BOr^m_{i=1} t_i \nq s_i\]
 taking the place sometimes of the more cumbersome notation 
\[\ol{\tm = \sm}\].
Notation for substitution: $[M/x]N$.
\end{Notation}

For a syntactic object ${\cal O}$, $FV({\cal O})$ will denote the set 
of its free variables.


\bedef [simple types] For every type $\alpha$ we assume a set $\cal 
C_{\alpha}$ of constants and countably infinite set of variables
$\cal 
V_{\alpha}$ such that disjoint \ldots. Put $\Sigma = \bigcup_{\alpha 
\in \cal T} C_{\alpha}$
\bedef [(local) stratification]
\label{d:strat}
\enef
Discussion of the \label{uqb} {\ul Universal Query Problem}: In Logic 
textbook a \fo language usually contains an infinite set of function 
symbol. On 
the other hand, the signature of (the language of) a program is finite. 
in the \lp\ community this seemingly innocent issue became hot 
\wrt the semantics of negation-as-failure. Kunen \cite{Kun87} and 
later Shepherdson \cite{} advocated a return to the former approach 
which makes the treatment of $CET$ nicer. Afterwards Maher 
\cite{Mah88} set the records straight (to be continued).
