\renewcommand\cfile{ra.tex}

\section{Relation Algebras} \label{ra-intro}

\comment{
Relations are a primary concept in many areas of computer science.
For example,
a program or program specification
can be modelled by
a set of (\textit{pre},\textit{post}) pairs,
which is just a relation on the state space of the machine.
Relations are also fundamental in
knowledge representation (for example, in relational databases).
}

A \bfi{relation}
on a set $U$ is a set of ordered pairs $(a,b)$ of elements of $U$, 
ie a subset of $U \times U$.
Since a relation is itself a set 
(of ordered pairs),
the operations on relations
include the operations of Boolean algebras.
Other relational operations are 
(as defined in \cite{dRA})
\bfi{composition} 
$R \circ S = \{ (a,b) \;|\; \exists c.\; (a,c) \in R 
\textrm { and } (c,b) \in S \}$,
its \bfi{identity} $\{ (a,a) \;|\; a \in U \}$, and 
\bfi{converse} 
$\smile R = \{ (a,b) \;|\; (b,a) \in R \}$.

Relation algebras are an abstraction of the notion of
binary relations on a set $U$;
reference to the actual elements of the set is abstracted away, leaving
the relations themselves as the objects under consideration.
%Thus a relation algebra is a set (whose members are the relations),
%with a number of operations.
Chin \& Tarski \cite{CT} give a finite equational
axiomatization of relation algebras.
%that is, a finite set of equations that relation algebras must satisfy.
The following definition, equivalent to that in \cite{CT},
is taken from \cite{BBS} and \cite{dRA}.

A relation-type algebra 
$\mathcal R = \langle R, \lor, \land,
\neg, \bot, \top, \circ, \smile, \1 \rangle$
(ie, a free algebra on the set of variables $R$ with binary
operators $\lor$, $\land$ and  $\circ$, unary operators $\neg$ and $\smile$, 
and constants $\bot$, $\top$ and $\1$)
is a \bfi{relation algebra} if it satisfies the following axioms
for each $r,s,t \in R$

\begin{center}
\begin{tabular} {l@{\hspace{3mm}}l@{\hspace{8mm}}l@{\hspace{3mm}}l}
\label{RA1-8}
(RA1) & 
\multicolumn 3 l {
$(R, \lor, \land, \neg, \bot, \top) $ is a Boolean algebra }\\[0.5ex]
(RA2) & $r \circ (s \circ t) = (r \circ s) \circ t$ &
(RA3) & $r \circ \1 = r = \1 \circ r $ \\[0.5ex]
(RA4) & $\smile \smile r = r $ &
(RA5) & $(r \lor s) \circ t = (r \circ t) \lor (s \circ t)$ \\[0.5ex]
(RA6) & $\smile (r \lor s) = (\smile r) \lor (\smile s) $ &
(RA7) & $\smile (r \circ s) = (\smile s) \circ (\smile r) $ \\[0.5ex]
(RA8) & $\smile r \circ \neg (r \circ s) \leq \neg s$ & & 
\end{tabular}
\comment{
\begin{tabular}{l@{\hspace{15mm}}c}
\label{RA1-8}
(RA1) & $(R, \lor, \land, \neg, \bot, \top) $ is a Boolean algebra \\[0.7ex]
(RA2) & $r \circ (s \circ t) = (r \circ s) \circ t$ \\[0.7ex]
(RA3) & $r \circ \1 = r = \1 \circ r $ \\[0.7ex]
(RA4) & $\smile \smile r = r $ \\[0.7ex]
(RA5) & $(r \lor s) \circ t = (r \circ t) \lor (s \circ t)$ \\[0.7ex]
(RA6) & $\smile (r \lor s) = (\smile r) \lor (\smile s) $ \\[0.7ex]
(RA7) & $\smile (r \circ s) = (\smile s) \circ (\smile r) $ \\[0.7ex]
(RA8) & $\smile r \circ \neg (r \circ s) \leq \neg s$  
\end{tabular}
}
\end{center}

Further operators can be defined:
$A \leq B$, as used in (RA8), means \mbox{$(A \land B) = A$.}
Duals of $\1$ and $\circ$ are defined:
\0 is $\neg \1$, and $A + B$ is $\neg(\neg A \circ \neg B)$.
We call this theory of relation algebras \RA\index{RA@\textbf{RA}|textbf}.
A \emph{proper} relation algebra 
consists of a set of relations on a set;
note that not all relation algebras 
are isomorphic to a proper relation algebra (\cite{Mad}, p.444-5).

\section{Relation Algebras in Display Logic}

