Structure of proofs and the complexity of cut elimination

DOI10.1016/j.tcs.2005.07.042zbMath1088.03046OpenAlexW1968209456MaRDI QIDQ2368983

Wen-Hui Zhang

Publication date: 28 April 2006

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

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

zbMATH Keywords

Proof complexityCut eliminationBalanced proofsProof structure

Mathematics Subject Classification ID

Cut-elimination and normal-form theorems (03F05) Structure of proofs (03F07) Complexity of proofs (03F20)

Related Items

Sharpened lower bounds for cut elimination

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Linear logic
• Don't eliminate cut
• Duplication of directed graphs and exponential blow up of proofs
• Cut elimination and automatic proof procedures
• Depth of proofs, depth of cut-formulas and complexity of cut formulas
• Focussing and proof construction
• Locus Solum: From the rules of logic to the logic of rules
• Logic Programming with Focusing Proofs in Linear Logic
• Bounds for proof-search and speed-up in the predicate calculus
• A new deconstructive logic: linear logic
• From Foundations to Ludics
• Computer Science Logic
• Asymptotic cyclic expansion and bridge groups of formal proofs