Sharpened lower bounds for cut elimination

DOI10.2178/jsl/1333566644zbMath1270.03118OpenAlexW2002681112MaRDI QIDQ2892684

Samuel R. Buss

Publication date: 19 June 2012

Published in: The Journal of Symbolic Logic (Search for Journal in Brave)

Full work available at URL: https://projecteuclid.org/euclid.jsl/1333566644

zbMATH Keywords

cut eliminationlower bounds

Mathematics Subject Classification ID

Cut-elimination and normal-form theorems (03F05)

Cites Work

• Corrected upper bounds for free-cut elimination
• Upper bound on the lengthening of proofs by cut elimination
• Lower bounds for increasing complexity of derivations after cut elimination
• Cut elimination and automatic proof procedures
• The computational complexity of logical theories
• Cut normal forms and proof complexity
• Depth of proofs, depth of cut-formulas and complexity of cut formulas
• Structure of proofs and the complexity of cut elimination
• The quantifier complexity of polynomial-size iterated definitions in first-order logic
• Unnamed Item
• Unnamed Item
• Unnamed Item