Aussagenlogik/Tautologien/Entscheidungsverfahren/Fakt

Es gibt ein algorithmisches Verfahren (ein „Entscheidungsverfahren“), das für einen gegebenen Ausdruck entscheidet, ob es sich um eine Tautologie handelt oder nicht.