Upper bound on the lengthening of proofs by cut elimination

DOI10.1007/BF01095640zbMath0595.03050MaRDI QIDQ1077414

V. P. Orevkov

Publication date: 1986

Published in: Journal of Soviet Mathematics (Search for Journal in Brave)

zbMATH Keywords

cut-free proofpredicatesintuitionistic predicate calculusclassical sequential calculus ofderivation-tree of a sequent

Mathematics Subject Classification ID

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

Related Items (2)

Sharpened lower bounds for cut elimination ⋮ Corrected upper bounds for free-cut elimination

Cites Work

• Bounds for proof-search and speed-up in the predicate calculus

This page was built for publication: Upper bound on the lengthening of proofs by cut elimination