Aussagenlogik/Tautologien/Entscheidungsverfahren/Fakt

Es gibt ein algorithmisches Verfahren (ein „Entscheidungsverfahren“), das für einen gegebenen Ausdruck ${}\alpha \in L^{V}$ entscheidet, ob es sich um eine Tautologie handelt oder nicht.