Structure of proofs and the complexity of cut elimination

DOI10.1016/J.TCS.2005.07.042MaRDI QIDQ2368983zbMATH OpenOpenAlexFDO

Authors Wenhui 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

Balanced proofsCut eliminationProof complexityProof structure

Mathematics Subject Classification ID

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

Recommendations

• Proof Complexity of the Cut-free Calculus of Structures
• scientific article; zbMATH DE number 515726
• Cut-elimination and proof schemata
• On the complexity of cutting-plane proofs
• scientific article; zbMATH DE number 1088197
• Upper bound on the lengthening of proofs by cut elimination
• Cut normal forms and proof complexity
• scientific article; zbMATH DE number 4087657
• On the complexity of cutting-plane proofs using split cuts
• Depth of proofs, depth of cut-formulas and complexity of cut formulas

Cites work

• A direct proof of the equivalence between Brouwer's fan theorem and König's lemma with a uniqueness hypothesis
• A new deconstructive logic: linear logic
• Asymptotic cyclic expansion and bridge groups of formal proofs
• Bounds for proof-search and speed-up in the predicate calculus
• Computer Science Logic
• Cut elimination and automatic proof procedures
• Depth of proofs, depth of cut-formulas and complexity of cut formulas
• Don't eliminate cut
• Duplication of directed graphs and exponential blow up of proofs
• Focussing and proof construction
• From Foundations to Ludics
• scientific article; zbMATH DE number 1670856 (Why is no real title available?)
• scientific article; zbMATH DE number 4209572 (Why is no real title available?)
• scientific article; zbMATH DE number 1948160 (Why is no real title available?)
• scientific article; zbMATH DE number 2043517 (Why is no real title available?)
• Linear logic
• Locus solum: From the rules of logic to the logic of rules.
• Logic Programming with Focusing Proofs in Linear Logic

Cited in

(16)

• Algebraic aspects of cut elimination
• Sufficient conditions for cut elimination with complexity analysis
• Sharpened lower bounds for cut elimination
• scientific article; zbMATH DE number 6680140 (Why is no real title available?)
• scientific article; zbMATH DE number 7447752 (Why is no real title available?)
• Unwinding a Non-effective Cut Elimination Proof
• scientific article; zbMATH DE number 4087657 (Why is no real title available?)
• Input Proofs and Rank One Cutting Planes
• scientific article; zbMATH DE number 515726 (Why is no real title available?)
• scientific article; zbMATH DE number 1086658 (Why is no real title available?)
• scientific article; zbMATH DE number 6829289 (Why is no real title available?)
• Cut-Elimination for SBL
• scientific article; zbMATH DE number 7178366 (Why is no real title available?)
• Computer Science Logic
• Cut formulas in propositional logic
• On the complexity of cutting-plane proofs using split cuts

This page was built for publication: Structure of proofs and the complexity of cut elimination

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