Geodesic
On the recognition of the tautological nature of propositional formulas
Zapiski Nauchnykh Seminarov POMI, Studies in constructive mathematics and mathematical logic. Part VII, Tome 60 (1976), pp. 197-206 
P. Yu. Suvorov. On the recognition of the tautological nature of propositional formulas. Zapiski Nauchnykh Seminarov POMI, Studies in constructive mathematics and mathematical logic. Part VII, Tome 60 (1976), pp. 197-206. http://geodesic.mathdoc.fr/item/ZNSL_1976_60_a14/
@article{ZNSL_1976_60_a14,
     author = {P. Yu. Suvorov},
     title = {On the recognition of the tautological nature of propositional formulas},
     journal = {Zapiski Nauchnykh Seminarov POMI},
     pages = {197--206},
     year = {1976},
     volume = {60},
     language = {ru},
     url = {http://geodesic.mathdoc.fr/item/ZNSL_1976_60_a14/}
}
TY  - JOUR
AU  - P. Yu. Suvorov
TI  - On the recognition of the tautological nature of propositional formulas
JO  - Zapiski Nauchnykh Seminarov POMI
PY  - 1976
SP  - 197
EP  - 206
VL  - 60
UR  - http://geodesic.mathdoc.fr/item/ZNSL_1976_60_a14/
LA  - ru
ID  - ZNSL_1976_60_a14
ER  - 
%0 Journal Article
%A P. Yu. Suvorov
%T On the recognition of the tautological nature of propositional formulas
%J Zapiski Nauchnykh Seminarov POMI
%D 1976
%P 197-206
%V 60
%U http://geodesic.mathdoc.fr/item/ZNSL_1976_60_a14/
%G ru
%F ZNSL_1976_60_a14

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

A formal language whose propositions express (in some sense) the properties of propositional formulas is described in the paper. For a certain subset of propositions of this language it is proved that each of them defines a class of propositional formulas, on which it is possible to recognize the tautological nature in a time polynomially dependent on the formula's length.