
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Here begins the end matter

% \bibliographystyle{plain}

% \bibliography{../ce,/home/discus/disk1/rpg/bib/fm,/home/discus/disk1/rpg/bib/modal,/home/discus/disk1/rpg/bib/mtl,/home/discus/disk1/rpg/bib/logic,/home/discus/disk1/rpg/bib/tl,/home/discus/disk1/rpg/bib/paracon,/home/discus/disk1/rpg/bib/linear,/home/discus/disk1/rpg/bib/algebra,/home/discus/disk1/rpg/bib/relevant,/home/discus/disk1/rpg/bib/dl,/home/discus/disk1/rpg/bib/atp}

\begin{thebibliography}{10}

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

% % \bibitem{borisavljevic-dosen-petric-permuting-cut-with-contraction}
% % M Borisavljevic, K Dosen, and Z Petric.
% % \newblock On permuting cut with contraction.
% % \newblock {\em Mathematical Structures in Computer Science}, 10:99--136, 2000.

% % \bibitem{church-types}
% % A~Church.
% % \newblock A formulation of the simple theory of types.
% % \newblock {\em Journal of Symbolic Logic}, 5:56--68, 1940.

\bibitem{dawson-gore-embedding-comparing}
J~E Dawson and R Gor{\'e}.
\newblock Embedding display calculi into logical frameworks: Comparing {T}welf
  and {I}sabelle.
\newblock {\em ENTCS} 42, 89--103.
% %\newblock In C~Fidge (Ed), {\em Proc.\ CATS 2001}, {\em ENTCS}, 42:89--103,
% % \url{http://www.elsevier.nl/gej-ng/31/29/23/68/show/Products/notes/cover.htt},
% 2001. Elsevier.

\bibitem{dawson-gore-cut-admissibility}
J~E Dawson and R Gor{\'e}.
\newblock Formalised Cut Admissibility for Display Logic. 
\newblock In Proc.\ TPHOLS'02, LNCS 2410, 131--147, Springer, 2002.

% % \bibitem{dawson-gore-machine-checked-strong-normalisation}
% % Jeremy~E.~Dawson and Rajeev Gor{\'e}.
% % A New Machine-checked Proof of Strong Normalisation for Display Logic.
% % In Computing: The Australasian Theory Symposium, 2003, ENTCS 78, 16--35, Elsevier.

\bibitem{abella-gacek}
A~Gacek.
\newblock The Abella interactive theorem prover (system description)
\newblock In Proc.\ IJCAR 2008 LNCS~5195:154-161, Springer, 2008.

% \bibitem{HOL-introduction}
% M~J~C Gordon and T~F Melham.
% \newblock {\em Introduction to {HOL}: a Theorem Proving Environment for Higher
%   Order Logic}.
% \newblock Cambridge University Press, 1993.

\bibitem{gore-india}
R~Gor\'e.
Invited talk in the Third Indian Conference on Logic and its
Applications, Chennai, January 2009.

\bibitem{gr-valentini}
R~Gor\'e and R~Ramanayake.
Valentini's Cut-elimination for Provability Logic Resolved.
Proc.\ AiML 2008, pp 67-86, College Publications
\url{http://users.rsise.anu.edu.au/~rpg/publications.html}

% % \bibitem{gore-relalg}
% % R~Gor{\'{e}}.
% % \newblock Cut-free display calculi for relation algebras.
% % \newblock In Proc.\ CSL96, LNCS 1258, 198--210, Springer, 1997.

\bibitem{Lei81}
D~Leivant. 
\newblock On the Proof Theory of the Modal Logic for Arithmetic Provability.
Journal of Symbolic Logic, 46:531–538, 1981.

\bibitem{moen} 
A~Moen. 
\newblock The proposed algorithms for eliminating cuts in the
provability calculus GLS do not terminate. 
\newblock NWPT 2001, Norwegian Computing Center, 2001-12-10
  \url{http://publ.nr.no/3411}

% \bibitem{IsLogHOL}
% T Nipkow, L~C. Paulson, and M Wenzel.
% \newblock Isabelle's logics: {HOL}.
% \newblock Technical report.
% \newblock 15 February 2001, \texttt{doc/logics-HOL.dvi} in the Isabelle
%   distribution.

% \bibitem{isabelle-ref}
% L~C. Paulson.
% \newblock The {Isabelle} reference manual.
% \newblock Technical report.
% \newblock 15 February 2001, \texttt{doc/ref.dvi} in the Isabelle distribution.

\bibitem{pfenning-structural-lics94}
F Pfenning.
\newblock Structural cut elimination.
\newblock In {\em Proc.\ LICS 94}, 1994.

% \bibitem{pym-harland-uniform}
% D. Pym and J. Harland.
% \newblock A Uniform Proof-theoretic Investigation of Linear Logic Programming.
% \newblock J.\ of Logic and Computation 4:2:175-207, 1994.

\bibitem{twelf-system}
F~Pfenning and C~Schürmann. 
\newblock System description:
           Twelf --- a meta-logical framework for deductive systems. 
\newblock In Proc.\ CADE-16, pages 202--206, Springer-Verlag LNAI 1632.

\bibitem{Sol76}
R~M~Solovay. 
\newblock Provability Interpretations of Modal Logic. Israel Journal
of Mathematics, 25:287–304, 1976.

\bibitem{Val83}
S~Valentini. 
\newblock The Modal Logic of Provability: Cut-elimination. Journal of
Philosophical Logic, 12:471–476, 1983.

% \bibitem{wansing-displaying-modal-logic}
% H Wansing.
% \newblock {\em Displaying Modal Logic}, volume~3 of {\em Trends in Logic}.
% \newblock Kluwer Academic Publishers, Dordrecht, August 1998.

\end{thebibliography}

