this directory contains assorted contributions towards the paper
Machine-checked Cut-Admissibility for Propositional Modal Logics
by Jeremy Dawson, Rajeev Gor\'e and Jesse Wu

Each has been divided into multiple LaTeX files to facilitate combining them;
but they still need to be massaged to make a coherent whole

by Jeremy Dawson
mints.tex:\input{gtd}
mints.tex:\input{s4c}

by Jesse Wu
jesse.tex:\input{jesse-intro}
jesse.tex:\input{s4}
jesse.tex:\input{s43}

from Gore and Dawson, GLS, LPAR 2010
formalisedprooftheory.tex:\input{gls}
formalisedprooftheory.tex:\input{refs}