In Chapter~\ref{ch:RA} we showed how we implemented the \dRA\ theory
for relation algebras in Isabelle.
Although a \dRA\ proof involved frequent and tedious use of the display
postulates, we provided 
a number of tactics and other functions to make this aspect
of constructing proofs easier.
We also provided tactics to search for certain patterns and replace
them wherever they are found, giving the power of a rewrite rule in a
term rewriting system.
Most of the rules for introducing logical connectives could be used in
this manner.
Certain other tactics and functions,
such as those which
transform between structural and logical forms of sequents,
have proved convenient in proofs on occasions.

Some useful derived rules were proved, for example those
showing how the unary operators distribute over the binary operators.
This gives virtually all we need for a decision procedure for
propositional calculus, and a tactic was written to complete this procedure.

We showed how the \dRA\ system can justify inferences in the (axiomatic)
theory of relation algebras.
This result appears as Theorem~6 of \cite{dRA},
but the published proof omits most of the detail.  
This gives an example of the value of an automated theorem prover,
which can confirm the details of proofs where these are too
voluminous to publish or even too tedious to check by hand.

Some important (and difficult) theorems from the literature were also
proved, for example some from \cite{CT}.
Other interesting theorems were discovered and proved, some of which
were needed in Chapter~\ref{ch:mad}.

In Chapter~\ref{ch:gord} we described an equational theory 
due to Gordeev for doing proofs in relation algebras,
and showed how its inferences can be justified in \dRA.

In \ch{mad} we described the sequent calculus system
of Maddux \cite{seqra},
\M, for relation algebras, and showed how its sequents and proofs 
correspond to sequents and proofs in \dRA.
We proved a result characterizing which sequents in \M\ can be translated into
\dRA; we did this by describing the pattern of relation variables and point
variables in the \M-sequent by a graph, 
and finding that whether or not an \M-sequent
can be translated into \dRA\ depends on the shape of the graph.

As a sequent in \M\ can often be translated to
any of several sequents in \dRA,
we showed that these several sequents are equivalent in \dRA.

The result relating proofs in the two systems was that
if an \M-sequent $\mathcal S$
can be translated into a \dRA-sequent $\mathcal S'$, 
then any \M-proof of $\mathcal S$
can be translated into a \dRA-proof of $\mathcal S'$,
provided that the \M-proof uses at most four point variables.
This required showing how such a proof in \M\ can be divided into
parts each of which could be turned into a part of a proof in \dRA.
%the sequent proved is one that can be translated into \dRA,
%As not all \M-sequents containing at most four point variables
%can be translated into \dRA,
%not all the intermediate stages of such a proof could be translated into \dRA,
%that is, not every individual step of the \M-proof could be converted into 
%a corresponding step of a proof in \dRA.
%Rather, a larger portion of the \M-proof had to be treated as a unit;
%we showed that we could always rearrange the \M-proof to get 
%these portions of a particular form, which
%conformed to a theorem that we had proved in Isabelle for \dRA.

This result provided a constructive proof of one direction of the result of
Maddux (\cite{seqra}, Thm.~6) that the class of relation algebras is
characterized by the \M-sequents provable using four variables.
The possibility of doing a similar translation in the reverse direction is
discussed in \ch{apfw}.

In \ch{cut} we described the procedure for eliminating any
occurrence of the cut rule from a proof in \dRA, and the
ML functions which perform this procedure on an Isabelle proof in \dRA.
This means that a user can construct a proof using cuts,
and obtain a cut-free version automatically.

\subsubsection{Isabelle and ML}

The work described in this thesis
showed the value of using a theorem prover, such as Isabelle,
which can be driven by a powerful programming language such as ML.
The search-and-replace tactics described in \S\ref{srtac},
which involved some complex ML programming,
were essential for proving a lot of the results described in this thesis.
The result \texttt{ml2}, \insrc{Mad.ML},
mentioned on \page{ml2},
was crucial to proving the main result of \ch{mad}.
Proving it in Isabelle required about a page of ML programming specifically
for proving that particular result; without this capability 
it may have been too difficult to prove.

ML is of course excellently suited to programming all the functions
described in \ch{cut}.