\subsection{Outline}


This dissertation is organized in two main parts which address:
\begin{itemize}
\item The relative  complement problem for \ho patterns.
\item Clause complementation for a fragment of third-order Hereditary Harrop formulae.
\end{itemize}


We start in Chapter~\ref{ch:el-rel} by introducing the relative
complement problem; we review the existing solutions to the \fo case
in the literature, namely a variant of Lassez \& Marriot's original
\emph{uncover} algorithm \cite{Lassez87} (Section~\ref{sec:bnot}) and
\emph{disunification} \cite{Comon91} (Section ~\ref{sec:disunif}). We
then discuss in Section \ref{sec:hocomplement} the problems connected
to extending those idea to the \ho case, where we notice the
fundamental difference between \emph{fully} and \emph{partially applied
  terms}. For the latter fragment, the simply-typed $\l$ calculus is
not closed under term complement. We remedy this by introducing the
\emph{strict} $\l$-calculus in Chapter~\ref{cap:strict}. We develop
the system and mention  the existence of canonical forms.
Once we have  a calculus strong enough to deal with partially
applied terms, Section \ref{sec:strictcomp} introduces a restriction of the language
(``simple terms'') for which complementation is possible.  The
algorithm for negation is presented in Section \ref{sec:compl}; in
Section \ref{sec:sunif} we give a unification algorithm for the same
fragment. This completes our solution to the relative complement
problems for \ho patterns. We conclude this chapter in Section~\ref{sec:algebra} by
showing how to organize finite sets of simple terms into a boolean
algebra. We end up this part of the dissertation reviewing related
work on strictness (Section \ref{sec:relstrict}).

Chapter~\ref{ch:hornelim} sets the stage for clause complementation.
First, in Section~\ref{sec:what}, we offer a  reconstruction
of the transformational approach to negation in the Horn case. Then in
Section~\ref{sec:intro5} and \ref{sec:completion} we give an informal
view of the complement algorithm for HHF and of the restrictions it
requires by means of examples.  In Section \ref{sec:motiv} we try to
motivate the pragmatic adequacy of the fragment of HHF we deal with, while
Section \ref{sec:lamrelated} reviews the state of the art in \NF and
intuitionistic provability.


Chapter \ref{ch:cc} is the heart of the thesis; we first introduce the
source language and its uniform proofs system in
Section~\ref{sec:logic}.  We then establish the fundamental notion of
context schema (Section~\ref{sec:runtime}). This allows to enforce
the \emph{Regular World Assumption} (RWA), on which clause
complementation is built.  After formalizing the restriction to
terminating programs in Section \ref{sec:termination}, we present the
clause complementation algorithm and the related notion of
\emph{augmentation} (Section~\ref{sec:cc} and \ref{sec:aug}). We
then prove the main theorem (Section~\ref{sec:excluproof} and
\ref{sec:exh}).  Finally, Section~\ref{sec:ref} discusses how to give an
operational semantics to our language.

We conclude the dissertation in Chapter~\ref{ch:end} by discussing
first how to lift some of the current restrictions
(Section~\ref{sec:lift}); then we address possible extensions,
implementation issues and further future work (Section \ref{sec:extend},
\ref{sec:iissues} and \ref{sec:additional}).




\section{Contributions and Technical Acknowledgments}

The original contribution of the thesis are:
\bit
\item
A relative complement algorithm for \ho patterns internalized into a strict
type theory.
\item
A complement algorithm for a useful class of third-order hereditary
Harrop formulae.
\enit

We contend that our approach is the first one to give a realistic
analysis of negation in logical frameworks with an emphasis on the
development of a practical tool to incorporate this operator in
existing languages.

This work has benefited enormously from the large ensemble of research
collected in the Elf and offspring projects: not only form the
existence of this language and environment, but also from
specific contributions which we have used (in a somewhat simplified setting) in
this thesis.  Let me mention only the most recent ones:  schema
contexts (Sch{\"u}rmann \cite{Schurmann00phd}), linear
unification (Cervesato and Pfenning \cite{Cervesato96lics}),
 subordination (Virga \cite{Virga99phd}), mode and
termination analysis (Rohwedder and Pfenning \cite{Rohwedder96esop}).

% Finally, I want to point out that Frank Pfenning originally suggested,
% among others, the idea of using strict types to enforce variables
% occurrences and the idea of the Regular World Assumption to make
% clause complementation feasible.

This research has been financially supported for seven semesters by the
Department of Philosophy at CMU and by a one-year scholarship from
``Consiglio Nazionale delle Ricerche'', Italy.



