О распознавании тавтологичности пропозициональных формул

В работе описан формальный язык, предложения которого выражают (в некотором смысле) свойства пропозициональных формул.
Для некоторого подмножества предложений этого языка доказано, что каждое из них определяет класс пропозициональных формул, на котором возможно распознавание тавтологичности за время, полиномиально зависящее от длины формулы. Библ. 3 назв.