# 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.

• Do you understand the difference between the satisfaction relation and the validity relation for logical formulae? Apr 17 '20 at 7:14
• Satisfiability, true in 1 interpretation compared to validity, true in all interpretations?
– Nift
Apr 17 '20 at 18:40
• Not satisfiability, but satisfaction. A model checker takes a formula and a model, and checks whether the formula holds in that particular model. That’s completely different from checking validity in all models. Apr 18 '20 at 6:43

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).