\documentclass[a4paper,12pt]{article}

\renewcommand{\today}{\number\day\ 
  \ifcase\month\or
  January\or February\or March\or April\or May\or June\or
  July\or August\or September\or October\or November\or December\fi
  \ \number\year}

\setlength\oddsidemargin{0mm}
\addtolength\textwidth{20mm}
\addtolength\textheight{20mm}
\addtolength\topmargin{-20mm}
\addtolength\parskip{2mm}

\newenvironment{litlist}
{\begin{list}{--}{
\setlength\parsep{0mm}
\setlength\itemsep{0mm}
\setlength\topsep{0.0\topsep}
\setlength\leftmargin{0.0\leftmargin}
\setlength\itemindent{0.9\parindent}}}
{\end{list}}

%\usepackage{amssymb}
%\usepackage{latexsym}

\renewcommand\thesubsubsection{\arabic{subsubsection}}
\renewcommand\theparagraph{\thesubsubsection.\arabic{paragraph}}
%\setcounter{secnumdepth}4

\begin{document}

{\bfseries{\centering\large AUTOMATING DISPLAY LOGIC

LITERATURE SURVEY

Jeremy Dawson

}}

\subsubsection{Introduction}

Display Logic is a system for representing logic, based on the Gentzen 
sequent calculus.
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 specific logic satisfy certain conditions.

Relation algebras are extensions of Boolean algebras, devised to model
relations on a given set rather than subsets of a set.
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 axiomatically using display
logic, and in several other ways.

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

The aim of the project is to implement the display logic formulation of 
relation algebras in Isabelle, and to demonstrate the relationship 
between this and some other formulations of relation algebras.

\subsubsection{Relation algebras}
A \textbf{relation}
on a set $U$ is a set of ordered pairs $(a,b)$ of elements of $U$, 
ie a subset of $U \times U$.
Relation Algebras are an abstraction of the notion of relations on a set $U$;
reference to the actual elements of the set is abstracted away, leaving
the relations themselves as the objects being considered.
Thus a relation algebra is a set (whose members correspond to the relations),
with a number of operations.
Since a relation is itself a set 
(of ordered pairs),
the operations of relation algebras
include the operations of Boolean algebras.
Other relation algebra operations are 
(as defined in \cite{RA})
{\bfseries composition} 
$R \circ S = \{ (a,b) \;|\; \exists c.\; (a,c) \in R 
\textrm { and } (c,b) \in S \}$,
its \textbf{identity} $\{ (a,a) \;|\; a \in U \}$, and 
{\bfseries converse} 
$\smile R = \{ (a,b) \;|\; (b,a) \in R \}$.

Chin \& Tarski \cite{CT} give a finite axiomatization of relation algebras.
These axioms capture most, but not all, of the characteristics of 
a {\bfseries proper} relation algebra, that is, a relation algebra 
consisting of a set of relations on a set $U$.
Note that in a proper relation algebra, there is a largest relation $T$
(with respect to which complements are taken);
$T$ need not be $U \times U$, though it must be an equivalence relation
(\cite{CT}, p.~345; \cite{Mad}, p.~444).
A relation algebra is called
{\bfseries representable} if in addition to satisfying Tarski's axioms,
it is isomorphic to a proper relation algebra.
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).

However it seems that a relation algebra is necessarily atomic.
An {\bfseries atom}
in a Boolean algebra is 
an element that is not the union of smaller elements
(intuitively, like a singleton set);
a Boolean algebra is 
{\bfseries atomic} if every element is a union of atoms.
Oheimb \& Gritzner \cite{RALL}
appear to say that every relation algebra is atomic,
and the proof system described there appears to apply to atomic algebras.
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).

There are a number of ways to define relation algebras.
There are several similar 
axiomatic definitions, described in \cite{Mad}, pp.~441--2,
of which that of Chin \& Tarski \cite{CT}
is used in \cite{RA}.
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}, ie,
it has no non-trivial congruence relations (\cite{Mad}, p.~441), 
or, equivalently,
it has no non-trivial \textbf{ideal elements} (see \cite{CT}, p.~362).

