Refutation in first order logic

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?

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

or


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

StackExchange Computer Science Q#103796, answer score: 3