%%
%% Template thesis.tex
%%
\documentclass[a4paper,12pt]{book}
%\usepackage{anuthesis}
%\usepackage[cm]{anuthesis}
%\usepackage[times]{anuthesis}
\usepackage[palatino]{anuthesis}
%\usepackage{graphicx}
\usepackage{thesis}
\usepackage{makeidx}
\usepackage{acmnew-xref}

\usepackage{latexsym}
\usepackage{amssymb}
\usepackage{exptrees}

\renewcommand{\today}{\number\day\ 
  \ifcase\month\or
  January\or February\or March\or April\or May\or June\or
  July\or August\or September\or October\or November\or December\fi
  \ \number\year}

\setlength \parskip {1.0ex}
\setcounter{secnumdepth}2
\setcounter{tocdepth}2

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% Preamble
\title{Mechanised Proof Systems for Relation Algebras}
\author{Jeremy E. Dawson}

\date{\today}

\newcommand\cfile{}
\renewcommand{\thepage}{\roman{page}}
\newcommand\shrinklist[1]{
\setlength\parskip{#1\parskip}
\setlength\itemsep{#1\itemsep}
\setlength\itemindent{#1\itemindent}
\setlength\topsep{#1\topsep}
}

\newcommand\comment[1]{} 
\newcommand\invrule[2]{ 
% for use in non-math mode, args interpreted in math mode
  \begin{tabular}{@{}c@{}}
  $ #1 $ \\ \hline \hline $ #2 $
  \end{tabular}}
\newcommand\slrule[2]{ % similar to \frac, except
% for use in non-math mode, args interpreted in math mode
  \begin{tabular}{@{}c@{}}
  $ #1 $ \\ \hline $ #2 $
  \end{tabular}}

\newcommand\proof{\noindent\textbf{Proof.}}
\newcommand\src[1]{source file \texttt{#1}}
\newcommand\apsrc[1]{Appendix \ref{app:code}}
%\newcommand\seesrc[1]{(see source file \texttt{#1}, \apsrc{#1})}
\newcommand\seesrc[1]{(see source file \texttt{#1})}
%\newcommand\insrc[1]{in source file \texttt{#1} (see \apsrc{#1})}
\newcommand\insrc[1]{in source file \texttt{#1}}
\newcommand\page[1]{page~\pageref{#1}}
\newcommand\fig[1]{Figure~\ref{fig:#1}}
\newcommand\ch[1]{Chapter~\ref{ch:#1}}
\newcommand\tbl[1]{Table~\ref{tbl:#1}}
\newcommand\thrm[1]{Theorem~\ref{thrm:#1}}
\newcommand\lem[1]{Lemma~\ref{lem:#1}}
\newcommand\ttl[1]{\tti{#1}\label{#1}}
\newcommand\ttdl[1]{\texttt{#1}\tti{#1}\label{#1}}
\newcommand\ttdef[1]{\texttt{#1}\tti{#1}}
\newcommand\tti[1]{\index{#1@\texttt{#1}}}
\newcommand\bfi[1]{\textbf{#1}\index{#1|textbf}}
\newcommand\dRA{{\boldmath $\delta$}\textbf{RA}}
\newcommand\dKt{{\boldmath $\delta$}\textbf{Kt}}
\newcommand\NRA{\textbf{NRA}}
\newcommand\RA{\textbf{RA}}
%\newcommand\M{$\mathcal M$}
\newcommand\M{\ensuremath{\mathcal M}}
\newcommand\Mp{$\mathcal M'$}
\newcommand\up[1]{\vspace{-#1ex}} 
\newcommand\vpf{\vspace{-3ex}} % to reduce space before proof tree
\newcommand\1{\textbf 1}
\newcommand\0{\textbf 0}

\newtheorem{thm}{Theorem}[chapter]
\newtheorem{lemma}[thm]{Lemma}
\newtheorem{defn}[thm]{Definition}
\newtheorem{cor}{Corollary}[thm]
\renewcommand\thecor{\thethm(\arabic{cor})}

\makeindex
\begin{document}

{\list{}{}} % to reduce list spacing and indentation
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% Title page
\pagestyle{empty}
\thispagestyle{empty}
\input titlepage

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% Here begin the preliminaries
\input frontmatter

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% Dedication (optional)
%\cleardoublepage
%\pagestyle{empty}
%\input dedication

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% Acknowledgements (optional!)
\cleardoublepage
\pagestyle{empty}
\input ack

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% Abstract
\cleardoublepage
\pagestyle{headings}
\input abstract

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% Table of contents

\cleardoublepage
\pagestyle{headings}
\markboth{Contents}{Contents}
\tableofcontents

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\pagestyle{headings}
\sloppy 

%% Here begins the main text
\mainmatter

\chapter{Introduction and Literature Survey}
\input{intro}
\section{Proof Systems for Relation Algebras}
\input{relwk}

\chapter{Relation Algebras} \label{ch:RA}
\input{ra}
\input{raisa}

\section{Results from the \dRA\ implementation}
\input{thms}

\chapter{Gordeev's term rewriting system for \RA} \label{ch:gord}
\input{gord}
\comment{
} %endcomment

\chapter{A point-variable sequent calculus} \label{ch:mad}
\section{Introduction}
\input{madint} \label{madint}

\section{An equivalent calculus}
\input{mad} \label{mad}

\section{Translating from \M\ to \dRA}
\input{trans} \label{trans}
\subsection{Characterizing when \M-sequents can be translated}
\input{trcond}
\subsection{The equivalence of alternative translations}
\input{eqtr}

\section{Mimicking an \M-proof in \dRA}
\input{mimlems}
\input{mim}

\chapter{Automating the Cut-Elimination procedure} \label{ch:cut}
\input{cut}

\chapter{Applications and Further Work} \label{ch:apfw}
\input{appl}

\chapter{Conclusion}
\input{concl}
\comment{
} %endcomment
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Here begins the end matter

\input app

\backmatter

\bibliographystyle{acmnew-xref}
\bibliography{thesis}

\printindex

\end{document}

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