\section{Definitions and Notation}
\label{defs}
We list some relevant notions\footnote{under construction}. We assume 
familiarity with the following:
\bit
\item
Basic proof theory
\item
\fo logic programming
\item
\fo and \ho unification
\enit


% We will  give the very basic notions of \ho logic programming

% \begin{Definition} [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{Definition}

% \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}$
\beq
A & ::= & a\mid (c\ a_{1}\mdots a_{n})\mid A_{1}\Imp A_{2}
\eneq
\enef

Order of types and of Goals


% Core language: for the Elf language \cite{Pfe9?}, under the Curry-Howard iso, we can 
% identify universals and implication, the latter being an empty $\Pi$.

% \beq
% G & ::= & P\mid G_{1}\Imp G_{2}\mid \Pi x:A.G\\
% D & ::= & P \If G \\
% \cP & ::= & \cdot\mid D,\cP
% \eneq


% \bedef [(local) stratification]
% \label{d:strat}
% \enef

% It can be shown that this equivalent to the following extended language 
% \cite{Mi89,Har90}: we will sometimes use the latter for sake of brevity

% \beq
%  D & ::= & A |\top| G \supset D| \forall x:A.D| D_1 \And D_2 \\
% G &::= & A |\top | G_1 \And G_2 | G_1 \lor G_2 | \forall x:A.G | 
% \exists x:A.G | D \supset G \\
% \eneq

% Uniform proofs judgments
% \[
% \begin{array}{ll}
% \cP\prv_{u} G & \mbox{Program $\cP$ uniformly entails $G$}\\
% \cP\prv_{u} D >> P & \mbox{Clause  $D$ immediately entails atom $P$ under  
% $\cP$}
% \end{array}
% \]
 
% % \newcommand{\vsk}{\\[2ex]}
% \[
% \begin{array}{c}
% \ianc{G_{1}, \cP\prv_{u} G_{2}}{\cP\prv_{u} G_{1}\Imp G_{2}}{S\Imp}
% \qquad
% \ianc{\cP\prv_{u}\forall x. G}{\cP\prv_{u} [a/x]G}{S\forall^{*}}\vsk
% \ianc{} {P >> P}{I-atom}
% \qquad
% \ianc{\cP\prv_{u} D >> P \quad\mbox{for $D$ in $\cP$}}{\cP\prv_{u} P}{S-atom} \vsk
% \ianc{\cP\prv_{u} G}{\cP\prv_{u} (G_\Imp P) >> P}{I\Imp}
% \qquad
% \ianc{\cP\prv_{u}\forall x.G >> P}{\cP\prv_{u} [t/x]G >> P}{I\forall}
% \end{array}
% \]
% The rule $S\forall^{*}$  is restricted to the case where the 
% parameter $a$ does not occur in $\cP$ nor in $\forall x.G$.

\smallskip
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).






