\begin{thebibliography}{99}

%\bibitem{hoare} Ten Years of Hoare's Logic -- A Survey, Part I,
%ACM Trans.\ Program.\ Lang.\ Syst.\ 3 (1981), 431--483.

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

\bibitem{RALF} Rudolf Berghammer \& Claudia Hattensperger,
Computer-Aided Manipulation of Relational Expressions and Formulae Using RALF,
preprint.

\bibitem{birk} Garrett Birkhoff,
On the Structure of Abstract Algebras,
Proc.\ Cambridge Phil.\ Soc.\ 31 (1935), 433-454.

\bibitem{BrS} R.J. Brachman \& J.G. Schmolze, 
An overview of the \textsc{KL-ONE} knowledge representation system,
Cognitive Science 9(2) (1985), 171--216.

\bibitem{BBS} Chris Brink, Katarina Britz \& Renate A. Schmidt,
Peirce Algebras, 
Formal Aspects of Computing 6 (1994), 339--358.

\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{thesis} Jeremy E. Dawson,
Mechanised Proof Systems for Relation Algebras,
Grad.\ Dip.\ Sci.\ sub-thesis, Dept of Computer Science,
Australian National University.  Available at
\verb|http://arp.anu.edu.au:80/~jeremy/thesis.dvi|

\bibitem{rewr} Jeremy E. Dawson,
Simulating Term-Rewriting in LPF and in Display Logic,
submitted.
Available at
\verb|http://arp.anu.edu.au:80/~jeremy/rewr/rewr.dvi|

%\bibitem{wp} Edsger W. Dijkstra,
%A Discipline of Programming, Prentice-Hall, 1976.

%\bibitem{dove} K.A.Easthaughffe, M.A.Ozols and A.Cant,
%Proof Tactics for a Theory of State Machines in a Graphical Environment,
%Proceedings of CADE-14, Lecture Notes in Computer Science 1249 (1997),
%366--379.

%\bibitem{db} Ramez A. Elmasri \& Shamkant B. Navathe,
%Fundamentals of Database Systems, 2nd ed, Benjamin/Cummings, Redwood City,
%1994.

\bibitem{Gallier} Jean H. Gallier,
Logic for Computer Science : Foundations of Automatic Theorem Proving, 
Harper \& Row, New York, 1986.

\bibitem{Gor} Lev Gordeev, personal communication.

%\bibitem{HOLdesc} The HOL System Description, Version 2,
%Computer Laboratory, Cambridge, 1991.

\bibitem{ILR} Rajeev Gor\'e, Intuitionistic Logic Redisplayed, 
Automated Reasoning Project TR-ARP-1-95, ANU, 1995.

\bibitem{dRA} Rajeev Gor\'e, 
Cut-free Display Calculi for Relation Algebras,
Computer Science Logic, Lecture Notes in Computer Science 1249 (1997), 198--210.
(or see \verb'http://arp.anu.edu.au/~rpg/publications.html').

\bibitem{jgwi} Jim Grundy,
Transformational Hierarchical Reasoning,
The Computer Journal 39 (1996), 291--302.

%\bibitem{CylII} Leon Henkin, J. Donald Monk \& Alfred Tarski,
%Cylindric Algebras, Part II,
%Elsevier, Amsterdam, 1985.

%\bibitem{Hennessy} M.C.B.Hennessy, 
%A proof-system for the first-order relational calculus,
%J. Comput.\ System Sci.\ 20 (1980), 96--110.

\bibitem{ho} G\'erard Huet \& Derek C. Oppen,
Equations and Rewrite Rules -- A Survey,
in Formal Languages: Perspectives and Open Problems, R.V. Book (ed),
Academic Press (1980), 349--405.

%\bibitem{JTII} Bjarni J\'onnson \& Alfred Tarski,
%Boolean Algebras with Operators, Part II,
%Amer.\ J. Math. 74 (1952), 127--162.

\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,
Proceedings of CADE-14, Lecture Notes in Computer Science 1249 (1997), 380--394.

% \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.

\bibitem{wi}
Peter J. Robinson \& John Staples,
Formalizing a Hierarchical Structure of Practical Mathematical Reasoning,
J. Logic \& Computation, 3 (1993), 47--61.

% \bibitem{Schonfeld} W. Sch\"onfeld, 
%Upper bounds for a proof-search in a sequent calculus for relational equations,
% Z. Math.\ Logik Grundlagen Math.\ 28 (1982), 239--246.

% \bibitem{Wadge} W. Wadge, 
% A complete natural deduction system for the relational calculus,
% Theory of Computation Report no.~5, University of Warwick, 1975.

\bibitem{Wansing} Heinrich Wansing,
Sequent Calculi for Normal Modal Propositional Logics,
Journal of Logic and Computation 4 (1994), 124--142. 

\end{thebibliography}