On the elimination of quantifier-free cuts
Copyright policy )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.
- TU Wien Austria
Herbrand’s theorem, cut-elimination, Complexity, Classical first-order logic, Article, Theoretical Computer Science, Herbrand's theorem, quantifier-free cuts, exponential upper bound, Cut-elimination, Cut-elimination and normal-form theorems, complexity, first-order logic, Computer Science(all)
Herbrand’s theorem, cut-elimination, Complexity, Classical first-order logic, Article, Theoretical Computer Science, Herbrand's theorem, quantifier-free cuts, exponential upper bound, Cut-elimination, Cut-elimination and normal-form theorems, complexity, first-order logic, Computer Science(all)
selected citations These citations are derived from selected sources.This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).3 popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network.Average influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).Top 10% impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network.Average
Citations provided by BIP!Popularity provided by BIP!