M. Baaz, A. Leitsch:
"Towards a clausal analysis of cut-elimination";
Journal of Symbolic Computation, 41 (2006), 381 - 410.
Clausal Analysis of Cut-elimination
Klausale Analyse der Schnitt-elimination
http://aleph.ub.tuwien.ac.at/F?base=tuw01&func=find-c&ccl_term=AC06587870