Affordable Access

Publisher Website

On the elimination of quantifier-free cuts

Authors
Journal
Theoretical Computer Science
0304-3975
Publisher
Elsevier
Publication Date
Volume
412
Issue
49
Identifiers
DOI: 10.1016/j.tcs.2011.08.035
Keywords
  • Cut-Elimination
  • Complexity
  • Herbrand’S Theorem

Abstract

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.

There are no comments yet on this publication. Be the first to share your thoughts.