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

% \bibliographystyle{plain}

% \bibliography{root}

\begin{thebibliography}{10}

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

\bibitem{brotherston-gore-interpolation}
\newblock James Brotherston \& Rajeev Gor\'e.
\newblock Craig Interpolation in Displayable Logics
\newblock In {\em Proceedings of {TABLEAUX-20}}, LNAI, pages 88--103. Springer,
  2011.

\bibitem{Caniart:10}
Nicolas Caniart.
\newblock {\sc Merit}: an interpolating model-checker.
\newblock In {\em Proceedings of CAV-22}, volume 6174 of {\em LNCS}, pages
  162--166. Springer, 2010.

\bibitem{Craig:57-2}
William Craig.
\newblock Three uses of the {H}erbrand-{G}entzen theorem in relating model
  theory and proof theory.
\newblock {\em Journal of Symbolic Logic}, 22(3):269--285, 1957.

\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-gls}
J~E Dawson and R Gor{\'e}.
\newblock Generic Methods for Formalising Sequent Calculi
       Applied to Provability Logic.
\newblock In Proc.\ Logic for Programming, Artificial Intelligence and
Reasoning (LPAR 2010), LNCS 6397, 263-277. 

\bibitem{Feferman:08}
Solomon Feferman.
\newblock Harmonious logic: {C}rai{g’s} interpolation theorem and its
  descendants.
\newblock {\em Synthese}, 164:341--357, 2008.

\bibitem{gore-india}
R~Gor\'e. Machine Checking Proof Theory: An Application of Logic to Logic.
Invited talk, Third Indian Conference on Logic and
Applications, Chennai, January 2009.

\bibitem{McMillan:08}
Kenneth~L. McMillan.
\newblock Quantified invariant generation using an interpolating saturation
  prover.
\newblock In {\em Proceedings of {TACAS}-14}, volume 4963 of {\em LNCS}, pages
  413--427, 2008.

\end{thebibliography}

