\section{Introduction}

Relation algebras are extensions of Boolean algebras;
whereas Boolean algebras model subsets of a given set,
relation algebras model binary relations on a given set.
Thus relation algebras have relational operations such as
composition and converse.
As each relation is itself a set (of pairs),
relation algebras also have the Boolean operations such as intersection 
(conjunction) and complement (negation).
Relation algebras form the basis of relational databases %\cite{db}
and of the specification and proof of correctness of programs.
%(\cite{wp},\cite{hoare}).
Recently, relation algebras and their extensions, Peirce algebras,
have also been shown to from the basis of description logics \cite{BBS}.
Just as Boolean algebras can be studied as a logical system
(classical propositional logic), relation algebras can also
be studied in a logical, rather than an algebraic, fashion.
In particular, relation algebras can be formulated using Display
Logic \cite{dRA}, and in several other ways \cite{Mad}.

Display Logic \cite{Bel} is a syntactic proof system for non-classical logic,
based on the Gentzen sequent calculus \cite{Gallier}.
%It can be applied to give syntactic proof systems for various logics.
Its advantages include a generic cut-elimination theorem, which 
applies whenever the rules for the display calculus satisfy certain conditions.
It is a significant general logical formalism, applicable to many logics;
%the implementation of one display calculus may be generalized to many others.
its mechanisation is therefore an important challenge for automated reasoning.

\comment{
Isabelle is an automated proof assistant \cite{Ref}.
It is written in ML, and the user interacts with it by issuing further ML
commands; this permits programming complex arrangements of
proof steps in ML.
The capabilities built in include higher-order unification and 
term rewriting.
Isabelle permits the user to define his/her own logic in which to perform
proofs, although in practice most users would build on one of the
systems of logic supplied \cite{OL}.
}

In this paper we describe an implementation of
\dRA\ \cite{dRA}, a display logic formulation of 
relation algebras, using the Isabelle theorem prover.
In this implementation the rules of \dRA\ form the axioms
of an Isabelle object logic -- 
\dRA\ is not built upon one of the standard Isabelle object logics 
(as is the case, for example, with RALL \cite{RALL}).
The ease with which this display calculus
can be implemented in Isabelle highlights
the generality of both Isabelle and Display Logic.
We demonstrate how Isabelle can be used to show the relationship 
between \dRA\ and two other formalizations of relation algebras.

\input{opf}