Geodesic
On cut-type rules for calculuses of general type
Zapiski Nauchnykh Seminarov POMI, Studies in constructive mathematics and mathematical logic. Part VI, Tome 40 (1974), pp. 63-76 
S. Yu. Maslov; S. A. Norgela. On cut-type rules for calculuses of general type. Zapiski Nauchnykh Seminarov POMI, Studies in constructive mathematics and mathematical logic. Part VI, Tome 40 (1974), pp. 63-76. http://geodesic.mathdoc.fr/item/ZNSL_1974_40_a8/
@article{ZNSL_1974_40_a8,
     author = {S. Yu. Maslov and S. A. Norgela},
     title = {On cut-type rules for calculuses of general type},
     journal = {Zapiski Nauchnykh Seminarov POMI},
     pages = {63--76},
     year = {1974},
     volume = {40},
     language = {ru},
     url = {http://geodesic.mathdoc.fr/item/ZNSL_1974_40_a8/}
}
TY  - JOUR
AU  - S. Yu. Maslov
AU  - S. A. Norgela
TI  - On cut-type rules for calculuses of general type
JO  - Zapiski Nauchnykh Seminarov POMI
PY  - 1974
SP  - 63
EP  - 76
VL  - 40
UR  - http://geodesic.mathdoc.fr/item/ZNSL_1974_40_a8/
LA  - ru
ID  - ZNSL_1974_40_a8
ER  - 
%0 Journal Article
%A S. Yu. Maslov
%A S. A. Norgela
%T On cut-type rules for calculuses of general type
%J Zapiski Nauchnykh Seminarov POMI
%D 1974
%P 63-76
%V 40
%U http://geodesic.mathdoc.fr/item/ZNSL_1974_40_a8/
%G ru
%F ZNSL_1974_40_a8

Voir la notice du chapitre de livre provenant de la source Math-Net.Ru

The problem of the cut-elimination for calculuses of general type is formulated as the problem of strict representability by means of Post canonical systems satisfying the additional requirement: each word can be a conclusion only of a finite member of applications of rules. Possibilities of elimination and of algorithmic elimination of cut-type rules are studied.