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