\documentclass[11pt,a4paper]{article}

\usepackage{isabelle,isabellesym}
\usepackage{amssymb,ragged2e}
\usepackage{pdfsetup}

\isabellestyle{it}
\renewenvironment{isamarkuptext}{\par\isastyletext\begin{isapar}\justifying\color{blue}}{\end{isapar}}
\renewcommand\labelitemi{$*$}
\urlstyle{rm}

\begin{document}

\title{Relational Forests}
\author{Walter Guttmann}
\maketitle

\begin{abstract}
  We study second-order formalisations of graph properties expressed as first-order formulas in relation algebras extended with a Kleene star.
  The formulas quantify over relations while still avoiding quantification over elements of the base set.
  We formalise the property of undirected graphs being acyclic this way.
  This involves a study of various kinds of orientation of graphs.
  We also verify basic algorithms to constructively prove several second-order properties.
\end{abstract}

\tableofcontents

\section{Overview}

The theories described in this document study second-order specifications of graph properties expressed as first-order formulas in Stone-Kleene relation algebras.
Of particular interest are undirected forests and their orientations, developed in Section 2.
We also verify the correctness of a number of basic graph algorithms, which we use in constructive proofs of graph properties in Section 3.

The theories formally verify results in \cite{Guttmann2021b}; results from this paper are annotated with the corresponding theorem numbers.
See the paper for further details and related work.

\begin{flushleft}
\input{session}
\end{flushleft}

\bibliographystyle{abbrv}
\bibliography{root}

\end{document}

