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$ – Martin Berger Apr 17 at 7:14
  • $\begingroup$ Satisfiability, true in 1 interpretation compared to validity, true in all interpretations? $\endgroup$ – Nift Apr 17 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řábek Apr 18 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.

| cite | improve this answer | |

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.