\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{cap1}

 \input{fo-not}


%           % cap strict

 \input{calculus}

 \input{honot}

 \input{hornelim}
\input{intro5}


 \input{logic}


 \input{context}

  \input{htermprf}

 \input{cc}

 \input{augment}
\input{excluproof}

 \input{exh}
\input{tensor}

%%%\input{local}
%%%\input{next}
\input{end}
\bibliography{not,framework,strict}



\end{document}