\section{Motivation}


%\subsection{not allowed}
Consider the following:
$even'(ssN)\If even'(0)\Imp even' (N)$, which enumerates $2,4...$.
Augmentation incorrect as $\neg even sM$ will overlap with factual
part $\neg even 0\And \neg even s0$. Tensoring the two would be wrong,
as we would violate the scope. If assumption is guarantted to
contain a parameter, then no overlapping is possible between dynamic
and static information.

As we have mentioned in \ref{sec:lamrelated}, N-Prolog, and a fortiori
hhf are \emph{not} closed under complementation. Differently from how
we have approached the analogous issue \wrt term complementation, we
will not extend the framework, but we will restrict to a sublanguage
for which closure under complementation holds and that we deem
encompassing most of the applications we are interested in. In
\cite{Giordano98} the authors show that the general case would require
swtching to a three-valued modal logic, which would serve no other
apparant purpose as a logic framework. This is to be compared with
the strict $\l$-calculus, which has an interset in its own and is
amenable of an implementation alonf the lines of \emph{LF}. Moreover
the distinction between which may or ought not depend on its argument
is a sharp one. 


\smallskip

While we have in the background an assumption as the CWA and the
completion, it is a characteristic of hhf that the completion in
itself is not enough to determine the behaviour of a program under
complementation. We will have to insert, at compile time,  additional structure in a
predicate definition so as to completely determine the provability and
failure of goals which mention \emph{parameters}. This procedure which
we describe in \ref{sec:augment} is fairly complex: we thus try to
motivate it with some examples.

\begin{Example}[copy]

\end{Example}