for testing whether a given formula is always satisfied (equiv., whether its negation is unsatisfiable).

The definition of tautology can be extended to sentences in predicate logic, which may contain quantifiers--a feature absent from sentences of propositional logic. Indeed, in propositional logic, there is no distinction between a tautology and a logically valid formula. In the context of predicate