%%
%% Template abstract.tex
%%

\chapter*{Abstract}
\label{cha:abstract}
\addcontentsline{toc}{chapter}{Abstract}


    This project involves implementing Display Logic,
and the Display Logic system for relation algebras, in Isabelle, and
looking at the relationship between this and other proof systems for relation
algebras. %This seminar is an interim account of progress in the project.

We give
a description of the implementation of the Display Logic system
for relation algebras in Isabelle,
various tactics and derived rules developed for making proof easier,
and example theorems proved using Isabelle.

We consider an equational theory for proofs in relation algebra, and show
how its inferences can be justified in the Display Logic system.

We consider a sequent calculus based on point variables, and show that sequents
and proofs in that system can be translated to sequents and proofs in the
Display Logic system.

Finally, we describe the implementation in ML of functions to represent
and manipulate Isabelle proofs, 
and to implement the cut-elimination procedure of
Display Logic.


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