Automatic theorem prover for first-order logic versus model checker What's the formal difference between a model checker, and an automated theorem prover for first-order logic, i.e. something like Meson/Metis/Sledgehammer/Vampire/E? Link to a clear discussion of the difference is preferred.
To add to the answer in the comments, it might help to first ask what the difference is between a model checker and an automated theorem prover for propositional logic.

Given the statement $$p \wedge q$$ we can ask whether it is true in the model $\{p=\top,q=\bot\}$ (model checking) or we can ask whether it is true in all models (theorem proving). We can also ask whether it is true in some models (satisfiability checking).

The same concepts follow over to first-order logic. For model checking we need a model; for theorem proving we don't.