\documentclass[11pt,a4paper]{article}
\usepackage{isabelle,isabellesym}

% this should be the last package used
\usepackage{pdfsetup}

% urls in roman style, theory text in math-similar italics
\urlstyle{rm}
\isabellestyle{it}

\begin{document}

\title{Undirected Graph Theory}
\author{Chelsea Edmonds}
\maketitle

\begin{abstract}
  This entry presents a general library for undirected graph theory - enabling reasoning on simple graphs and undirected graphs with loops. It primarily builds off Noschinski's basic ugraph definition \cite{noschinski_2012}, however generalises it in a number of ways and significantly expands on the range of basic graph theory definitions formalised. Notably, this library removes the constraint of vertices being a type synonym with the natural numbers which causes issues in more complex mathematical reasoning using graphs, such as the Balog Szemeredi Gowers theorem which this library is used for. Secondly this library also presents a locale-centric approach, enabling more concise, flexible, and reusable modelling of different types of graphs. Using this approach enables easy links to be made with more expansive formalisations of other combinatorial structures, such as incidence systems, as well as various types of formal representations of graphs. Further inspiration is also taken from Noschinski's \cite{noschinski_2015} Directed Graph library for some proofs and definitions on walks, paths and cycles, however these are much simplified using the set based representation of graphs, and also extended on in this formalisation.
\end{abstract}

\tableofcontents

\subsection*{Acknowledgements}
Chelsea Edmonds is jointly funded by the Cambridge Trust (Cambridge Australia Scholarship)
and a Cambridge Department of Computer Science and Technology Premium Research Studentship.
The ALEXANDRIA project is funded by the European Research Council, Advanced Grant GA 742178.
\newpage

% include generated text of all theories
\input{session}

\bibliographystyle{abbrv}
\bibliography{root}

\end{document}
