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.

  • 1
    $\begingroup$ Do you understand the difference between the satisfaction relation and the validity relation for logical formulae? $\endgroup$ Apr 17 '20 at 7:14
  • $\begingroup$ Satisfiability, true in 1 interpretation compared to validity, true in all interpretations? $\endgroup$
    – Nift
    Apr 17 '20 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$ Apr 18 '20 at 6:43

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.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.