A number of different logical systems can be formulated using the
method, or style, of Display Logic \cite{Bel}.
These include several normal modal logics \cite{Wansing},
and intuitionistic logic \cite{ILR}.
Display Logic resembles the Gentzen sequent calculus \textbf{LK},
but with significant differences.
For example, the rules for introducing the connective `$\lor$' 
(on the right) in \textbf{LK} and Display Logic are
\label{|-v}
$$\frac {\Gamma \vdash \Delta, P, Q}
{\Gamma \vdash \Delta, P \lor Q}(\mbox{\textbf{LK}-}\vdash \lor )
\qquad \textrm{ and } \qquad 
\frac {X \vdash P , Q}
{ X \vdash P \lor Q}(\mbox{DL-}\vdash \lor )
$$ 
Whereas, in \textbf{LK},
$\Gamma$ and $\Delta$ denote comma-separated lists of formulae,
in Display Logic, $X$ denotes a Display Logic structure,
which can involve several \emph{structural} operators (one of which is `,').
(See \cite{dRA} or \cite{thesis}
for a full explanation of \emph{structures} and \emph{formulae}).
In Display Logic, unlike in \textbf{LK},
the introduced formula (here, $P \lor Q$) stands by itself
on one side of the turnstile.
However there are also rules (the ``display postulates'')% described below)
which effectively allow moving formulae from one side to the other.
In \cite{dRA} there is a Display Logic formulation of relation algebras,
called \dRA\
whose structural operators are `,' `;' `$*$' `$\bullet$' `$I$' `$E$' .
As in \textbf{LK}, the use of `,' to stand for either `$\land$' or `$\lor$'
(depending on the position) reflects the duality between them.
Likewise in \dRA\ `;' stands for either
`$\circ$' or `$+$', whose duality was noted above.
Each structural operator stands for one, or two (depending on the position),
formula operators.
Thus $I$ stands for truth or falsity, $E$ for the identity relation or its
complement, $*$ for Boolean negation and $\bullet$ for the relational converse.
The rules of \dRA\ are sound and complete
with respect to the equational axiomatization of Chin \& Tarski \cite{dRA}.

