<p>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.</p>

<p>Given the statement <span class="math-container">$$p \wedge q$$</span> we can ask whether it is true in the model <span class="math-container">$\{p=\top,q=\bot\}$</span> (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).</p>

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

CC BY-SA 4.0
2020-05-29T01:09:25.350Z
2020-05-29T01:09:25.350Z
selig
<p>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.</p>

CC BY-SA 4.0
2020-04-17T07:14:01.137Z
Do you understand the difference between the *satisfaction* relation and the *validity* relation for logical formulae?
Martin Berger
CC BY-SA 4.0
2020-04-17T18:40:44.337Z
Satisfiability, true in 1 interpretation compared to validity, true in all interpretations?
Ilk
CC BY-SA 4.0
2020-04-18T06:43:27.000Z
Not *satisfiability*, but *satisfaction*. A [model checker](https://en.wikipedia.org/wiki/Model_checking) 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.
Emil Jeřábek
<reference-request><automated-theorem-proving><model-checking>
Automatic theorem prover for first-order logic versus model checker
Ilk
# Automatic theorem prover for first-order logic versus model checker

(Asked by: username_0 on 2020-04-15)

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.

**Tags:** reference-request, automated-theorem-proving, model-checking
> **Comments:**
> **username_1**: Do you understand the difference between the *satisfaction* relation and the *validity* relation for logical formulae?  
> **username_0**: Satisfiability, true in 1 interpretation compared to validity, true in all interpretations?  
> **username_2**: Not *satisfiability*, but *satisfaction*. A [model checker](https://en.wikipedia.org/wiki/Model_checking) 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.  

---

## 1 answers

### Answer by username_3 on 2020-05-29. Score: 3 | Accepted answer

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.


---

