scientific article; zbMATH DE number 1086658

MaRDI QIDQ4362908zbMATH OpenFDO

Authors Matthias Baaz, Alexander Leitsch

Publication date 14 June 1998

zbMATH Keywords

cut-projectionexponential boundsfast cut eliminationKalmar elementary boundSkolemizationStatman's sequence of sequents

Mathematics Subject Classification ID

Cut-elimination and normal-form theorems (03F05) Complexity of proofs (03F20) Complexity classes (hierarchies, relations among complexity classes, etc.) (68Q15)

Recommendations

• Cut normal forms and proof complexity
• Fast cut-elimination by CERES
• Gentzen systems, resolution, and literal trees
• Structure of proofs and the complexity of cut elimination
• Algorithmic introduction of quantified cuts
• On permuting cut with contraction
• Structural cut elimination. I: Intuitionistic and classical logic
• scientific article; zbMATH DE number 1748575
• A sequent calculus with implicit term representation
• Duplication of directed graphs and exponential blow up of proofs

Cited in

(4)

• Cut normal forms and proof complexity
• Efficient elimination of Skolem functions in \(\text{LK}^\text{h} \)
• scientific article; zbMATH DE number 2051382 (Why is no real title available?)
• Towards Hilbert's 24th Problem: Combinatorial Proof Invariants

This page was built for publication:

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