Cut normal forms and proof complexity

DOI10.1016/S0168-0072(98)00026-8zbMath0940.03062MaRDI QIDQ1302302

Alexander Leitsch, Matthias Baaz

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)

Related Items (15)

2000 Annual Meeting of the Association for Symbolic Logic ⋮ Sharpened lower bounds for cut elimination ⋮ On the complexity of proof deskolemization ⋮ Effective Skolemization ⋮ UNSOUND INFERENCES MAKE PROOFS SHORTER ⋮ Towards a clausal analysis of cut-elimination ⋮ Sufficient conditions for cut elimination with complexity analysis ⋮ CERES: An analysis of Fürstenberg's proof of the infinity of primes ⋮ Cut-elimination and redundancy-elimination by resolution ⋮ Proof Transformations and Structural Invariance ⋮ Herbrand's theorem and term induction ⋮ A Clausal Approach to Proof Analysis in Second-Order Logic ⋮ Describing proofs by short tautologies ⋮ Expansion trees with cut ⋮ Herbrand Sequent Extraction

Cites Work

• Proof theory. 2nd ed
• Lower bounds for increasing complexity of derivations after cut elimination
• Lower Bounds on Herbrand's Theorem
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

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