\documentclass[11pt]{book}
\usepackage{latexsym}
\usepackage{cdsty}
\usepackage{amssymb}
\usepackage{fancyheadings}
%\usepackage{showkeys}
%\usepackage{graphics}
% \usepackage{functions}
% \usepackage{epic}
% \usepackage{eepic}
% \usepackage{eepicemu}
% \usepackage{color}
% \usepackage{makeidx}
% \usepackage{cmu-titlepage}
% % \usepackage[dvips]{graphics}

\sloppy
\textheight22cm
\textwidth16cm
\topmargin-0.5cm
\oddsidemargin0cm
\evensidemargin0cm

\lhead[\rm\thepage]{\leftmark}
\chead{}
\rhead[\rightmark]{\rm\thepage}
\cfoot{\makebox[\textwidth]{\hrulefill\ {\tiny Draft --- Do Not Distribute}  \hrulefill\ {\tiny \today}\ }}
%\cfoot{}
\pagestyle{fancy}

% %\includeonly{introduction}
% %\includeonly{meta-logical-frameworks,mlf,app-rules}
% %\includeonly{logical-frameworks}
% %\includeonly{automated-deduction}
% %\includeonly{meta-logical-frameworks}
% %\includeonly{mlf}
% %\includeonly{operational-semantics,app-rules,app-proofs}
% %\includeonly{operational-semantics}
% %\includeonly{meta-theory}
% %\includeonly{meta-theory,app-proofs}
% %\includeonly{app-rules}
% %\includeonly{app-proofs}
% %\includeonly{abstract,introduction}
% %\includeonly{twelf}
% %\includeonly{conclusion}


 \begin{document}
% %\input{def.tex} \input{abbrev.tex} \input{diagmac.tex}

 \title{Automating the Meta Theory of Deductive Systems}
 \bibliographystyle{alpha}
 \author{Carsten Sch\"urmann}
 \date{\today}
 
 \keywords{ meta logic, LF, induction, regular world assumption,
   realizability, higher-order abstract syntax, Twelf}
 \trnumber{CMU-CS-00-146}
 \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 \\
     Robert Harper \\
     Peter Lee \\
     Dana Scott \\
     Natarajan Shankar, SRI International
 \end{center}}

 \copyrightnotice{Copyright \copyright\  2000 Carsten Sch\"urmann}

% \cmuabstract{This thesis describes the design of a meta-logical
%   framework that supports the representation and verification of
%   deductive systems, its implementation as an automated theorem
%   prover, and experimental results related to the areas of programming
%   languages, type theory, and logics.}
  
\evensidemargin 0pt
\oddsidemargin 0pt
\maketitle{}
\newpage
\thispagestyle{empty}
\vspace*{1in}
\pagestyle{fancy}
\pagenumbering{roman}
\tableofcontents
\listoffigures
\cleardoublepage
\pagenumbering{arabic}
%\input{logic}

%\tableofcontents


%\include{abstract}
\include{introduction}          % 15 pages

\part{Background}               % 50 pages
  \include{logical-frameworks}  % 40 pages
  \include{automated-deduction} % 10 pages

\part{Design of a Meta-Logical Framework}
                                % 60 pages
  \include{meta-logical-frameworks}
                                
  \include{mlf}
  \include{operational-semantics}
  \include{meta-theory}
\part{Implementation}
  \include{twelf}
  \include{conclusion}

\appendix

\include{app-rules}
\include{app-proofs}

\bibliographystyle{alpha}
\bibliography{thesis,lfs-new,ergobib,pfenning,fp,carsten,pvs-bib,proposal,linear}

\end{document}



%%% Local Variables: 
%%% mode: latex
%%% TeX-master: "thesis"
%%% End: 