Gordeev \cite{Gor} has proposed a system of axioms for rewriting equations
of the form $F = T$, where $T$ 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 = T$.
However it has been shown that every boolean combination of equations is
equivalent to an equation of the form
$F = T$ (see \cite{CT}, pp.~435--6, pp.~439--440).

Oheimb \& Gritzner \cite{RALL} have developed a proof system, 
called RALL, for relation algebras, in Isabelle.
It is based on the Isabelle HOL set theory, and the Lattice theory 
which is built upon that.
The Lattice theory is stated to define the class of complete atomic boolean
lattices, and the RALL system makes heavy use of the atomicity of relation
algebras.
It does this by converting an algebraic expression into a propositional one,
by regarding an element as the collection of atoms contained in it.
For example $x \subseteq y \cup z$ becomes
$\forall a:\mbox{atom. } a \subseteq x \to  a \subseteq y \vee a \subseteq z$.
The basis for this is the theorem (\cite{RALL}, Thm.~2)
that a relation algebra can be
represented as a ``relational atom structure",
which enables a relation algebra to be considered in terms of its atoms.

\subsubsection{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 sets, or propositions;
this example means 
($P$ and $Q$) implies ($R$ or $S$).
Each of $P,Q, R,S$ represents a formula such as $A \& B$.
The sequent calculus rules are basically of the form
where a sequent containing a formula with a connective
is derived from one or more sequents not using that connective.
For example, the rules for introducing the connective ``\&'' into the
left and right sides of a sequent are
$$ \frac {\Gamma, P, Q \vdash \Delta} {\Gamma, P \& Q \vdash \Delta}
\quad \textrm{ and } \quad 
\frac {\Gamma \vdash \Delta, P \qquad \Gamma \vdash \Delta, Q}
{\Gamma \vdash \Delta, P \& Q}$$ 
where $\Gamma$ and $\Delta$ denote comma-separated lists of formulae.
Thereby, 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 using these rules.
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
will normally 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 extends these ideas. 
A distinction is made between 
{\bfseries structures} and
{\bfseries formulae}.
A structure is the analogue of (in Gentzen) a sequence of formulae, separated
by commas; a structure is defined as a formula, or a combination of 
structures formed using the structural operators (which include comma).
There are rules (``display rules")
for manipulating sequents to enable any chosen structure
to be ``displayed", ie, appear by itself, on one side of the turnstile.
These rules are bidirectional (ie, equivalences), which is indicated by a
double bar.
For example, one such rule is 
%$$ \frac {P,Q \vdash R} {P \vdash R,*Q} $$
\begin{center}
\begin{tabular}{c}
$ {P,Q \vdash R} $ \\ \hline \hline $ {P \vdash R,*Q} $
\end{tabular}
\end{center}
where ``*" is a structural connective corresponding to ``not".
The third structural operator for classical propositional logic is ``$I$'',
which means ``true" or ``false", depending on whether it is in
an \textbf{antecedent} position (within the scope of an even/odd number
of `*' symbols when on the left/right) or in a \textbf{succedent} position
(vice versa).

A number of different logical systems can be formulated using the
method, or style, of Display Logic.
These include several normal modal logics, and intuitionistic logic
\cite{ILR}.
Much of the behaviour of these logics is captured by the
display rules and some other simple 
``structural rules",
rules which apply at the structural level, ie, they are expressed in terms of
arbitrary structures rather than formulae.
There are then the ``logical rules", which are rules for introducing the
various logical connectives.
The valuable cut-elimination theorem of sequent calculus (which 
says that if a sequent is provable, it is provable without using the cut rule)
applies in all
of these logics, provided that the rules satisfy certain conditions, which are
relatively easily checked (\cite{Bel}).

There is an axiomatic definition for relation algebras in terms of Display
Logic \cite{RA},
called {\boldmath $\delta$}\textbf{RA}.
It uses six structural operators, three for classical logic, or Boolean algebra
(as above), and three operators 
``;", ``$\bullet$", and ``E",
which, in an antecedent position,
represent composition and converse
of relations, and the identity relation.
The Display Rules bear a striking similarity to the display rules for the 
Boolean operators, for example
\begin{center}
\begin{tabular}{c}
$ {P;Q \vdash R} $ \\ \hline \hline $ {P \vdash R;*\bullet Q} $
\end{tabular}
\end{center}

Maddux \cite{seqra} deals with relation algebras in terms of the relations
and, in a sense, of the elements of the set $U$.
He gives a sequent calculus in which variables appear in 
the place of elements of $U$.
Thus, for example, his rules for introducing the conjunction operator
(which we write ``\&") are
$$ \frac {\Gamma, xRy, xSy \vdash \Delta} {\Gamma, xR \& Sy \vdash \Delta}
\quad \textrm{ and } \quad 
\frac {\Gamma \vdash \Delta, xRy \qquad \Gamma \vdash \Delta, xSy}
{\Gamma \vdash \Delta, xR \& Sy}$$ 
If the $x$ and $y$ are removed from these rules, they become
the rules of the sequent calculus shown above,
which are themselves
easily derivable in the Display Logic system {\boldmath $\delta$}\textbf{RA}.
However the rules for introducing the relation composition operator
(which we write $\circ$) are
$$ \frac {\Gamma, xRy, ySz \vdash \Delta} {\Gamma, xR \circ Sz \vdash \Delta}
\quad \textrm{ and } \quad 
\frac {\Gamma \vdash \Delta, xRy \qquad \Gamma \vdash \Delta, ySz}
{\Gamma \vdash \Delta, xR \circ Sz}$$ 
with the restriction that $y$ cannot appear in the conclusion of the first of
these rules.
There appears to be no straightforward way to represent these rules in 
{\boldmath $\delta$}\textbf{RA}.

Since the $x,y,z$ in this formulation stand for members of $U$, it
may be suspected that the system actually axiomatizes \emph{representable}
relation algebras rather than general relation algebras.
However, Maddux looks at $MA_n$, the class of
algebras satisfying all properties which can be proved from his sequent rules
using only $n$ variables $x,y,z,\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).

\subsubsection{Isabelle}

Isabelle is an automated 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 applied to the user's own choice of
logical system, for very little is built in.
The logic built in is described as intuitionistic higher-order logic,
with three operators producing propositions: 
\texttt{==>} (implication),
\texttt{==} (equality), and
\texttt{!!} (universal quantification).
These operators have only the properties necessary to support their meanings.
For example, since
\texttt{[| P; Q |] ==> R}
means that \texttt R can be deduced from \texttt P and \texttt Q,
it necessarily follows that
\texttt{[| P ==> Q; P |] ==> Q}, and that
\texttt{([| P; Q |] ==> R) ==> ([| Q; P |] ==> R)}.
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 supply 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}
\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 amd S43, built on LK
\end{itemize}

Isabelle provides a number of basic proof steps (\textbf{tactics}), as well as 
functions for combining these in various ways (\textbf{tacticals}).
The user can also write complex proof tactics in ML;
many complex tactics are supplied with
the standard Isabelle object logics,
and there are some which are applicable
to most or all object logics. 

\subsubsection{Automating Display Logic}

Isabelle can be used to show the equivalence of Display Logic 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 Display Logic is effective for proving the various
axioms of the other systems.

Some of these proofs are, however, far from straightforward,
particularly if they are to be done without using cut.
A proof which is done by hand, and then translated into Display Logic
in a natural way, will often contain cuts; the cut-elimination theorem shows
how to eliminate them, but this can produce a longer proof.

The cut-elimination theorem enables proofs to be done using backwards proof,
where there is, at each step, a limited choice of rules from which one must be
chosen.
In the Display Logic formulation of classical propositional logic
(which is decidable), 
a straightforward implementation of these rules leads naturally to a decision
procedure.

A decision procedure, or any systematic automated procedure, 
therefore needs to have methods of doing cut-free proofs.
As the theory of relation algebras is not decidable, 
no simple application of rules will guarantee success;
there is a need to find strategies that are useful
for producing cut-free proofs in 
Display Logic, with a view to automating them.

Other aspects of the implementation may be
\begin{itemize}
\item automating the cut-elimination procedure, to produce a cut-free proof
from a proof involving the cut rule
\item automatically producing a printable record of a proof 
\item producing a record of the elementary rules used when a complex
tactic is applied
\item automatically converting a proof in one system (eg the Chin \& Tarski
axiomatization, or the Gordeev system) to {\boldmath $\delta$}\textbf{RA},
or vice versa
\item developing tactics to use the principles behind the window inference
method
\end{itemize}

\subsubsection{Work done so far}

Work done so far includes
\begin{itemize}
\item an Isabelle theory for the Display Logic system
{\boldmath $\delta$}\textbf{Kt} for tense logic (\cite{ILR})
\item an Isabelle theory for the Display Logic system
{\boldmath $\delta$}\textbf{RA} for Relation Algebras (\cite{RA})
\item a large number of derived rules to facilitate proofs in
{\boldmath $\delta$}\textbf{Kt} and {\boldmath $\delta$}\textbf{RA} 
\item a number of complex tactics for proofs in 
{\boldmath $\delta$}\textbf{Kt} and {\boldmath $\delta$}\textbf{RA},
including tactics to 
\begin{itemize}
\item display a selected structure
\item prove a subgoal by weakening and the identity rule
\item simulate a global search-and-replace by displaying all 
structures in a sequent and applying a chosen set of rules, if
possible, to each one
\end{itemize}
\item {\boldmath $\delta$}\textbf{RA}
proofs of a number of theorems of relation algebras
\end{itemize}

\begin{thebibliography}{99}

\bibitem{Bel} Nuel D. Belnap, Display Logic, Journal of Philosophical Logic
11 (1982), 375-417.

\bibitem{CT} Louise H. Chin \& Alfred Tarski,
Distributive and Modular Laws in the Arithmetic of Relation Algebras,
University of California Publications in Mathematics, New Series,
I (1943-1951), 341-384.

\bibitem{Gor} Lev Gordeev, personal communication.

\bibitem{ILR} Rajeev Gore, Intuitionistic Logic Redisplayed, 
Automated Reasoning Project Technical Report TR-ARP-1-95, ANU, 1995.

\bibitem{RA} Rajeev Gore, 
Cut-free Display Calculi for Relation Algebras,
preprint, Automated Reasoning Project, ANU, 1997.

\bibitem{seqra} Roger D. Maddux, A Sequent Calculus for Relation Algebras,
Annals of Pure and Applied Logic 25 (1983), 73-101.

\bibitem{Mad} Roger D. Maddux, The Origin of Relation Algebras in the
Development and Axiomatization of the Calculus of Relations,
Studia Logica 50 (1991), 421-455.

\bibitem{RALL} David von Oheimb \& Thomas F. Gritzner,
RALL: Machine-supported proofs for
Relation Algebra, to appear in the Conference Proceedings of CADE-14, 
Lecture Notes in Computer Science.

\bibitem{Int} Lawrence C. Paulson,
Introduction to Isabelle,
Computer Laboratory, University of Cambridge, 1995.

\bibitem{Ref} Lawrence C. Paulson,
The Isabelle Reference Manual,
Computer Laboratory, University of Cambridge, 1995.

\bibitem{OL} Lawrence C. Paulson,
Isabelle's Object-Logics,
Computer Laboratory, University of Cambridge, 1995.

\end{thebibliography}
\end{document}