Consider the following statement

In FOL, we can reduce entailment checking to satisfiability checking:

$S \models S' \iff S \land \neg S'$ is satisfiable (This proof strategy is called refutation).

Is the above statement true? If yes, then I got confusion because of the following steps

$ S \models S' \iff S\implies S'$ is true

$S \models S' \iff \neg S \lor S'$ is satisfiable

$S \models S' \iff \neg( S \land \neg S') $ is satisfiable

$S \models S' \iff S \land \neg S' $ is unsatisfiable

Which one is true?

  • 1
    $\begingroup$ This is a math question, and belongs in Mathematics. $\endgroup$ Feb 3, 2019 at 15:38
  • 2
    $\begingroup$ @YuvalFilmus I disagree. Logic is fundamental to CS. $\endgroup$ Feb 3, 2019 at 16:40

1 Answer 1


This looks like a typo in your source, and your derivation looks correct. So the corrected statement should be:

$S \models S' \iff S \land \neg S'$ is unsatisfiable


$S \models S' \iff {\boldsymbol \neg} (S \land \neg S')$ is satisfiable


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.