\subsection{Other mechanised proof systems for relation algebras}

%There are other computer-based proof systems for relation algebras.

RALL \cite{RALL} is a theorem proving system for relation algebra,
based on Isabelle.
It uses the atomicity of relation algebras;
every relation algebra can be embedded in an atomic relation
algebra.
Although RALL provides automated proof search,
this feature is heavily dependent on 
%As stated in \cite{RALL}, \S5, the key idea to enable this is 
the atomization of the relation algebra.
It is still not clear to us
to what extent RALL is applicable to relation algebras which
are not themselves atomic.
RALL is built upon the \texttt{HOL} Isabelle theory, 
whereas our implementation of \dRA\ is built directly upon Isabelle's
metalogic.

RALF \cite{RALF} is a graphically oriented relation algebra formula
manipulation system and proof assistant.
It contains a large number of hard-coded transformation rules,
and the super-user can add others.
However the rules do not form a formal calculus.
%so it is not built upon any formal system.
Thus it does not demonstrate that the results it derives follow from 
any formalization of relation algebra. 
In fact it may be
seen as complementing a system such as that described in this paper since 
%it provides a powerful proof tool by using 
%the sorts of rules which can be derived from axioms by a system such as ours.
an interesting avenue for further work would be to obtain the 
transformation rules of RALF as \dRA\ derived rules,
giving a rigrorous basis to RALF and a graphical front-end to \dRA.