\section{Conclusion and Further Work}

We have formulated the Display Calculus for Relation Algebra, \dRA,
in Isabelle/HOL.
This formulation is a ``deep embedding'' which allows us to model,
and reason about, derivations in the logic (rather than just
performing derivations, as in a shallow embedding).
We have proved, from the definitions, ``transitivity'' results
about the composition of proofs.
These are results which have been omitted -- due to their difficulty --
from another reported mechanized formalization of provability.

We have proved Belnap's cut-elimination theorem for Display Calculi
for the Display Calculus \dRA.
This has been a considerable effort, and could not have been achieved without
the complementary features (found in Isabelle) of the 
\begin{itemize}
\item extensive provision of powerful tactics, and
\item powerful programming language interface available to the user.
\end{itemize}

Belnap's theorem is expressed to apply to any Display Calculus 
satisfying his conditions. 
To prove his theorem in that form would require modelling
an arbitrary Display Calculus, with 
arbitrary sets of structural and logical connectives
(as is done by Gor\'e in \cite{gore-sld-igpl}), and of rules.
In a sense, this would require a ``deeper'' embedding still.
For, in our first implementation, 
we set up the specific connectives and rules of \dRA\ in Isabelle,
and used Isabelle proofs as the \dRA-derivations.
In the present implementation,
we again set up the specific connectives and rules of \dRA,
although we set up data structures to model arbitrary proofs.
To prove the generic Belnap theorem, we need to set up the necessary
structures to model arbitrary sets of connectives and rules.

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