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

Voir la notice de l'article 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). 
@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},
     publisher = {mathdoc},
     volume = {105},
     year = {1981},
     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
PB  - mathdoc
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
%I mathdoc
%U http://geodesic.mathdoc.fr/item/ZNSL_1981_105_a4/
%G ru
%F ZNSL_1981_105_a4
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/