Automata are used for an algorithmic approach to logical decision problems, in particular the satisfiability problem: does a given φ have a model? Other equally fundamental problems like the validity problem (is a given formula φ true in all possible interpretations?) or the equivalence problem (do two given formulas φ and ψ express the same property?) can easily be reduced to the satisfiability problem, at least when the logic provides negation.