\renewcommand\cfile{ra.tex}

\section{Introduction} \label{ra-intro}

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{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}.

\section{Classes of Relation Algebras} \label{ra-class}

In this section we refer in more detail
to some of the theoretical background of relation algebras.

There are a number of ways to define relation algebras abstractly.
Several similar definitions are described in \cite{Mad}, pp.~441--2,
of which that of Chin \& Tarski \cite{CT}
is used in \cite{dRA} (see \page{RA1-8}).
Of the other axiomatic definitions, some have included
additional axioms ensuring that the algebra is non-trivial (ie, has more than
one element) and that it is 
\textbf{simple}\index{relation algebra!simple|textbf}
ie, it has no non-trivial congruence relations (\cite{Mad}, p.~441), 
or, equivalently,
it has no non-trivial 
\textbf{ideal elements}\index{relation algebra!ideal element|textbf}
(see \cite{CT}, p.~362).
Otherwise these definitions are equivalent.

Naturally, one example of a relation algebra 
is $\mathcal R (U)$, the set of all relations on a set $U$.
Other examples would be subsets of
$\mathcal R (U)$ that are closed under all the operations.
There are also relation algebras on $U$ in which the largest relation $\top$
is not $U \times U$, but a proper subset of it.
(In these relation algebras, 
complements are taken with respect to $\top$.)
In these cases, however, $\top$ must be an equivalence relation on $U$.
A relation algebra 
consisting of a set of relations on a set $U$ is called 
a \textbf{proper}\index{relation algebra!proper|textbf} relation algebra
(\cite{CT}, p.~345; \cite{Mad}, p.~444).

The definitions of relation algebra
do not capture all of the characteristics of 
a proper relation algebra.
A relation algebra is called
\textbf{representable}\index{relation algebra!representable|textbf}
if it is isomorphic to a proper relation algebra.
%in addition to satisfying Tarski's axioms (RA1) to (RA8),
Not all relation algebras are representable; however, to characterize
the representable relation algebras among all relation algebras requires an
infinite set of conditions (see \cite{Mad}, p.~445).

An \textbf{atom}\index{atom|textbf} in a Boolean algebra is 
an element that is not the union of smaller elements
(intuitively, like a singleton set);
a Boolean algebra is 
\textbf{atomic}\index{relation algebra!atomic|textbf}
if every element is a union of atoms.
Oheimb \& Gritzner (\cite{RALL}, Theorem 2)
appear to say that every relation algebra is atomic
(which is not the case, see Theorem~\ref{notatom});
however a relation algebra can be \emph{embedded in} an atomic relation algebra.
Maddux discusses how the structure of a \emph{finite} relation algebra is
determined by the atoms and their compositions and converses 
(\cite{Mad}, pp.~445--448).

\section{Relation Algebras in Display Logic}

Display Logic is a Gentzen-type sequent calculus.
A Gentzen sequent is of the form (for example)
$P,Q \vdash R,S$
where $P,Q, R,S$ are propositions;
it means ``($P$~and~$Q$) entails ($R$ or $S$)''.
Each of $P,Q, R,S$ can represent a formula such as $A \& B$.
An inference rule consists of a \bfi{conclusion} and (usually)
one or more \bfi{premises}, the premises being written above a horizontal line.
It means that when instances of the premise sequents have been inferred
then the corresponding instance of the conclusion may also be inferred.
The sequent calculus rules are primarily ``introduction rules'',
where the conclusion contains a connective not present in the premise(s).
For example, the rules for introducing the connective ``$\land$'' into the
left and right sides of a sequent are
$$ \frac {\Gamma, P, Q \vdash \Delta} {\Gamma, P \land Q \vdash \Delta}
(\land \vdash )\qquad \textrm{ and } \qquad 
\frac {\Gamma \vdash \Delta, P \qquad \Gamma \vdash \Delta, Q}
{\Gamma \vdash \Delta, P \land Q}(\land \vdash )$$ 
where $\Gamma$ and $\Delta$ denote comma-separated lists of formulae.
See Gallier \cite{Gallier} for a full description.

