title: On the elimination of quantifier-free cuts.
abstract: 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.
authors.affiliation: Institute of Computer Languages (E185), Vienna University of Technology, Favoritenstraße 9, 1040 Vienna, Austria.
authors.forename: Daniel
authors.initials: D
authors.lastname: Weller