Cut normal forms and proof complexity

DOI10.1016/S0168-0072(98)00026-8MaRDI QIDQ1302302zbMATH OpenFDO

Authors Matthias Baaz, Alexander Leitsch

Publication date 24 July 2000

Published in Annals of Pure and Applied Logic (Search for Journal in Brave)

zbMATH Keywords

cut-eliminationcut normal formsequational sequentsnon-elementary complexitynon-monotone cuts

Mathematics Subject Classification ID

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

Recommendations

• Publication:4453638
• Cut Elimination In Situ
• Publication:4436026
• On the elimination of quantifier-free cuts
• Algorithmic introduction of quantified cuts

Cites work

• scientific article; zbMATH DE number 3687363 (Why is no real title available?)
• scientific article; zbMATH DE number 627412 (Why is no real title available?)
• scientific article; zbMATH DE number 1086658 (Why is no real title available?)
• A direct proof of the equivalence between Brouwer's fan theorem and König's lemma with a uniqueness hypothesis
• Lower Bounds on Herbrand's Theorem
• Lower bounds for increasing complexity of derivations after cut elimination
• Proof theory. 2nd ed

Cited in

(20)

• Unsound inferences make proofs shorter
• 2000 Annual Meeting of the Association for Symbolic Logic
• Cut-elimination and redundancy-elimination by resolution
• CERES: An analysis of Fürstenberg's proof of the infinity of primes
• Towards a clausal analysis of cut-elimination
• scientific article; zbMATH DE number 2006630 (Why is no real title available?)
• Sharpened lower bounds for cut elimination
• Proof Transformations and Structural Invariance
• Describing proofs by short tautologies
• Structure of proofs and the complexity of cut elimination
• Herbrand's theorem and term induction
• A Clausal Approach to Proof Analysis in Second-Order Logic
• Expansion trees with cut
• Sufficient conditions for cut elimination with complexity analysis
• Herbrand Sequent Extraction
• On the complexity of proof deskolemization
• scientific article; zbMATH DE number 2051382 (Why is no real title available?)
• Effective Skolemization
• On the computational complexity of cut-reduction
• scientific article; zbMATH DE number 1086658 (Why is no real title available?)

This page was built for publication: Cut normal forms and proof complexity

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