|
Zapiski Nauchnykh Seminarov LOMI, 1984, Volume 137, Pages 87–98
(Mi znsl4788)
|
|
|
|
This article is cited in 1 scientific paper (total in 1 paper)
Upper bounds for lengthening of proofs after cut-elimination
V. P. Orevkov
Abstract:
Define $2_i^n$ by $2_0^n=n$ and $2_{i+1}^n=2^{2_i^n}$. Let $\mathcal D$ be derivation tree of a sequent $S$ in the Gentzen-style calculus for the classical or intuitionistic first-order logic. The main result of the paper: There is a cut-free proof $\mathcal D'$ of $S$ such that the height of $\mathcal D'$ is less than $2^h_l$, where $h$ is the height of $\mathcal D$ and $l$ is the number of different sequents in $\mathcal D$.
Citation:
V. P. Orevkov, “Upper bounds for lengthening of proofs after cut-elimination”, Computational complexity theory. Part II, Zap. Nauchn. Sem. LOMI, 137, "Nauka", Leningrad. Otdel., Leningrad, 1984, 87–98
Linking options:
https://www.mathnet.ru/eng/znsl4788 https://www.mathnet.ru/eng/znsl/v137/p87
|
|