Geodesic
Upper and lower bounds on the height of proofs in sequent calculus for intuitionistic logic
Zapiski Nauchnykh Seminarov POMI, Combinatorics and graph theory. Part XII, Tome 497 (2020), pp. 124-169

Voir la notice de l'article provenant de la source Math-Net.Ru

We prove upper and lower bounds on the height of proofs in sequent calculus for intuitionistic logic for the case when cut formulas may only contain essentially positive occurrences of the existential quantifier. We consider the cases of both proofs with and proofs without function symbols. 
@article{ZNSL_2020_497_a5,
     author = {V. P. Orevkov},
     title = {Upper and lower bounds on the height of proofs in sequent calculus for intuitionistic logic},
     journal = {Zapiski Nauchnykh Seminarov POMI},
     pages = {124--169},
     publisher = {mathdoc},
     volume = {497},
     year = {2020},
     language = {ru},
     url = {http://geodesic.mathdoc.fr/item/ZNSL_2020_497_a5/}
}
TY  - JOUR
AU  - V. P. Orevkov
TI  - Upper and lower bounds on the height of proofs in sequent calculus for intuitionistic logic
JO  - Zapiski Nauchnykh Seminarov POMI
PY  - 2020
SP  - 124
EP  - 169
VL  - 497
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/ZNSL_2020_497_a5/
LA  - ru
ID  - ZNSL_2020_497_a5
ER  - 
%0 Journal Article
%A V. P. Orevkov
%T Upper and lower bounds on the height of proofs in sequent calculus for intuitionistic logic
%J Zapiski Nauchnykh Seminarov POMI
%D 2020
%P 124-169
%V 497
%I mathdoc
%U http://geodesic.mathdoc.fr/item/ZNSL_2020_497_a5/
%G ru
%F ZNSL_2020_497_a5
V. P. Orevkov. Upper and lower bounds on the height of proofs in sequent calculus for intuitionistic logic. Zapiski Nauchnykh Seminarov POMI, Combinatorics and graph theory. Part XII, Tome 497 (2020), pp. 124-169. http://geodesic.mathdoc.fr/item/ZNSL_2020_497_a5/