% We described an implementation of the \dRA\ theory
% for relation algebras in Isabelle.
% This is the first implementation of any Display Logic system, 
% and generalizes easily to other Display Logic systems.
We described an implementation, in Isabelle, of the display
calculus \dRA\ for relation algebras. This is the first
implementation of any display calculus. We intend to generalise it to
other display calculi in future work.
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, but not all, 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.
There is scope for further work to devise more 
automatic techniques than those described here.

The use of display postulates to ``display'' a subterm resembles the use of
window inference \cite{wi},\cite{jgwi} to ``focus'' upon a subterm.
Further work is needed to connect these two modes of reasoning.

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.
Although this result appears as Theorem~6 of \cite{dRA},
the published proof omits most of the detail.
The detail is provided in the Isabelle proofs,
giving an example of the value of a mechanized theorem prover 
to confirm the details of proofs which 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 for the work outlined in \S\ref{mad}.

In \S\ref{gord} we described an equational theory 
due to Gordeev for relation algebras,
and showed how its inferences can be justified in \dRA.
As mentioned there, we obtained a corresponding result for 
the sequent calculus system of Maddux.
This showed how Isabelle could be used to demonstrate the 
relationship between different logical systems for relation algebra.

Theorems 3.6 and 3.8 of \cite{BBS} show that Peirce algebras
can be embedded inside relation algebras in various ways.
The authors also show that Peirce algebras form the basis of most of the common
Knowledge Representation languages like \textsc{KL-ONE} \cite{BrS}.
Minor modifications of our system should give mechanised proof systems for
these logics.

%\input{opf}