\comment{
In Display Logic,
statements are in the form of sequents,
built up of structures and formulae.
A \bfi{formula} is either a propositional variable,
or a combination of formulae formed using the formula operators, 
which are shown in the first and third rows of the table below,
and which have the arities shown in the fourth row of the table.
Conventionally we use $A,B,C,D$ as variables denoting formulae.
A \bfi{structure} is defined as a formula, %or a structure variable,
or a combination of structures formed using the structure operators.
In \dRA, 
the structure operators are `$I$' and `$E$' (constant),
`$*$' and `$\bullet$' (unary), and `,' and `;' (binary).
Conventionally we use $X,Y,Z,W,\ldots$ as variables denoting structures.
A \bfi{sequent} is of the form $X \vdash Y$, where $X$ and $Y$ are 
structures.

\begin{center}
\begin{tabular}{l@{\qquad\qquad}ccc@{\qquad\qquad}ccc}
 & \multicolumn 3 {c@{\qquad\qquad}} {Boolean} &
\multicolumn 3 {c} {Relational} \\
Formula & $\top$ & $\lnot$ & $\land$ & $\1$ & $\smile$ & $\circ$ \\
Structure & $I$ & $*$ & $,$ & $E$ & $\bullet$ & $;$ \\
Formula & $\bot$ & $\lnot$ & $\lor$ & $\0$ & $\smile$ & $+$ \\
Arity & 0 & 1 & 2 & 0 & 1 & 2 
\end{tabular}
\end{center}

Thus we have the following BNF-style definition, where 
$\mathcal S$, $\mathcal F$ and $p$ denote 
a structure, a formula and a primitive proposition respectively.
\begin{eqnarray*}
\mathcal F & ::= & p \:|\: 
  \mathcal F \land \mathcal F \:|\: \mathcal F \lor \mathcal F \:|\: 
  \mathcal F \circ \mathcal F \:|\: \mathcal F + \mathcal F \:|\: 
  \lnot \mathcal F \:|\: \smile \mathcal F \:|\: 
  \top \:|\: \bot \:|\: \1 \:|\: \0 \\
\mathcal S & ::= & \mathcal F \:|\: 
  \mathcal S , \mathcal S \:|\: \mathcal S ; \mathcal S \:|\: 
  * \mathcal S \:|\: \bullet \mathcal S \:|\: I \:|\: E 
\end{eqnarray*}

A structure in a sequent is in an 
\bfi{antecedent} position if
it is on the left-hand side of the turnstile and 
within the scope of an even number (including zero) of `$*$' operators,
or on the right-hand side of the turnstile and 
within the scope of an odd number of `$*$' operators;
otherwise it is in a \bfi{succedent} position.
A structure operator, when in an antecedent (succedent) position,
stands for the formula operator in the first (third) row of the table.
For example, the structural operator `,' appearing in an
antecedent position stands for the formula operator `$\land$'.

The rules consist of the following classes.
Note that the name shown on the right of a rule is that used in the
Isabelle implementation; a dagger (\dag) indicates that a rule,
although given in \cite{dRA} as a separate rule, is in fact derivable
from the remaining rules.
\begin{description}
\item[identity, cut] are two rules which are common to all display logics.
Note that in the identity rule, $p$ stands for a primitive proposition,
not an arbitrary formula, 
and in the cut rule, $A$ must be a formula (not an arbitrary structure).
They are
\begin{center}
\label{id}
(id) $p \vdash p$ %(\verb:idf:)
\hspace{20mm}
(cut) $\displaystyle
\frac{X \vdash A \qquad A \vdash Y} {X \vdash Y}$(\ttdef{cut})
\end{center}

\item[display postulates] \index{display postulates|textbf}
These are sufficient to \bfi{display}
any chosen structure in a sequent, ie, 
to transform the sequent so that the chosen structure appears by itself on
one side or the other of the turnstile.
As the display postulates never move a structure between an antecedent position
and a succedent position, there is no choice as to which side
this will be.
These rules are all bi-directional, which is indicated by the double line.
They are shown on page~?? of \cite{RA}.
(These and the rules described below are also reproduced in \cite{thesis}).
We often use ``(dp)'' in a proof to indicate the use of one or more
display postulates.
\item[basic structural rules] \index{basic structural rules|textbf}
These are the rules, other than the display postulates,
which involve only structural variables and operators.
They are shown in Figure~2 of \cite{RA}.
\item[logical introduction rules] \index{logical introduction rules|textbf}
These rules allow introduction of the logical, or formula, operators.
They are shown in Figure~2 of \cite{RA}.
\end{description}
}

Like \textbf{LK},
Display Logic is suited to backwards search for proof of a sequent,
provided that a sequent is provable without using the cut rule.
In terms of backwards proof, the logical introduction rules
eliminate the logical operators and replace them with corresponding
structural operators.
The cut-elimination theorem of \textbf{LK} 
applies in all Display Logics,
provided that the rules satisfy certain conditions,
which are relatively easily checked (\cite{Bel}).
Indeed the 
procedure for eliminating cuts from a proof has been automated, see
\S\ref{cutelim}.

Unlike \textbf{LK}, Display Logic has bi-directional
rules, the display postulates.
Therefore any proof search technique must avoid
a naive application of these \emph{ad infinitum}.
Although 
this is a difficulty in developing a purely automatic proof search technique,
this is not insurmountable, and requires further work.
%undoubtedly, though, there is the potential to implement tactics
%for automatic proof search.
%scope for further work in devising more largely
%automatic techniques than those described here.
%This has not been investigated in detail yet.
For example, the techniques described below are sufficient to obtain
a decision procedure for the classical propositional calculus (see
\cite{thesis}, \S2.6.1 for details).
In any case 
it is known that the theory of relation algebras is undecidable
(see \cite{Mad}, p.432).

Note that although 
Display Logic is suited to backwards proof,
we will always write a proof tree, or a rule, with the premises at the top
and the conclusion at the bottom
(except that a double line in a rule means that it is bi-directional),
and we will refer to the order of steps in a proof as though it is done in a
forward direction, from premises to conclusion.
%Thus, for example, we will talk of the monotonicity rules
%($M \vdash$) and ($\vdash M $) as \emph{adding} a structure to a sequent.
As an alternative to writing a rule with one premise $\mathcal P$ and a
conclusion $\mathcal C$ separated by a horizontal line, we often write 
$\mathcal P \Longrightarrow \mathcal C$, and 
for a bi-directional rule we often write $\mathcal P \iff \mathcal C$.
For a full explanation of Display Logic and \dRA\ see \cite{dRA}.

\section{Isabelle}

Isabelle is an interactive computer-based proof system,
described in \cite{Ref}.
Its capabilities include higher-order unification and 
term rewriting.
It is written in Standard ML;
when it is running, the user can interact with it by
entering further ML commands, and can program complex proof sequences in ML.
Isabelle provides a number of basic proof steps for
backwards proof (\emph{tactics}\index{tactic|textbf}), as well as 
\emph{tacticals}\index{tactical|textbf}
for combining these.
%Isabelle automatically keeps track of the subgoals generated by this backward
%search procedure and the user can choose to work on any subgoal.
%The user can also write complex proof tactics in ML;
%many complex tactics and tacticals are supplied with
%Isabelle or its standard object logics.
Isabelle also supports forward proof.

It has a simple meta-logic, an intuitionistic higher-order logic.
\comment{
It has the unusual feature that it can be used with the user's own choice of
logical system, for very little is built in.
The built-in logic is described as intuitionistic higher-order logic,
with three operators producing propositions: 
\texttt{==>} (implication, or deducibility),
\texttt{==} (equality, or substitutibility), and
\texttt{!!} (universal quantification).
These operators have only the properties necessary to support their
intended meanings.
For example, since
\mbox{\texttt{[| P; Q |]~==>~R}}
means that \texttt R can be deduced from \texttt P and \texttt Q,
it necessarily follows that
\mbox{\texttt{[|~P~==>~Q;~P~|] ==> Q},} and that
{\par\noindent\centering
\texttt{([| P; Q |] ==> R) ==> ([| Q; P |] ==> R)}.
\par\noindent}
Likewise, since 
\texttt{P == Q}
means that \texttt P can be replaced by \texttt Q, or vice versa,
\texttt{==} is reflexive, symmetric and transitive.
}
The user then has to augment this by defining an object-level logic,
though normally one would use one of
several which are packaged with the Isabelle distribution \cite{OL}.
\comment{
Anything that can be proved using the built-in logic
from the ``axioms'' 
%asserted by the user in a ``theory file'' 
of the chosen object logic is a theorem,
of ML type \ttdef{thm}.
Isabelle uses the strong typing of ML to prevent the user from `proving'
results other than by the inference steps permitted;
only these steps can produce something of Isabelle type \texttt{thm}.
Naturally the primitive inference steps built in can be combined, both in
the more powerful functions provided in Isabelle, or by the user
programming more complex proof functions in ML.
}

