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.

Statistics

Seen <100 times
0 Comments