Thus, if a proof could be done using only these rules,
and it were done backwards from the intended goal,
there would be a very restricted choice of rules to be applied at each step.
This is a great advantage in automated proof.
In fact, if a sequent can be
proved, without any premises, then it can be proved only using rules
of this sort.
On the other hand, one may wish to prove a sequent from premises,
eg, a result of the form
$$ \frac {\Gamma' \vdash \Delta'} {\Gamma \vdash \Delta} $$
(Such a result may be wanted as a lemma for proving a further result).
To prove such a result
may require the cut rule, ie
$$ \frac {\Gamma \vdash \Delta',A \qquad \Gamma',A \vdash \Delta} 
{\Gamma,\Gamma' \vdash \Delta',\Delta} $$
In doing backwards proof, using the cut rule involves guessing
the arbitrary formula $A$, which is a disadvantage in doing automated proof.

Display Logic works slightly differently from this; the formula being
introduced will be by itself on its side of the turnstile.
That is, in the rule ($\land \vdash $) above, $\Gamma$ is empty,
and in ($\vdash \land $) above, $\Delta$ is empty.
In the cut rule, $\Gamma' $ and $ \Delta'$ are empty.
However there are also rules (the ``display postulates'' described below)
which effectively allow moving formulae from one side to the other.
In \cite{dRA} Gor\'e gives a Display Logic formulation of relation algebras,
called \dRA;
he shows that his set of rules is sound and complete
with respect to the equational axiomatization of Chin \& Tarski.

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 in \fig{dps}.
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 \fig{bsr}.
\item[logical introduction rules] \index{logical introduction rules|textbf}
These rules allow introduction of the logical, or formula, operators.
They are shown in \fig{lir}.
\end{description}

Display Logic is suited to backwards search for proof
of a sequent, that is,
the style of proof starting with the desired conclusion (goal),
finding a rule whose conclusion matches the goal, and then
attempting to prove the premises of the rule (subgoals) in the
same way.
The proof search terminates when there are no remaining subgoals,
(other than instances of (id)).
In terms of backwards proof, 
the logical introduction rules
eliminate the logical operators and
replace them with structural operators.

Unlike Gentzen's sequent calculus, Display Logic has bi-directional
rules, the display postulates.
Therefore any proof search technique must avoid
a naive application of these \emph{ad infinitum}.

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 may write it
$\mathcal P \Longrightarrow \mathcal C$;
for a bi-directional rule we may write $\mathcal P \iff \mathcal C$.
% DISPLAY POSTULATES
\begin{figure}[htbp]
\begin{center}
\begin{tabular}{c@{\hspace{15mm}}c}
 \multicolumn 2 {c} {
 \invrule { *X \vdash Y } { *Y \vdash X } (\ttdef{sA}) \qquad
 \invrule { X \vdash *Y } { Y \vdash *X } (\ttdef{sS}) \qquad
 \invrule { **X \vdash Y } { X \vdash Y } (\ttdef{rssA}) } \\ & \\
 \invrule { \bullet X \vdash Y } { X \vdash \bullet Y } (\ttdef{mblob}) &
 \invrule { \bullet \bullet X \vdash Y } { X \vdash Y } (\ttdef{rbbA}) \\ & \\
\begin{tabular}{@{}c@{}}
$ X \vdash Z, *Y $ \\ \hline \hline $ X,Y \vdash Z $ \\
\hline \hline $ Y \vdash *X,Z $
\end{tabular}
\begin{tabular}{@{}c@{}}
\\[-2.2ex] (\ttdef{sa1}) \\[0.5ex] (\ttdef{sa2})
\end{tabular}
&
\begin{tabular}{@{}c@{}}
$Z, *Y \vdash  X $ \\ \hline \hline $Z \vdash  X,Y $ \\
\hline \hline $*X,Z \vdash  Y $
\end{tabular}
\begin{tabular}{@{}c@{}}
\\[-2.2ex] (\ttdef{ss2}) \\[0.5ex] (\ttdef{ss1})
\end{tabular}
\\ & \\

