Geodesic
Two tautologihood proof systems based on the split method
Zapiski Nauchnykh Seminarov POMI, Theoretical application of methods of mathematical logic. Part III, Tome 105 (1981), pp. 24-44 
E. Ya. Dantsin. Two tautologihood proof systems based on the split method. Zapiski Nauchnykh Seminarov POMI, Theoretical application of methods of mathematical logic. Part III, Tome 105 (1981), pp. 24-44. http://geodesic.mathdoc.fr/item/ZNSL_1981_105_a4/
@article{ZNSL_1981_105_a4,
     author = {E. Ya. Dantsin},
     title = {Two tautologihood proof systems based on the split method},
     journal = {Zapiski Nauchnykh Seminarov POMI},
     pages = {24--44},
     year = {1981},
     volume = {105},
     language = {ru},
     url = {http://geodesic.mathdoc.fr/item/ZNSL_1981_105_a4/}
}
TY  - JOUR
AU  - E. Ya. Dantsin
TI  - Two tautologihood proof systems based on the split method
JO  - Zapiski Nauchnykh Seminarov POMI
PY  - 1981
SP  - 24
EP  - 44
VL  - 105
UR  - http://geodesic.mathdoc.fr/item/ZNSL_1981_105_a4/
LA  - ru
ID  - ZNSL_1981_105_a4
ER  - 
%0 Journal Article
%A E. Ya. Dantsin
%T Two tautologihood proof systems based on the split method
%J Zapiski Nauchnykh Seminarov POMI
%D 1981
%P 24-44
%V 105
%U http://geodesic.mathdoc.fr/item/ZNSL_1981_105_a4/
%G ru
%F ZNSL_1981_105_a4

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

Two systems for generating of all propositional tautologies and only them are considered. In every of these calculuses there are one axiom and one rule of inference. Proofs for tautologies of many well-known classes with polinomial time recognition algorithm have linear length in these systems. Various formulae's characteristics that influence on length of proofs are studied (one of them is a symmetry of formulae).