On the elimination of quantifier-free cuts
When investigating the complexity of cut-elimination in first-order logic, a natural subproblem is the elimination of quantifier-free cuts. So far, the problem has only been considered in the context of general cut-elimination, and the upper bounds that have been obtained are essentially double exponential. In this note, we observe that a method due to Dale Miller can be applied to obtain an exponential upper bound. (C) 2011 Elsevier B.V. All rights reserved.
complexity cut-elimination herbrand's theorem