\documentclass{book}[12pt]
 \usepackage{fullpage}
\usepackage{latexsym}
\usepackage{amsfonts}
\usepackage{cdsty2}
%\usepackage{prooftree}
\usepackage{fancyheadings}
%\usepackage{amtitlepage}
\def\zzctdrawdotedge{\drawdotedge{4pt}0}
\def\ctabutborderlr{1em}
\def\ctabutbordertb{1ex}
 \lhead[\fancyplain{}{\thepage}]{\fancyplain{}{\rightmark}}
 \rhead[\fancyplain{}{\leftmark}]{\fancyplain{}{\thepage}}
 \cfoot{\footnotesize \it Draft of \today}
\usepackage{lcom}
\usepackage{thesis}



\begin{document}
\bibliographystyle{alpha}

% \title{Elimination of Negation in a Logical Framework}

% \author{Alberto Momigliano
% \date{\today}
% % \keywords{
% %    negation,
% %    logical framework,
% %    negation-as-failure,
% %    higher-order logic programming,
% %    strict $\lambda$-calculus,
% %    regular world assumption
% %  }
% \citationinfo{\begin{center} \emph{Submitted in partial fulfillment of
%       the requirements} \\
%  \emph{for the degree of Doctor of Philosophy} \\[1cm]
%   \textbf{Thesis Committee:} \\
%   Frank Pfenning, Chair \\
%   Dana Scott \\
%   Dale Miller, Pennsylvania State University 
% \end{center}}

% \copyrightnotice{Copyright \copyright\  2000 Alberto Momigliano}

% \clearpage

% \abstract{We address the issue of endowing a logical framework 
%   with a logically justified notion of negation. Logical frameworks with
%   a logic programming interpretation such as hereditary Harrop
%   formulae  cannot directly express  negative information,
%   although negation is a useful specification tool.  Since
%   negation-as-failure does not fit well in a logical framework,
%   especially one endowed with hypothetical and parametric judgments,
%   we adapt the idea of \emph{elimination} of negation from Horn logic
%   to a fragment of higher-order hereditary Harrop
%   formulae. The idea is to replace occurrences
%   of negative predicates with  positive ones which are
%   operationally equivalent. This entails two separate phases.
% \vsk
%   \emph{Complementing terms}, i.e.\  in our case higher-order patterns. Due the
%   presence of \emph{partially applied} lambda terms, intuitionistic
%   lambda calculi are not closed under complementation.  We thus
%   develop a strict lambda calculus, where we can directly express
%   whether a function depends on its argument.
%   \vsk
%   \emph{Complementing clauses}. This can be seen as a negation normal form
%   procedure which is consistent with intuitionistic provability. It
%   entails finding a middle ground between the Closed World Assumption
%   usually associated with negation and the Open World Assumption
%   typical of logical frameworks. As this is in general not possible,
%   we restrict ourselves to a fragment in which clause complementation
%   is viable and that has proven to be expressive enough for the
%   practice of logical frameworks. The main technical idea is to
%   isolate a set of programs where static and dynamic clauses do not
%   overlap.
%   }

% \evensidemargin 0pt
% \oddsidemargin 0pt
% \maketitle
% \newpage
% \thispagestyle{empty}
% \vspace*{1in}
% \pagestyle{fancy}
% \pagenumbering{roman}
% \tableofcontents
% \listoffigures
% \cleardoublepage
% \pagenumbering{arabic}


\pagestyle{fancyplain}
 \include{cnn}


\bibliography{framework,strict}
\end{document}