\begin{thebibliography}{FHMV95}

\bibitem[AB75]{anderson-belnap-entailment-I}
A~R Anderson and N~D Belnap.
\newblock {\em Entailment: The Logic of Relevance and Necessity}, 1.
\newblock Princeton University Press, Princeton, USA, 1975.

\bibitem[{Bel}82]{belnap-display}
N~D {Belnap}.
\newblock Display logic.
\newblock {\em J. of Philosophical Logic}, 11:375--417, 1982.

\bibitem[BGH95]{barwise-gabbay-hartonas-information-flow}
J~Barwise, D~Gabbay, and C~Hartonas.
\newblock On the logic of information flow.
\newblock {\em Bulletin of the IGPL}, 3(1):7--49, 1995.

\bibitem[Cer82]{farinal-del-cerro-simple}
L~Farinas~Del Cerro.
\newblock A simple deduction method for modal logic.
\newblock {\em Information Processing Letters}, 14(2):49--51, 1982.

\bibitem[Daw97]{dawson-rewr}
J~E Dawson.
\newblock Simulating term-rewriting in {LPF} and in display logic.
\newblock (submitted), Automated Reasoning Project, 1997.

\bibitem[DEL90]{debart-enjalbert-lescot-multi-modal}
F~Debart, P~Enjalbert, and M~Lescot.
\newblock Multi-modal logic programming using r=equational and order-sorted
  logic.
\newblock Technical Report 90-3, 1990.

\bibitem[DG97]{dawson-gore-dra}
J~E Dawson and R~Gor\'{e}.
\newblock A mechanised proof system for relation algebra using display logic.
\newblock (submitted), Automated Reasoning Project, 1997.

\bibitem[DG98]{demri-gore-nominal-tense}
S~Demri and R~Gor\'{e}.
\newblock Cut-free display calculi for nominal tense logics.
\newblock (submitted), Automated Reasoning Project, 1998.

\bibitem[DSH93]{dosen-schroeder-heister-substructural}
K~Do{\v{s}}en and P~Schroeder-Heister, editors.
\newblock {\em Substructural Logics}.
\newblock Studies in Logic and Computation. Oxford University Press, 1993.

\bibitem[FHMV95]{Fagin&Halpern&Moses&Vardi95}
R Fagin, J Halpern, Y Moses, and M Vardi.
\newblock {\em Reasoning about {K}nowledge}.
\newblock The MIT Press, 1995.

\bibitem[Gir87]{girard-linear}
J-Y Girard.
\newblock Linear logic.
\newblock {\em Theoretical Computer Science}, 50:1--102, 1987.

\bibitem[Gor97]{gore-relalg}
R~Gor\'{e}.
\newblock Cut-free display calculi for relation algebras.
\newblock In D~van Dalen and M~Bezem, editors, {\em CSL96},
   LNCS 1258, 198--210. Springer, 1997.

\bibitem[Gor98]{gore-sld-igpl}
R~Gor\'{e}.
\newblock Substructural logics on display.
\newblock {\em Logic Journal of the IGPL}, 6(3):451--504, 1998.

\bibitem[HC96]{hughes-cresswell-new-introduction}
G~E Hughes and M~J Cresswell.
\newblock {\em A New Introduction To Modal Logic}.
\newblock Routledge, 1996.

\bibitem[HSZ96]{heuerding-seyfried-zimmermann-loop}
A Heuerding, M Seyfried, and H Zimmermann.
\newblock Efficient loop-check for backward proof search in some non-classical
  logics.
\newblock In {\em Tableaux 96},
   LNAI 1071, 
  210--225. Springer, 1996.

\bibitem[Kra96]{kracht-power}
M~Kracht.
\newblock Power and weakness of the modal display calculus.
\newblock In H~Wansing, editor, {\em Proof Theory of Modal Logics}, 
  92--121. Kluwer, 1996.

\bibitem[MFD96]{fisher-woolridge-dixon-resolution}
M~Wooldridge M~Fisher and C~Dixon.
\newblock A resolution-based proof method for temporal logics of knowledge and
  belief.
\newblock In D~Gabbay and J-J Ohlbach, editors, {\em Proceedings of FAPR'96},
  178--192. Springer-Verlag, 1996.

\bibitem[Ohl88]{ohlbach-resolution-modal}
H-J Ohlbach.
\newblock A resolution calculus for modal logics.
\newblock In {\em CADE-9}, LNCS 310, 
   500--516. Springer-Verlag, 1988.

\bibitem[Pau90]{paulson-700}
L~C Paulson.
\newblock Isabelle: The next 700 theorem provers.
\newblock In P~Odifreddi, editor, {\em Logic and Computer Science}, 
  361--385. Academic Press, 1990.

\bibitem[Pra91]{pratt-action-logic}
V~Pratt.
\newblock Action logic and pure induction.
\newblock In {\em JELIA90},
 LNCS 478, 97--120. Springer-Verlag, 1991.

\bibitem[Res98]{restall-substructural-I}
G~Restall.
\newblock Displaying and deciding substructural logics {I}: logics with
  contraposition.
\newblock {\em Journal of Philosophical Logic}, to appear, 1998.

\bibitem[Wal89]{wallen-book}
L~A Wallen.
\newblock {\em Automated Deduction in Nonclassical Logics: Efficient Matrix
  Proof Methods for Modal and Intuitionistic Logics}.
\newblock MIT Press, 1989.

\bibitem[Wan94]{wansing-sequent}
H~Wansing.
\newblock Sequent calculi for normal modal propositional logics.
\newblock {\em Journal of Logic and Computation}, 4:125--142, 1994.

\end{thebibliography}