\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{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{wp} Edsger W. Dijkstra,
A Discipline of Programming, Prentice-Hall, Englewood Cliffs, 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 Technical Report 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.

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

\end{thebibliography}