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.
3
-
1$\begingroup$ Do you understand the difference between the satisfaction relation and the validity relation for logical formulae? $\endgroup$– Martin BergerApr 17, 2020 at 7:14
-
$\begingroup$ Satisfiability, true in 1 interpretation compared to validity, true in all interpretations? $\endgroup$– NiftApr 17, 2020 at 18:40
-
3$\begingroup$ 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. $\endgroup$– Emil JeřábekApr 18, 2020 at 6:43
Add a comment
|
1 Answer
$\begingroup$
$\endgroup$
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.
