\begin{thebibliography}{MJCG93}

\bibitem[ams08]{ams-formal-proof}
Special issue on formal proof.
\newblock Notices of the American Mathematical Society, volume 55, December
  2008.

\bibitem[Bd96]{bierman96}
Gavin Bierman and Valeria {de Paiva}.
\newblock Intuitionistic necessity revisited.
\newblock In {\em Proceedings of the Logic at Work conference}, 1996.

\bibitem[Bel82]{belnap1982}
Nuel~D Belnap.
\newblock Display logic.
\newblock {\em Journal of philosophical logic}, 11(4):375--417, 1982.

\bibitem[Cas06]{castellini06}
Claudio Castellini.
\newblock Automated reasoning in quantified modal and temporal logics.
\newblock {\em AI Communications}, 19(2):183--185, 2006.

\bibitem[Daw14]{dawson14}
Jeremy Dawson.
\newblock Mix-elimination for {S4}.
\newblock
  \url{http://users.cecs.anu.edu.au/~jeremy/isabelle/2005/seqms/S4ca.ML}, 2014.
\newblock Included in Isabelle code base.

\bibitem[DG00]{davoren-gore-aiml-2001}
Jennifer~M. Davoren and Rajeev Gor{\'{e}}.
\newblock Bimodal logics for reasoning about continuous dynamics.
\newblock In {\em Advances in Modal Logic 3, papers from the third conference
  on "Advances in Modal logic", held in Leipzig (Germany) in October 2000},
  pages 91--111, 2000.

\bibitem[DG10]{dawson-gore-generalised}
Jeremy~E. Dawson and Rajeev Gor{\'e}.
\newblock Generic methods for formalising sequent calculi applied to
  provability logic.
\newblock In {\em Proceedings of the 17th International Conference on Logic for
  Programming, Artificial Intelligence, and Reasoning}, LPAR'10, pages
  263--277, Berlin, Heidelberg, 2010. Springer-Verlag.

\bibitem[DSH93]{schroeder-heister}
Kosta Dosen and Peter Schroder-Heister, editors.
\newblock {\em Substructural Logics}.
\newblock Clarendon Press, 1993.
\newblock Studies in Logic and Computation 2.

\bibitem[Gen35]{gentzen-lk}
Gerhard Gentzen.
\newblock Untersuchungen \"uber das logische schlie\ss en.
\newblock {\em Mathematische Zeitschrift}, 39:176--210 and 405--431, 1935.

\bibitem[Gir87]{girard-linear-logic}
Jean{-}Yves Girard.
\newblock Linear logic.
\newblock {\em Theor. Comput. Sci.}, 50:1--102, 1987.

\bibitem[GL96]{Goubault96}
Jean Goubault-{L}arrecq.
\newblock On computational interpretations of the modal logic {S4}. {I.} cut
  elimination.
\newblock Technical report, Institut f\"ur Logik, Komplexit\"at und
  Deduktionssysteme, Universit\"at Karlsruhe, 1996.

\bibitem[Gor94]{gore94}
Rajeev Gor{\'e}.
\newblock Cut-free sequent and tableau systems for propositional diodorean
  modal logics.
\newblock {\em Studia Logica}, 53(3):433--457, 1994.

\bibitem[Gor09]{Gore09}
Rajeev Gor{\'e}.
\newblock Machine checking proof theory: An application of logic to logic.
\newblock In Ramaswamy Ramanujam and Sundar Sarukkai, editors, {\em ICLA},
  volume 5378 of {\em Lecture Notes in Computer Science}, pages 23--35.
  Springer, 2009.

\bibitem[GR08]{Gore08}
Rajeev Gor{\'e} and Revantha Ramanayake.
\newblock Valentini's cut-elimination for provability logic resolved.
\newblock In {\em Advances in Modal Logic}, volume~7, pages 67--86. College
  Publications, London, 2008.

\bibitem[Ind12]{indrzejczak12}
Andrzej Indrzejczak.
\newblock Cut-free hypersequent calculus for {S4.3}.
\newblock {\em Bulletin of the Section of Logic}, 41(1-2):89--104, 2012.

\bibitem[Min13]{mints-jaegerfest}
Grigori Mints.
\newblock Two examples of cut-elimination for non-classical logics.
\newblock talk at J\"agerFest, 2013.

\bibitem[MJCG93]{gordon-hol}
editors Michael J. C.~Gordon, Thomas F.~Melham.
\newblock {\em Introduction to HOL: A Theorem-proving Environment for
  Higher-Order Logic}.
\newblock Cambridge University Press, 1993.

\bibitem[Neg05]{Negri05}
Sara Negri.
\newblock Proof analysis in modal logic.
\newblock {\em Journal of Philosophical Logic}, 34(5-6):507--544, 2005.

\bibitem[NvP01]{Negri01}
Sara Negri and Jan von Plato.
\newblock {\em Structural proof theory}.
\newblock Cambridge University Press, 2001.

\bibitem[OM57]{ohnishi1957}
Masao Ohnishi and Kazuo Matsumoto.
\newblock Gentzen method in modal calculi.
\newblock {\em Osaka Mathematical Journal}, 9(2):113--130, 1957.

\bibitem[Pau94]{paulson-nipkow}
Lawrence Paulson.
\newblock {\em Isabelle: A Generic Theorem Prover}, volume 828.
\newblock LNCS, 1994.
\newblock (with a contribution by T. Nipkow).

\bibitem[Pfe95]{pfenning-structural-cut-elimination}
Frank Pfenning.
\newblock Structural cut elimination.
\newblock In {\em 10th Annual IEEE Symposium on Logic in Computer Science, San
  Diego, California, USA, June 26-29, 1995}, pages 156--166. IEEE Computer
  Society, 1995.

\bibitem[Shi91]{Shimura91}
Tatsuya Shimura.
\newblock Cut-free systems for the modal logic {S4.3} and {S4.3Grz}.
\newblock {\em Reports on Mathematical Logic}, 25:57--72, 1991.

\bibitem[Tew13]{tews-coq}
Hendrik Tews.
\newblock Formalizing cut elimination of coalgebraic logics in coq.
\newblock In {\em Automated Reasoning with Analytic Tableaux and Related
  Methods, TABLEAUX 2013}, volume 8123, pages 257--272. LNCS, 2013.

\bibitem[TN02]{Isabelle-hol}
Markus~Wenzel Tobias~Nipkow, Lawrence~Paulson.
\newblock {\em Isabelle/HOL. A Proof Assistant for Higher-Order Logic}, volume
  2283.
\newblock LNCS, 2002.

\bibitem[TS00]{troelstra-schwichtenberg-basic}
Anne Troelstra and Helmut Schwichtenberg.
\newblock {\em Basic Proof Theory}.
\newblock Cambridge University Press, 2000.

\end{thebibliography}
