On the computational complexity of cut-reduction

DOI10.1016/j.apal.2009.06.004zbMath1223.03042OpenAlexW2046382802MaRDI QIDQ636310

Arnold Beckmann, Klaus Aehlig

Publication date: 26 August 2011

Published in: Annals of Pure and Applied Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.apal.2009.06.004

zbMATH Keywords

bounded arithmeticcut-eliminationdefinable functionsnotation systems

Mathematics Subject Classification ID

Cut-elimination and normal-form theorems (03F05) First-order arithmetic and fragments (03F30) Complexity of proofs (03F20)

Related Items

POLYNOMIAL LOCAL SEARCH IN THE POLYNOMIAL HIERARCHY AND WITNESSING IN FRAGMENTS OF BOUNDED ARITHMETIC ⋮ A Characterisation of Definable NP Search Problems in Peano Arithmetic

Cites Work

• How easy is local search?
• Structure and definability in general bounded arithmetic theories
• Finite investigations of transfinite derivations
• Dynamic ordinal analysis
• Continuous normalization for the lambda-calculus and Gödel's T
• Untersuchungen über das logische Schliessen. I
• Untersuchungen über das logische Schliessen. II
• Notation systems for infinitary derivations
• Beweistheoretische Erfassung der unendlichen Induktion in der Zahlentheorie
• Exact bounds for lengths of reductions in typed λ-calculus
• Fragments of Bounded Arithmetic and Bounded Query Classes
• ÜBER EINE BISHER NOCH NICHT BENÜTZTE ERWEITERUNG DES FINITEN STANDPUNKTES
• An Application of Boolean Complexity to Separation Problems in Bounded Arithmetic
• A syntactical analysis of non-size-increasing polynomial time computation
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: On the computational complexity of cut-reduction