\begin{tabular}{@{}c@{}}
$ X \vdash Z; *\bullet Y $ \\ \hline \hline $ X;Y \vdash Z $ \\
\hline \hline $ Y \vdash *\bullet X;Z $
\end{tabular}
\begin{tabular}{@{}c@{}}
\\[-2.2ex] (\ttdef{ca1}\dag) \\[0.5ex] (\ttdef{ca2}\dag)
\end{tabular}
&
\begin{tabular}{@{}c@{}}
$Z; *\bullet Y \vdash  X $ \\ \hline \hline $Z \vdash  X;Y $ \\
\hline \hline $*\bullet X;Z \vdash  Y $
\end{tabular}
\begin{tabular}{@{}c@{}}
\\[-2.2ex] (\ttdef{cs2}) \\[0.5ex] (\ttdef{cs1})
\end{tabular}
\end{tabular}
\end{center}
\caption{Display Postulates}
\label{fig:dps}
\end{figure}

% BASIC STRUCTURAL RULES
\begin{figure}[htbp]
\begin{center}
\begin{tabular}{c@{\hspace{15mm}}c}
\multicolumn 2 c {
(tag)\slrule {X ; Y \vdash Z }{\bullet Y ; \bullet X \vdash \bullet Z }
 (\ttdef{taga})
} \\ & \\
($A; \vdash$)\invrule
{X;(Y;Z) \vdash W} {(X;Y);Z \vdash W} (\ttdef{arA}) &
($\vdash A;$)\invrule
{W \vdash X;(Y;Z) } {W \vdash (X;Y);Z } (\ttdef{arS}\dag) \\ & \\

\begin{tabular}{@{}c@{}}
\\[-2.2ex] ($E \vdash $) \\[0.5ex] ($E \vdash $)
\end{tabular}
\begin{tabular}{@{}c@{}}
$ X;E \vdash Y $ \\ \hline \hline $ X \vdash Y $ \\
\hline \hline $ E;X \vdash Y $
\end{tabular}
\begin{tabular}{@{}c@{}}
\\[-2.2ex] (\ttdef{era}) \\[0.5ex] (\ttdef{ela})
\end{tabular}
&
\begin{tabular}{@{}c@{}}
\\[-2.2ex] ($\vdash E $) \\[0.5ex] ($\vdash E $)
\end{tabular}
\begin{tabular}{@{}c@{}}
$Y \vdash  X;E $ \\ \hline \hline $Y \vdash  X $ \\
\hline \hline $Y \vdash  E;X $
\end{tabular}
\begin{tabular}{@{}c@{}}
\\[-2.2ex] (\ttdef{els}) \\[0.5ex] (\ttdef{ers})
\end{tabular}
\\ & \\

($\bullet E \vdash$)\invrule{E \vdash X}{\bullet E \vdash X} (\ttdef{bEa}\dag) &
($\vdash \bullet E $)\invrule{X \vdash E }{X \vdash \bullet E }
(\ttdef{bEs}\dag)\\ & \\
($\bullet I \vdash$)\invrule{I \vdash X}{\bullet I \vdash X} (\ttdef{bIa}\dag) &
($\vdash \bullet I $)\invrule{X \vdash I }{X \vdash \bullet I }
(\ttdef{bIs}\dag)\\ & \\

\begin{tabular}{@{}c@{}}
\\[-2.2ex] ($I \vdash $) \\[0.5ex] ($I \vdash $)
\end{tabular}
\begin{tabular}{@{}c@{}}
$ X,I \vdash Y $ \\ \hline \hline $ X \vdash Y $ \\
\hline \hline $ I,X \vdash Y $
\end{tabular}
\begin{tabular}{@{}c@{}}
\\[-2.2ex] (\ttdef{ira}) \\[0.5ex] (\ttdef{ila})
\end{tabular}
&
\begin{tabular}{@{}c@{}}
\\[-2.2ex] ($\vdash I $) \\[0.5ex] ($\vdash I $)
\end{tabular}
\begin{tabular}{@{}c@{}}
$Y \vdash  X,I $ \\ \hline \hline $Y \vdash  X $ \\
\hline \hline $Y \vdash  I,X $
\end{tabular}
\begin{tabular}{@{}c@{}}
\\[-2.2ex] (\ttdef{ils}) \\[0.5ex] (\ttdef{irs})
\end{tabular}
\\ & \\

