Получение всех пропозициональных тавтологий

[nikov]

Нужно написать программу, которая будет печатать бесконечный список всех пропозициональных тавтологий (наподобие $A \rightarrow A$). Причем нужно исключить случаи, когда очередная тавтология является частным случаем предыдущей (то есть получается из нее подстановкой каких-либо пропозициональных формул вместо пропозициональных переменных, например после $A \rightarrow A$ не должно быть напечатано $B \rightarrow B$ или $(A \rightarrow B) \rightarrow (A \rightarrow B)$.
Я написал один вариант, но он работает медленно (точнее, с постепенным замедлением) из-за того, что каждая полученная формула проверяется на то, не является ли она частным случаем каждой из предыдущих. За день программа может напечатать всего около 10 тысяч тавтологий.
Интересует, существуют ли быстрые алгоритмы для этой задачи.