scientific article

zbMath0429.03033MaRDI QIDQ3866101

V. P. Orevkov

Publication date: 1979

Full work available at URL: https://eudml.org/doc/67048

Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.

zbMATH Keywords

cut-eleminationlower bounds for proof length

Mathematics Subject Classification ID

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

Related Items

On the generation of quantified lemmas, Algorithmic introduction of quantified cuts, On feasible numbers, Upper and lower bounds for the height of proofs in sequent calculus for intuitionistic logic, On the compressibility of finite languages and formal proofs, Classical logic with partial functions, Non-elementary speed-ups in proof length by different variants of classical analytic calculi, Non-elementary speed-ups in logic calculi, Refinement of bounds of the height of terms in the most general unifier, Sufficient conditions for cut elimination with complexity analysis, Extracting Herbrand disjunctions by functional interpretation, A complexity analysis of functional interpretations, On the form of witness terms, Some pitfalls of LK-to-LJ translations and how to avoid them, Compressibility of Finite Languages by Grammars