
\newcommand{\eq}{\eqd}  
\newcommand{\yield}{\Rightarrow}
\renewcommand{\neq}{\not\eqd}
\newcommand{\alg}{aug_{\mbox{\tiny \textrm{G}}}}
\newcommand{\ald}{aug_{\mbox{\tiny \textrm{D}}}}
\newcommand{\gfald}{\ga\vd_{\!\Phi}\ald} %changed
\newcommand{\gfalg}{\Gamma;\cD\prv_{\!\Phi}\alg}
\newcommand{\mnota}{{\rm Not}_{\mbox{$\alpha$} }}
\newcommand{\mnotd}{{\rm Not}_{\rm D}  }
\newcommand{\mnotg}{{\rm Not}_{\rm G}  }
 \newcommand{\mnotxi}{\mnot^i_x}
\renewcommand{\sp}{\vd_{\!\cP}}
\newcommand{\spp}{\vd_{\!\PP}}
\newcommand{\snp}{\vd_{\!\PM}\mnotg}
\newcommand{\sn}{\vd_{\!\PM}}


%\newcommand{\allxa}{\forall x\!:\!A.\,}
\newcommand{\fpp}{\nvd_{\!\PP}}
\newcommand{\fnp}{\nvd_{\!\PM}\mnotg }
\newcommand{\fn}{\nvd_{\!\PM}}
\newcommand{\fp}{\nvd_{\!\cP}}
\newcommand{\cA}{{\cal A}}
\newcommand{\cT}{{\cal T}}
\newcommand{\cJ}{{\cal J}}
\newcommand{\tensor}{\oplus}
\newcommand{\ga}{\Gamma;\cD }
\newcommand{\gna}{ \Gamma;\cD }
\newcommand{\vS}{\vec{S}}
%\newcommand{\vM}{\vec{M}}
\newcommand{\PA}{\mid \cP\mid}
\newcommand{\eqd}{\stackrel{\cdot}{=}}
\newcommand{\neqd}{\not\stackrel{\cdot}{=}}
\newcommand{\imm}{>\!\!>}
\newcommand{\nimm}{\imm}
\newcommand{\IP}{{\cal I}^{+}}
\newcommand{\IM}{{\cal I}^{-}}
\newcommand{\SP}{{\cal S}^{+}}
\newcommand{\SM}{{\cal S}^{-}}
%\newcommand{\gf}{\Gamma;\cD\vd_{\!\Phi}^{\! Q}} CHANGE (Input
%variables \Phi
\newcommand{\gf}{\Gamma\vd}
%\newcommand{\gf}{\Gamma\vd^{\! Q}}
\newcommand{\gfq}{}
%\newcommand{\gfq}{q\oftp \An\Imp\prop\vd}
% \newcommand{\vdf}{\vd_{\!\Phi}} input variables
\newcommand{\vdf}{\vd_{\!\cP}}
\newcommand{\foq}{\mbox{\textrm{for all }$ \q$  }}
\renewcommand{\emp}{\cdot;\top}
\newcommand{\csa}{\cS^a}
\newcommand{\yd}{\stackrel{\mbox{\tiny{$D$}}}{\Longrightarrow}}
\newcommand{\yg}{\stackrel{\mbox{\tiny{$G$}}}{\Longrightarrow}}
\newcommand{\less}{\prec} 
\newcommand{\boxarray}[1]{\[\fbox{$\begin{array}
      {c}\mbox{}\vsk #1\mbox{}\vsk\end{array}$}\]}
% call with the context of the array


%\newcommand{\bsu}{\` By subst.}

\chapter{Clause Complementation}
\label{ch:cc}

%\input{intro5}

\input{htermprf}

\input{context}

\input{cc}

\input{augment}

\input{excluproof}

\input{exh}

\input{tensor}










% \section{Clause Complementation}
% \label{sec:alge}


% We now introduce in Figure \ref{fig:notd} and Figure \ref{fig:notg} the
% rules for (static) clause and goal complementation. 
% We  collect essentially existential variables in a pool $\Phi$
% left here, for the moment, implicit. $\Pi(Q\If \top)$ denotes the
% universal closure of (all) the free variables in $Q$.


% Note that rule $\mnotd\Imp$ is where all the work is done: a set of
% negative facts is built via term complementation $\cdot\vd\mnot
% (\vM)$, whose fresh free variables
% are universally closed and the negative counterpart of the source
% clause is obtained via complementation of the body. The original
% quantification is retained thanks to rule $\mnotd\Pi$.




% \section{Augmentation}



% Judgments:
% \bit
% \item
% $\gf\mnota(\cD)$:
% Complementation of the dynamic definitions in $\cD$ \wrt an atom $Q$ and input terms $\Phi$.
% \item
% $\gf\mnota(D)$:   Complementation of assumption
%   $D$.
% \item
% $\gf\mnot^x(D)$:   Complementation of assumption $D$ \wrt $x$.
% \item
% $\gf\mnotxi(D)$:   Complementation of assumption $D$ \wrt $x$ and
%   position $i$.
% \item
% $\gfald(D)$:   Augmentation of clause $D$.
% \item
% $\gfalg(G)$:   Augmentation of goal $G$
% \enit
% where,
% \begin{itemize}
% \item $\GG$ is a list of  parameters.
% \item $\cD$ is a conjuction of  assumption.
% \item $\Phi$ is a list of  \emph{input} evars.
% \end{itemize}



% We present two definitions: the first (eager complementation) computes
% complementation of ground terms via the auxiliary judgment $\gf\mnotxij
% (D) \yield D'$, while the second (lazy complemetation) always
% introduces disequations, even when they are unsatisfiable:

% \begin{Definition}[Eager Assumption Complementation]
%   \label{def:nota}
% Let 
% for  $0\leq j\leq n$, 
% $Z_j$ be a fresh logic variable of correct type: the judgment
% $\gf\mnotxi(D)=D'$ is realized by the following rules:
%   \[
%   \begin{array}{c}
%  \ianc{}{\gf\mnotxi(\bot_q)  =   \top_q}{\mnotxi\bot}\vsk
%     \ianc{head(Q)=q, \Sigma(q)= \An\Imp \prop}
%     {\gf\mnotxi(\top_q)  =
%       \PI{Z_1}{A_1}\dots\PI{Z_n}{A_n} \neg q\ Z_1\dots Z_{i-1}\ x\
%       Z_{i+1}\dots Z_n}{\mnotxi\top}\vsk
% %\mbox{no case for $\GG=\cdot$}\footnote{\mbox{does not make sense,
% %    since $x\in\GG$}}\vsk 
%  %  \ianc{M_i \mbox{ \ \textrm{closed}}}
% %   {\GG,x\oftp A\vdf \mnotxi\ q(M_1\mdots  M_i\mdots M_m, x,\Nn) \yield 
% %     \BAnd_{N\in\cdot\vd\mmnot M_i}\Pi(\neg q(M_1\mdots N\mdots M_m,
% %     x,\Nn)\If\top) }{\mnotxi\mmnot}\vsk
% %   \ianc{M_i
% % \mbox{ \textrm{no case for $M_j$ local gvar}}\vsk
% %{\gf\mnotxi  q(M_1\mdots  M_i\mdots M_m,
% %      x,\Nn)\yield \top}{\mnotxi At\_else}\vsk
%   \ibnc{\gf\mnotxi(D_1) =  D_1'}{\gf\mnotxi(D_2) =  D_2 '}
%     {\gf\mnotxi(D_{1}\And D_{2})  =  D_{1}'\tensor D_{2}'}{\mnotxi\And}\vsk
%     \ibnc{\gf\mnotxi(D_1) =  D_1'}{\gf\mnotxi(D_2) =  D_2 '}
%     {\gf\mnotxi(D_{1}\tensor D_{2})  =  D_{1}'\And
%     D_{2}'}{\mnotxi\tensor}\vsk
%   \ianc {\gf \mnotxi(D)= D' }{\gf\mnotxi(\PI{y}{B} D)= \PI{y}{B}
%     D'}{\mnotxi\Pi}\vsk
%   \ianc{p\not\equiv head(Q)}{\gf\mnotxi(p\ \Mn\If G)= \top_q}{\mnotxi At-nmr}\vsk
%     \ibnc{\gf\mnotxij(q\ \Mn)=D'}{\gf\mnotg(G) =  G'}{\gf\mnotxi(q\ \Mn\If G )=
%     D'\And\neg q\ \Mn \If G'}{\mnotxi\If}\vsk\vsk

%     \ianc{ \exists j\oftp 1\leq j\leq n, j\not\equiv i\,.\,M_j\in\GG\cup\Phi
%    }{\gf\mnotxij  (q\ \Mn)\yield
%     \PI{Z_1}{A_1}\dots\PI{Z_n}{A_n} \neg q\ Z_1\dots Z_{i-1}\ x\
%     Z_{i+1}\dots Z_n\If M_j\neqd Z_j}{\mnotxij Atc}\vsk
%      \ianc{\exists j\oftp 1\leq j\leq n, j\not\equiv i}
%      {\gf\mnotxij  (q\ \Mn)\yield\BAnd_{N\in\mnot(M_j)}\Pi(
%     %\PI{Z_1}{A_1}\dots\PI{Z_n}{A_n} 
%        \neg q\ Z_1\dots\ N\ \dots\ x\ 
%        \dots Z_n)\If\top_q}{\mnotxij At}
%   \end{array}
%   \]
% where
% $$\gf\mnotxij(D)=\BAnd D'\mid \gf\mnotxij(D)\yield D'$$
% \end{Definition}

% In the rule $\mnotxij At$ we choose a term $M_j$ in the source atom
%   such that it is either an input term or another parameter, in a CLP
%   style, we add the relative disequation. Otherwise we compute its
%   complement with a call to $\mnot$. In particular, if $M_j$ is an
%   essentially existential variable, its complement is empty and
%   $\top_Q$ is returned.

% \begin{Definition}[Lazy Assumption Complementation]
%   \label{def:lazynota}
% The judgment
% $\gf\mnotxi(D)= D'$ is realized by the following rules:
%   \[
%   \begin{array}{c}
%     \ianc{}{\gf\mnotxi(\bot_q)  =   \top_q}{\mnotxi\bot}\vsk
%    %  \ianc{head(Q)=q, \Sigma(q)= \An\Imp \prop}
% %     {\gf\mnotxi(\top_q)  =
% %       \PI{Z_1}{A_1}\dots\PI{Z_n}{A_n} \neg q\ Z_1\dots Z_{i-1}\ x\
% %       Z_{i+1}\dots Z_n}{\mnotxi\top}\vsk
% %     \ibnc{1\leq j\leq n,j\not = i}{\GG\vd\mnotg(G)=G'}{\begin{array}{l}
% % \gf\mnotxi  (q\ \Mn\If G)=
% %     \BAnd\PI{Z_1}{A_1}\dots\PI{Z_n}{A_n} \neg q\ Z_1\dots Z_{i-1}\ x\
% %     Z_{i+1}\dots Z_n\If M_j\neqd Z_j\\
% %     \mbox{}\And \neg q\ \Mn\If G'\end{array}}{\mnotxi At}\vsk
% %   \ianc{p\not\equiv head(Q)}{\gf\mnotxi(p\ \Mn\If G)= \top_q}{\mnotxi At-nmr}\vsk
% %   \ibnc{\gf\mnotxi(D_1) =  D_1'}{\gf\mnotxi(D_2) =  D_2 '}
% %     {\gf\mnotxi(D_{1}\And D_{2})  =  D_{1}'\tensor D_{2}'}{\mnotxi\And}\vsk
% %     \ibnc{\gf\mnotxi(D_1) =  D_1'}{\gf\mnotxi(D_2) =  D_2 '}
% %     {\gf\mnotxi(D_{1}\tensor D_{2})  =  D_{1}'\And
% %     D_{2}'}{\mnotxi\tensor}\vsk
% %   \ianc {\gf \mnotxi(D)= D' }{\gf\mnotxi(\PI{y}{B} D)= \PI{y}{B} D'}{\mnotxi\Pi}
% %   \end{array}
% %   \]
% % \end{Definition}



% %  Remark that there are three-layers: once we have collected the complement of an assumption
% % \wrt to $x$ and a given position $i$, we need to do the same for every
% % other position $x$ can occur in the atom we are complementing
% % with. Once this is done, we proceed to do it again \wrt every
% % parameter in $\GG$ whose type (for the time being only of base type)
% % can be used in building argument to the pivot atom.


% \begin{Lemma}
% \label{le:defnot}
% Let $\ga\vdf\mnota(\cD)=\cD_{\neg}$. Then $D\in def(q,\ga)$ iff $D\in
% def(q,\GG;(\cD\And\cD_{\neg})$.
% \end{Lemma}
% \begin{proof}
% A straightforward induction on the structure of $D$.
% \end{proof}

% We call a clause or a goal \emph{positive} if it contains no
% occurrance of a negative literal.

% \begin{Theorem}[Positive Conservativity]
% \label{thm:conservaug}
% If $G$ is positive, then $\ga\vdf G$ iff $\ga\vdf\alg(G)$.
% \end{Theorem}

% \begin{proof}
% We generalize this...
% \end{proof}
















