Corrected upper bounds for free-cut elimination

DOI10.1016/j.tcs.2011.05.053zbMath1267.03053OpenAlexW2008575211MaRDI QIDQ719283

Arnold Beckmann, Samuel R. Buss

Publication date: 10 October 2011

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.tcs.2011.05.053

zbMATH Keywords

upper boundscut eliminationsequent calculusfree cut

Mathematics Subject Classification ID

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

Related Items

Logic and majority voting, Sharpened lower bounds for cut elimination, Collapsing modular counting in bounded arithmetic and constant depth propositional proofs, Propositional proofs and reductions between NP search problems, Improved witnessing and local improvement principles for second-order bounded arithmetic

Uses Software

• Pesca

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Upper bound on the lengthening of proofs by cut elimination
• Proof theory. 2nd ed
• Cut elimination and automatic proof procedures
• The role of quantifier alternations in cut elimination
• A Conservation Result Concerning Bounded Theories and the Collection Axiom
• Cut Elimination in the Presence of Axioms
• Computer Science Logic
• On n-quantifier induction
• Cut-elimination and redundancy-elimination by resolution