Thus a logical system such as 
\dRA\ can be implemented in Isabelle so that the only
proof rules available are those of \dRA.
This contrasts with an implementation in other proof systems, where
the \dRA\ rules would be added to the rules of the logic on which 
that proof system was based.
(Of course, systems can be implemented in this way in Isabelle too;
thus RALL \cite{RALL}
is implemented on top of the \texttt{HOL} Isabelle theory).

% The user asserts a set of `axioms' in a `theory file', where 
% the syntax of the object-logic is also specified.
% Isabelle treats these axioms as theorems (of type \texttt{thm}).

\label{isathm}
Isabelle theorems (including the axioms of the theory)
may but need not involve Isabelle's metalogical operators.
%for example, a result of the form \texttt{([| P; Q |] ==> R)}.
In the Isabelle implementation of Display Logic, an Isabelle theorem
(of type \texttt{thm})
may be either a simple sequent of \dRA, 
or a sequent \emph{rule}.
Whereas a sequent of \dRA\ becomes an Isabelle theorem of the form $X \vdash Y$,
a sequent rule becomes an Isabelle theorem containing also 
the operators \texttt{==>} (implication) or \texttt{==} (equality).
% For example, the (cut) rule (shown on \page{id}) appears as
% {\par\noindent\centering
% \texttt{"[| \$?X |- ?A; ?A |- \$?Y |] ==> \$?X |- \$?Y"}
% \par\noindent}
For example, the ($\vdash \lor $) rule (shown in \S\ref{|-v}) appears as
$$\texttt{"\$?X |- ?A, ?B ==> \$?X |- ?A v ?B"}$$
in Isabelle. 
(The `\verb:?:' denotes a variable which can be instantiated,
and the `\verb:$:' denotes a structural variable or constant.)
The variant $A \vdash A$ of the (id) rule (see \S\ref{otm})
appears as \texttt{"?A |- ?A"}.
The bi-directional \texttt{dcp} rule, shown in \fig{sdr},
appears as \texttt{"\$?X |- \$?Y == * \$?Y |- * \$?X"}.

%An Isabelle theorem whose use of the metalogic is
%even more complex is \texttt{G910meth}, discussed in \S\ref{gord}.

Isabelle can be used to show the equivalence of \dRA\ to the various
other systems; in most cases this serves only to confirm proofs appearing in the
literature, and in many cases it can only provide proofs of 
the various inductive steps of a proof that requires structural induction.
However it shows that \dRA\ is effective for proving the 
axioms or rules of the other systems.

\renewcommand\cfile{}