(VerI)\slrule
{I \vdash X} {Y \vdash X} (\ttdef{exs}\dag) &
(ExI)\slrule 
{X \vdash I } {X \vdash Y } (\ttdef{exa}\dag) \\ & \\

($M \vdash$)\slrule
{X \vdash Z} {X,Y \vdash Z} (\ttdef{mra}) &
($\vdash M $)\slrule
{Z \vdash X } {Z \vdash X,Y } (\ttdef{mrs}\dag) \\ & \\

($C \vdash$)\slrule
{X,X \vdash Z} {X \vdash Z} (\ttdef{cA}) &
($\vdash C $)\slrule
{Z \vdash X,X } {Z \vdash X } (\ttdef{cS}\dag) \\ & \\

($A \vdash$)\invrule
{X,(Y,Z) \vdash W} {(X,Y),Z \vdash W} (\ttdef{aA}) &
($\vdash A$)\invrule
{W \vdash X,(Y,Z) } {W \vdash (X,Y),Z } (\ttdef{aS}\dag) \\ & \\

($P \vdash$)\slrule
{Y,X \vdash Z} {X,Y \vdash Z} (\ttdef{pA}) &
($\vdash P $)\slrule
{Z \vdash Y,X } {Z \vdash X,Y } (\ttdef{pS}\dag)  
 
\end{tabular}
\end{center}
\caption{Basic Structural Rules}
\label{fig:bsr}
\end{figure}

% LOGICAL INTRODUCTION RULES
\begin{figure}[htbp]
\begin{center}
\begin{tabular}{c@{\hspace{15mm}}c}

($\0 \vdash $) $\0 \vdash E$ (\ttdef{r0A}) &
($\vdash \0 $) \slrule {Z \vdash E } {Z \vdash \0 } (\ttdef{r0S}) \\ & \\

($\1 \vdash $) \slrule {E \vdash Z} {\1 \vdash Z} (\ttdef{r1A}) &
($\vdash \1 $) $E \vdash \1 $ (\ttdef{r1S}) \\ & \\

($\circ \vdash $) \slrule {A;B \vdash Z} {A \circ B \vdash Z} (\ttdef{compa}) &
($\vdash \circ $) \slrule {X \vdash A \quad Y \vdash B}
  {X;Y \vdash A \circ B} (\ttdef{comps}) \\ & \\

($+ \vdash $) \slrule {A \vdash X \quad B \vdash Y }
  {A + B \vdash X;Y } (\ttdef{rsa}) &
($\vdash + $) \slrule {Z \vdash A;B } {Z \vdash A + B } (\ttdef{rss}) \\ & \\

($\smile \vdash $) \slrule {\bullet A \vdash Z} {\smile A \vdash Z}
(\ttdef{conva})&
($\vdash \smile $) \slrule {Z \vdash \bullet A } {Z \vdash \smile A }
(\ttdef{convs})\\ & \\

($\bot \vdash $) $\bot \vdash I$ (\ttdef{fA}) &
($\vdash \bot $) \slrule {Z \vdash I } {Z \vdash \bot } (\ttdef{fS}) \\ & \\

($\top \vdash $) \slrule {I \vdash Z} {\top \vdash Z} (\ttdef{tA}) &
($\vdash \top $) $I \vdash \top $ (\ttdef{tS}) \\ & \\

($\lor \vdash $) \slrule {A \vdash X \quad B \vdash Y }
  {A \lor B \vdash X,Y } (\ttdef{ora}) &
