The Role of Quantifier Alternations in Cut Elimination
Philipp Gerhardy · Notre Dame Journal of Formal Logic · 2005
Extending previous results from work on the complexity of cut elimination for the sequent calculus LK, we discuss the role of quantifier alternations and develop a measure to describe the complexity of cut elimination in terms of quantifier alternations in cut formulas and contractions on such formulas.