\renewcommand\cfile{relwk.tex}


In this section we 
describe some of the other proof systems for relation algebra.

\subsection{RALL} \label{RALL}
Oheimb \& Gritzner \cite{RALL} have developed a proof system, 
called RALL\index{RALL}, for relation algebras, in Isabelle.
It is built on the Isabelle \texttt{HOL} set theory, 
and the \texttt{Lattice} theory 
which is built upon that.
The \texttt{Lattice} theory is stated to define the
class of complete atomic Boolean lattices; 
the RALL system makes heavy use of the atomicity of relation
algebras, and therefore applies directly only to atomic relation algebras.
It does this by converting an algebraic expression into a propositional one,
by regarding an element as the union of the atoms contained in it.
For example $x \subseteq y \cup z$ becomes
$\forall a:\mbox{atom. }$
\mbox{$a \subseteq x \to  a \subseteq y \vee a \subseteq z$.}

\subsection{Gordeev's rewriting system}
Gordeev \cite{Gor} has proposed a system of rules for rewriting equations
of the form $F = \top$, where $\top$ denotes the unique largest element.
%These are a mixture of some rules which may rewrite an arbitrary part of the 
%formula $F$, and others which may only be applied to the whole of $F$, or,
%when $F$ is a conjunction, to one of the conjuncts of $F$.
It is therefore a system which only allows for proving statements of the form
$F = \top$.
However it has been shown that every Boolean combination of equations in
relation algebra is equivalent to an equation of this form
(see \cite{Mad}, pp.~435--6, pp.~439--440).
In Chapter~\ref{ch:gord} we show how an equation provable in this system
is provable in \dRA.

\subsection{A point-variable sequent calculus} \label{intro-mad}

Maddux \cite{seqra} deals with relation algebras in terms of the relations
and, in a sense, of the elements of the underlying set $U$.
He gives a sequent calculus in which variables appear in 
the place of elements of $U$.
The sequent $R \vdash S$ of \dRA\ becomes 
$x[R]y \vdash x[S]y$ in this system.
Intuitively, this sequent can be taken to mean
%$\forall x,y \: ( x[R]y \Rightarrow x[S]y) $.
$\forall x,y \: ( (x,y) \in R \Rightarrow (x,y) \in S) $.

Since the $x,y,\ldots$ in this formulation stand for members of $U$, it
may be suspected that the system actually axiomatizes \emph{representable}
relation algebras (defined in \S\ref{ra-class})
rather than general relation algebras.
However, Maddux looks at $MA_n$, the class of
algebras satisfying the properties which can be proved from his sequent rules
using only $n$ variables $x,y,\ldots$.
He shows that $MA_4$ is the class of relation algebras, and that 
$MA_\omega$ (ie, the class of relation algebras satisfying
all properties which can be proved from his sequent rules using any number of
variables) is the class of representable relation algebras (\cite{seqra},
Thm.~6).

Note that proofs in this system may require the (cut) rule.
In \cite{seqra}, Maddux gives an example of a sequent which is provable in 
$MA_3$, but which cannot be proved in 
$MA_3$ without using the (cut) rule.
However it can be proved in $MA_4$ without using (cut).
This is discussed further in \S\ref{mad-cut}.

\subsection{RALF} 

Berghammer \& Hattensperger \cite{RALF}
have produced a relation algebra formula manipulation system
and proof checker, called RALF\index{RALF}.
The system is graphically oriented, and can
display pictorially the structure of expressions, and of proofs.
The inferences of the system include
\begin{itemize} \shrinklist{0.5}
\item[--] transformation rules, ie, term-rewriting with either
hard-coded or previously proved equivalences
\item[--] use of hard-coded inference rules
\end{itemize}

There are a large number of hard-coded inference rules, and
the super-user can add more.
The soundness of results proved by the system depends therefore on
the correctness of all the transformation rules and inference rules 
built into the system.

\renewcommand\cfile{}