($\vdash \lor $) \slrule {Z \vdash A,B } {Z \vdash A \lor B } (\ttdef{ors}) \\ & \\

($\land \vdash $) \slrule {A,B \vdash Z} {A \land B \vdash Z} (\ttdef{anda}) &
($\vdash \land $) \slrule {X \vdash A \quad Y \vdash B}
  {X,Y \vdash A \land B} (\ttdef{ands}) \\ & \\

($\lnot \vdash $) \slrule {* A \vdash Z} {\lnot A \vdash Z} (\ttdef{nota}) &
($\vdash \lnot $) \slrule {Z \vdash * A } {Z \vdash \lnot A } (\ttdef{nots}) 
\end{tabular}
\end{center}
\caption{Logical Introduction Rules}
\label{fig:lir}
\end{figure}

\section{Isabelle}

Isabelle is an interactive computer-based proof system,
described in \cite{Int} and \cite{Ref}.
It is written in Standard ML;
when it is running, the user can interact with it by
entering further ML commands.

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.
Anything that can be proved using this built-in logic is a theorem,
of ML type \ttdef{thm}.

The user then has to define an object-level logic,
though normally one would use one of
several which are packaged with the Isabelle distribution \cite{OL}.
These include 
\begin{itemize} \shrinklist{0.5}
\item FOL, first-order logic in a natural deduction style
\item ZF, Zermelo-Fraenkel set theory, built on FOL
\item HOL, Church's higher-order logic
\item LK, first-order logic using the sequent calculus
\item CTT, Constructive Type Theory
\item CCL, Classical Computational Logic
\item LCF, Logic for Computable Functions
\item Modal, the modal logics T, S4 and S43, built on LK
\end{itemize}

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.

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}
%In many object-logics the theorems one typically wishes to prove are
%expressible entirely using the constructs of that object-logic;
%in other cases one way often want to prove theorems 
Isabelle theorems (including the axioms of the theory)
may or may 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
may be either a `simple' theorem of \dRA, of the form $X \vdash Y$,
or a \bfi{rule}, corresponding to an Isabelle theorem containing
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}
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{sA} rule, shown in \fig{dps},
appears as \texttt{"* \$?X |- \$?Y == * \$?Y |- \$?X"}.
An Isabelle theorem whose use of the metalogic is
even more complex is \texttt{G910meth}, discussed on \page{G910meth}.

Isabelle provides a number of basic proof steps for
backwards proof (\textbf{tactics}\index{tactic|textbf}), as well as 
functions for combining these in various ways 
(\textbf{tacticals}\index{tactical|textbf}).
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.
%and there are some which are applicable
%to most or all object logics. 
Some tactics are designed for a more automated style of proof search;
they will repeatedly attempt a large number of tactics.
Others, for example \ttdef{rtac}, are designed more for interactive use,
when the user can see what proof steps are needed.
Thus \texttt{rtac} \textit{th sg} attempts to match the conclusion of 
theorem \textit{th} to subgoal number \textit{sg} -- if it succeeds,
it will replace that subgoal by the premises (if any) of \textit{th}.

Isabelle also supports forward proof; a function commonly used is
\ttdef{RS} (which is binary infix);
for example, if \textit{th} is a rule with a single premise,
\textit{thsf}~\texttt{RS}~\textit{th} 
in effect uses the rule \textit{th} 
to transform the conclusion of \textit{thsf}.
More precisely, if 
\textit{thsf} is $A' \texttt{==>} B'$,
and \textit{th} is $B'' \texttt{==>} C''$,
and the most general unifier of $B'$ and $B''$ is $\theta$,
(so $ B' \theta = B'' \theta$)
%taking these to 
%$A' \theta \texttt{==>} B' \theta$ and 
%$B'' \theta \texttt{==>} C'' \theta$,
then \textit{thsf} \texttt{RS} \textit{th} is 
$A' \theta \texttt{==>} C'' \theta$.

\renewcommand\cfile{}