\renewcommand\cfile{other.tex}
\section{Comparing Different Logical Calculi for RA Using \dRA}

In this section we describe how we used 
the implementation of \dRA\ in Isabelle
to demonstrate the soundness
of some other logical systems for relation algebra.
(As described in \S\ref{provRA}, we did the same for \RA;
as we use \RA\ as a ``reference point'' we treated this as
a demonstration of the completeness of \dRA).

\subsection{Gordeev's term rewriting system for \RA} \label{gord}

Gordeev \cite{Gor} has given a system \NRA\ of rules for rewriting
relational equations
of the form $F = \top$ (where $F$ is a relational formula and
$\top$ is the unique largest element).
A derivation of $F$ in \NRA\ is a sequence of permitted rewrites 
(``reductions'')
$F \longrightarrow \cdots \longrightarrow  \top$.
Thus \NRA\ proves equations of the form $F = \top$.
However it is known that every Boolean combination of equations is
equivalent to an equation of the form
$F = \top$ (see \cite{Mad}, pp.~435--6, pp.~439--440).
Gordeev has shown that
$F$ is derivable in \NRA\ iff $F=\top$ is derivable in \RA.

It is expected that details of \NRA\ will be published in due course;
the actual rules are not pertinent here, 
since we simply outline how Isabelle
was used as the basis of a proof of the soundness of \NRA.

\NRA\index{NRA@\textbf{NRA}|textbf},
uses ``literals'' ($L$) and ``positive terms'' ($A, B, C, D$).
Literals are of the shape
$P$, $\lnot P$, $\smile P$, $\lnot \smile P$, $\top$, $\bot$, $\0$ or $\1$,
for any given primitive relation symbol $P$.
Positive terms are
built up from literals using the binary operators.
Any \RA\ term is reducible to a positive term by the distributive 
rules which show how the unary operators distribute over the binary operators
(see \fig{sdr} for the structural counterparts).

In \NRA\ there are 12 rewriting rules (NRA1)-(NRA12), but, given a 
%Not all the rules may be used to rewrite an arbitrary part of the 
formula $F$, some may only be used to rewrite $F$ or a conjunct of $F$.
The permitted rewrites, or ``reductions'', are
\begin{itemize}
\item
$F[G'] \longrightarrow F[G'']$,
% $F \longrightarrow F[G' \gets G'']$
where $G' \longrightarrow G''$ is 
an instance of any rule (NRA$i$) except for (NRA9) and (NRA10)
\item $G_1 \land G_2 \land \ldots \land G_j' \land \ldots \land G_k
\longrightarrow 
G_1 \land G_2 \land \ldots \land G_j'' \land \ldots \land G_k$
where $1 \leq j\leq k$ and 
$G_j' \longrightarrow G_j''$ is an instance of (NRA9) or (NRA10)
\end{itemize}

We take it that $F[\cdot]$ above must be such that 
$G$ is a `sub-positive-term' of $F[G]$, ie, that $G$ is not a literal properly
contained in a larger literal within $F[G]$
(for example, $F[G]$ may not be $\lnot G \lor H$).
This point was not spelt out in the brief communication \cite{Gor},
and we realized the need for it only in doing the proof in Isabelle.
This gives an example of the value of a computer-based theorem prover in 
ensuring such details are not overlooked.

%That is, the rules, except for (NRA9) and (NRA10), can be applied to 
%rewrite any sub-positive-term of $F$.
%However, (NRA9) and (NRA10) can be applied to rewrite only a conjunct of $F$.

The following lemma explains the \NRA\ reduction step in terms of \dRA.

\begin{lemma} \label{gordlem}
Whenever $F' \longrightarrow F''$ in \NRA, 
then $\top \vdash F'' \Longrightarrow \top \vdash F'$ in \dRA.
\end{lemma}

\proof\ 
For rules other than (NRA9) and (NRA10), 
we show that $F'' \vdash F'$ in \dRA.
Let $F' = F[G']$ and $F'' = F[G'']$,
where the \NRA\ rule is $G' \longrightarrow G''$.
For each rule the \dRA\ theorem $G'' \vdash G'$ was proved in Isabelle.

%Recall that, for rules other than (NRA9) and (NRA10),
%$F[G'] \longrightarrow F[G'']$ is
%a ``reduction" in \NRA\ where
%$G' \longrightarrow G''$ is an instance of one of the rules.
%So, assume $F' \longrightarrow F''$ is 
%$F[G'] \longrightarrow F[G'']$, where 
%$G' \longrightarrow G''$ is an instance of a rule other than (NRA9) and (NRA10).

From $G'' \vdash G'$ we show $F[G''] \vdash F[G']$
by induction on the structure of $F[\cdot]$.
As $F[\cdot]$ uses only literals and the binary operators,
the inductive steps rely on the four \dRA-theorems
\texttt{cong\_or}, \texttt{cong\_and}, \texttt{cong\_comp} and \texttt{cong\_rs}
(see \S\ref{congs}), and the identity rule $A \vdash A$ .%(\texttt{idf}).

Since $F'' \vdash F'$, if we assume 
$\top \vdash F''$, then the (cut) rule gives $ \top \vdash F'$.

We now look at rules (NRA9) and (NRA10).
For these rules, where the \NRA\ rule is \mbox{$G' \longrightarrow G''$,}
we have proved the \dRA\ derived rule
$\top \vdash G'' \Longrightarrow \top \vdash G'$ in Isabelle.
%
%Now for these rules,
%$F[G'] \longrightarrow F[G'']$ is
%a ``reduction" in \NRA\ where
%$G'$ is a conjunct of $F[G']$, 
%and $G' \longrightarrow G''$ is an instance of one of the rules.
%So we have 
%$\top \vdash G'' \Longrightarrow \top \vdash G'$,
So from this we need to show 
$\top \vdash F[G''] \Longrightarrow \top \vdash F[G']$,
where $G'$ is a conjunct of $F[G']$. 
This is shown by induction on the number of conjuncts in $F[\cdot]$.
The inductive step uses the following \dRA-theorem.
\begin{center}
\slrule {  \top \vdash G1'' \Longrightarrow \top \vdash G1' \qquad
      \top \vdash G2'' \Longrightarrow \top \vdash G2' }
       { \top \vdash G1'' \land G2'' \Longrightarrow \top \vdash G1' \land G2'}
(\ttdef{G910meth})
\end{center}
\qed

\label{G910meth}\texttt{G910meth} is
a theorem whose use of Isabelle's metalogic is
more complex than others seen so far,
with nested occurrences of the
metalogical operator $\Longrightarrow$.

% It follows easily from the lemma that
Lemma 1 implies that
for every \NRA-derivation of $F$ there is a
\dRA-derivation of $\top \vdash F$.
%This demonstrates the soundness of \NRA\ with respect to \RA.
Thus \NRA\ is sound with respect to \RA.

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

In \cite{thesis}, Ch.~4, we described the sequent calculus system
of Maddux \cite{seqra},
\M, for relation algebras, and showed how its sequents and proofs
correspond to sequents and proofs in \dRA.
We characterized the sequents in \M\ which can be translated into
\dRA by describing the pattern of relation variables and point
variables in the \M-sequent as a graph,
and showing that whether or not an \M-sequent
can be translated into \dRA\ depends on the shape of the graph.

As a sequent in \M\ can often be translated to
any of several sequents in \dRA,
we showed that these several sequents are equivalent in \dRA.

The result relating proofs in the two systems was that
if an \M-sequent $\mathcal S$
can be translated into a \dRA-sequent $\mathcal S'$,
then any \M-proof of $\mathcal S$
can be translated into a \dRA-proof of $\mathcal S'$,
provided that the \M-proof uses at most four point variables.
This required showing how such a proof in \M\ can be divided into
parts each of which could be turned into a part of a proof in \dRA.

As not all \M-sequents containing at most four point variables
can be translated into \dRA,
not all the intermediate stages of such a proof could be translated into \dRA,
that is, not every individual step of the \M-proof could be converted into
a corresponding step of a proof in \dRA.
Rather, a larger portion of the \M-proof had to be treated as a unit;
we showed that we could always rearrange the \M-proof to get
these portions of a particular form, which
conformed to a theorem that we had proved in Isabelle for \dRA.

This result provided a constructive proof of one direction of the result of
Maddux (\cite{seqra}, Thm.~6) that the class of relation algebras is
characterized by the \M-sequents provable using four variables.
%The possibility of doing a similar translation in the reverse direction is
%discussed in \ch{apfw}.


\renewcommand\cfile{}