On the computational complexity of cut-reduction

DOI10.1016/J.APAL.2009.06.004MaRDI QIDQ636310zbMATH OpenOpenAlexFDO

Authors Klaus Aehlig, Arnold Beckmann

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) Complexity of proofs (03F20) First-order arithmetic and fragments (03F30)

Recommendations

• The computational content of arithmetical proofs
• Sharpened lower bounds for cut elimination
• Uniform Proof Complexity
• Cut normal forms and proof complexity
• Lower bounds for resolution and cutting plane proofs and monotone computations

Cites work

• scientific article; zbMATH DE number 3912375 (Why is no real title available?)
• scientific article; zbMATH DE number 4059391 (Why is no real title available?)
• scientific article; zbMATH DE number 3497842 (Why is no real title available?)
• scientific article; zbMATH DE number 1088186 (Why is no real title available?)
• scientific article; zbMATH DE number 819737 (Why is no real title available?)
• scientific article; zbMATH DE number 2196511 (Why is no real title available?)
• scientific article; zbMATH DE number 3327279 (Why is no real title available?)
• A syntactical analysis of non-size-increasing polynomial time computation
• An Application of Boolean Complexity to Separation Problems in Bounded Arithmetic
• Beweistheoretische Erfassung der unendlichen Induktion in der Zahlentheorie
• Continuous normalization for the lambda-calculus and Gödel's T
• Dynamic ordinal analysis
• Exact bounds for lengths of reductions in typed \(\lambda\)-calculus
• Finite investigations of transfinite derivations
• Fragments of Bounded Arithmetic and Bounded Query Classes
• Generalised dynamic ordinals -- universal measures for implicit computational complexity
• How easy is local search?
• Notation systems for infinitary derivations
• Structure and definability in general bounded arithmetic theories
• Untersuchungen über das logische Schliessen. I
• Untersuchungen über das logische Schliessen. II
• ÜBER EINE BISHER NOCH NICHT BENÜTZTE ERWEITERUNG DES FINITEN STANDPUNKTES

Cited in

(13)

• The computational complexity of disconnected cut and \(2 K_2\)-partition
• scientific article; zbMATH DE number 6829289 (Why is no real title available?)
• Cut-elimination and redundancy-elimination by resolution
• scientific article; zbMATH DE number 5999585 (Why is no real title available?)
• On the complexity of slice functions
• Mathematical logic: proof theory, constructive mathematics. Abstracts from the workshop held November 12--17, 2023
• Computer Science Logic
• Sharpened lower bounds for cut elimination
• A Characterisation of Definable NP Search Problems in Peano Arithmetic
• Computing circumscription revisited: A reduction algorithm
• Sufficient conditions for cut elimination with complexity analysis
• Polynomial local search in the polynomial hierarchy and witnessing in fragments of bounded arithmetic
• On the complexity of finding balanced oneway cuts

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q636310)